Bove-Capretta w/ Equations+SSReflect

bove_capretta_ssr.v

(** * The Bove-Capretta method

   This method involves building the graph and/or domain of a recursive
   definition and to define it by recursion + inversion on that graph,
   but not direct pattern matching. We show a difficult example
   involving nested recursive calls. *)

From Equations Require Import Equations.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype.

Definition inspect {A} (a : A) : {b | a = b} :=
  exist _ a erefl.

Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).

(** The graph of the [f91] function. *)

Inductive f91_graph : nat -> nat -> Prop :=
| f91_gt n : n > 100 -> f91_graph n (n - 10)
| f91_le n nest res :
    n <= 100 -> f91_graph (n + 11) nest ->
    f91_graph nest res ->
    f91_graph n res.

Derive Signature for f91_graph.

(** It is easy to derive the spec of [f91] from it, by induction. *)
Lemma f91_spec n m : f91_graph n m -> if n <= 100 then m = 91 else m = n - 10.
Proof.
elim=>{m}n; first by rewrite ltnNge=>/negbTE->.
move=>nest res Hn _; rewrite Hn.
case: ifP=>_; first by move->.
rewrite -addnBA // (_ : 11 - 10 = 1) // => -> _.
case: ifP=>// /negbT; rewrite -ltnNge addn1 ltnS.
move: Hn; rewrite leq_eqVlt=>/orP; case; last by case: ltngtP.
by move/eqP=>->_->.
Qed.

(** One can construct the graph using a (relatively) complex termination argument.
    Note that it is required to know that the result is in the graph to show
    termination at the second, nested recursive call to [f91_exists]. *)

Equations? f91_exists n : {r | f91_graph n r} by wf (101 - n) lt :=
f91_exists n with inspect (n <= 100) := {
  | true eqn: H => let '(exist x fx) := f91_exists (n + 11) in
                   let '(exist y fy) := f91_exists x in
                   exist _ _ (f91_le _ _ _ H fx fy)
  | false eqn: H => exist _ (n - 10) _
  }.
Proof.
1-2: apply: ssrnat.ltP.
- by apply: ltn_sub2l=>//; rewrite -{1}(addn0 n) ltn_add2l.
- move: (f91_spec _ _ fx)=>/=; case: ifP.
  - rewrite {1}(_ : 100 = 89 + 11) // leq_add2r =>H2 ->.
    by rewrite ltn_sub2l //; apply: (leq_ltn_trans H2).
  move=>_->; apply: ltn_sub2l=>//.
  by rewrite -addnBA // addn1.
by apply: f91_gt; move: H=>/negbT; rewrite -ltnNge.
Defined.

(** Combining these two things allow us to derive the spec of [f91]. *)
Lemma f91 n : sval (f91_exists n) = if n <= 100 then 91 else n - 10.
Proof.
case: f91_exists=>x /= /f91_spec.
by case: ifP.
Qed.

(** This extracts to [f91]. *)
(* Extraction f91_exists. *)

(** An alternative is to use the domain of [f91] instead,
    which for nested recursive calls requires a quantification
    on the graph relation. *)

Inductive f91_dom : nat -> Prop :=
| f91_dom_gt n : n > 100 -> f91_dom n
| f91_dom_le n :
    n <= 100 -> f91_dom (n + 11) ->
    (forall n', f91_graph (n + 11) n' -> f91_dom n') ->
    f91_dom n.

(** This structural inversion lemma is essential: we rely on the fact
    that it returns a subterm of its [prf] argument below to define [f91_ongraph]
    by _structural_ recursion. *)

Equations f91_dom_le_inv_r {n} (prf : f91_dom n) (Hle : n <= 100) :
  forall n', f91_graph (n + 11) n' -> f91_dom n' :=
| f91_dom_gt n H | Hle := ltac:(by rewrite leqNgt H in Hle);
| f91_dom_le n H Hd Hg | Hle := Hg.

(** In this case, [f91_ongraph] is recursive on the domain proof, but only does
    inversion of it, not direct pattern-matching which would be forbidden as it
    lives in [Prop]. *)

Equations? f91_ongraph n (prf : f91_dom n) : {r | f91_graph n r} by struct prf :=
f91_ongraph n prf with inspect (n <= 100) := {
  | true eqn: H => let '(exist x fx) := f91_ongraph (n + 11) _ in
                   let '(exist y fy) := f91_ongraph x _ in
                   exist _ _ (f91_le _ _ _ H fx fy);
  | false eqn: H => exist _ (n - 10) _ }.
Proof.
- move: H; case: n / prf => // n Hn.
  by rewrite leqNgt Hn.
- by apply: (f91_dom_le_inv_r prf H).
by apply: f91_gt; move: H=>/negbT; rewrite -ltnNge.
Defined.

Lemma f91_ongraph_spec n dom : sval (f91_ongraph n dom) = if n <= 100 then 91 else n - 10.
Proof.
case: f91_ongraph=>/= x /f91_spec.
by case: ifP.
Qed.

(** The proof witness [f91_dom n] disappears at extraction time.
    But the polymorphic sigma type makes it leave a dummy unit value
    on the side.
 *)

(* Extraction f91_ongraph. *)