# The Bove-Cappretta 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.
Require Import Arith Lia Relations Utf8.
Import Sigma_Notations.

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 le_lt_dec n 100 then m = 91 else m = n - 10.
Proof.
induction 1; repeat destruct le_lt_dec; try lia; auto.
Qed.

(* Do not simpl the (101 - n) call *)
Arguments minus : simpl never.

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 le_lt_dec n 100 := {
| left H := ((f91_exists (f91_exists (n + 11)).1).1, _) ;
| right H := (n - 10, _) }.
Proof.
all:hnf. 2-3:edestruct f91_exists; cbn.
3:destruct f91_exists. lia.
apply f91_spec in pr2. destruct le_lt_dec; subst; lia.
econstructor 2; eauto. constructor. lia.
Defined.

Combining these two things allow us to derive the spec of f91.
Lemma f91 n : (f91_exists n).1 = if le_lt_dec n 100 then 91 else n - 10.
Proof.
destruct f91_exists. simpl. generalize (f91_spec _ _ pr2).
destruct le_lt_dec; auto.
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)
( n', f91_graph (n + 11) n' f91_dom n')
f91_dom n.

Lemma le_nle n : n 100 100 < n False.
Proof. lia. Qed.

These two structural inversion lemmas are essential: we rely on the fact that they return subterms of their prf argument below to define f91_ongraph by structural recursion.

Equations f91_dom_le_inv_l {n} (prf : f91_dom n) (Hle : n 100) : f91_dom (n + 11) :=
| f91_dom_gt n H | Hle := ltac:(elimtype False; eauto using le_nle);
| f91_dom_le n H Hd Hg | Hle := Hd.

Equations f91_dom_le_inv_r {n} (prf : f91_dom n) (Hle : n 100) : ( n', f91_graph (n + 11) n' f91_dom n') :=
| f91_dom_gt n H | Hle := ltac:(elimtype False; eauto using le_nle);
| f91_dom_le n H Hd Hg | Hle := Hg.

Module WithSigma.

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 le_lt_dec n 100 :=
{ | left H((f91_ongraph (f91_ongraph (n + 11) _).1 _).1, _);
| right H(n - 10, _) }.
Proof.
clear f91_ongraph.
destruct prf. elimtype False; lia.
apply prf.
destruct f91_ongraph. clear f91_ongraph. simpl. eapply f91_dom_le_inv_r in prf; eauto.
destruct f91_ongraph. simpl in ×.
destruct f91_ongraph. clear f91_ongraph. simpl in ×.
econstructor 2; eauto.
constructor. lia.
Defined.

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. *)
End WithSigma.

Module WithSubset.

Same thing with a subset type for cleaner extraction. We use Program Mode to avoid explicit projections/injections into subset types.

Set Program Mode.
Equations? f91_ongraph n (prf : f91_dom n) : { r | f91_graph n r } by struct prf :=
f91_ongraph n prf with le_lt_dec n 100 :=
{ | left Hf91_ongraph (f91_ongraph (n + 11) _) _;
| right Hn - 10 }.
Proof.
clear f91_ongraph.
destruct prf. elimtype False; lia.
apply prf.
destruct f91_ongraph. clear f91_ongraph. simpl. eapply f91_dom_le_inv_r in prf; eauto.
destruct f91_ongraph. simpl in ×.
destruct f91_ongraph. clear f91_ongraph. simpl in ×.
econstructor 2; eauto.
constructor. lia.
Defined.

Lemma f91_ongraph_spec n dom : proj1_sig (f91_ongraph n dom) = if le_lt_dec n 100 then 91 else n - 10.
Proof.
destruct f91_ongraph. simpl. generalize (f91_spec _ _ f).
destruct le_lt_dec; auto.
Qed.

All proof witnesses f91_dom n and f91_graph n r disappear at extraction time, giving the "real" f91 implementation.

(* Extraction f91_ongraph. *)
End WithSubset.