(** D Larchey-Wendling et JF Monin, 2018

    This example is from Bove&Capretta [MSCS05] p699 but here we do
    not need mutual Induction-Recursion definition as in that paper
    (they are NOT available in Coq)

    See also a first Coq approach by JF Monin
    
    http://www-verimag.imag.fr/~monin/Talks/talk_f91.pdf
    
    which uses Prop-domain termination certificates but which seems to
    need proof-relevance.
    
    Here we use a custom bar inductive predicate and combine it with
    the relational description of the desired fuction.
    The key idea of using bar-induction comes from D Larchey-Wendling.
 
    let rec f91 = if n > 100 then n - 10 else f91 (f91 (n+11))
    
    Generalization, for i, a and d fixed natural numbers: let rec g91
    = if n >= i then n - a else g91 (g91 (n+a+1+d))

    We also prove that when d=0, g91 n = max i n - a.  For arbitrary
    d, we only have g91 n + a >= max i n, which is enough to justify
    the head recursive call.
      
    No axiom needed.  No use of False_elim to get structurally smaller
    subterms.

    Using small inversions, it is then clearly possible to remove all
    uses of False_elim.

  *)

Require Import Arith.
Require Import PeanoNat. Import Nat.

(* TODO : small inversion instead of le_not_lt *)
Ltac False_le_lt := 
  match goal with
    [hle: ?x <= ?y, hlt: ?y < ?x |- _] => case (le_not_lt x y hle hlt)
  end.

(* Ad-hoc lemmas *)
Lemma max_plus_insert {i a b n m} : max i (a + b + n) <= a + m -> n <= m.
Proof.
  intros l. apply max_lub_r in l. 
  apply (le_le_add_le 0 b).
  - apply le_0_n.
  - rewrite <- plus_n_O; rewrite plus_comm.
    apply (add_le_mono_l _ _ a). rewrite plus_assoc. exact l.
Qed.

Lemma plus_n_Sm_p : forall n m p, n + S m + p = n + m + S p.
Proof. intros; rewrite <- plus_n_Sm; cbn; apply plus_n_Sm. Qed.

Definition always (P : nat -> Prop) n := forall m, n <= m -> P m.

Inductive bar (i: nat) (n : nat) : Prop :=
| bar_stop : i <= n -> (n < i -> forall m, bar i m) -> bar i n
| bar_again : always (bar i) (S n) -> bar i n.
Arguments bar_stop [i n] _. Arguments bar_again [i n] _.

Definition inv_bar {i n} (lni: n < i) (b: bar i n) : always (bar i) (S n) :=
  match b with 
    bar_stop _  F => fun m _ => F lni m  |  bar_again alb => alb
  end.

Lemma bar_always {i n} : bar i n -> always (bar i) n.
Proof. 
  intros b m lnm. destruct (le_lt_dec i n) as [ lin | lni ].
  - assert (lim : i <= m) by apply (le_trans _ _ _ lin lnm). apply (bar_stop lim).
    intro lmi; False_le_lt.
  - destruct lnm as [ | m]; [exact b | apply (inv_bar lni b (S m) (le_n_S _ _ lnm))]. 
Qed.

Lemma bar_cont : forall i n m, n <= m -> bar i m -> bar i n.
  intros i n m lnm. induction lnm as [| m lnm bnm]; intro b.  
  - exact b.
  - apply bnm. apply (bar_again (bar_always b)). 
Qed.

Fact bar_any : forall i n, bar i n.
Proof.
  intros i n. destruct (le_lt_dec i n) as [l | l].
  - apply (bar_stop l). intro F; False_le_lt.
  - apply (bar_cont i n i).
    + apply (Nat.lt_le_incl _ _ l).
    + refine ((fun lii => bar_stop lii _) (le_n i)). intro; False_le_lt.
Qed.

Section Loop.
  
  Variable i a d: nat.
  
  Inductive specg91 (n : nat) : nat -> Prop :=
  | G91_stop : i <= n -> specg91 n (n - a)
  | G91_again : n < i -> 
        forall y1 y2, specg91 (a+d + S n) y1 -> specg91 y1 y2 -> specg91 n y2.

  Arguments G91_stop [n] _. Arguments G91_again [n] _ [y1 y2] _ _.
  
  Lemma spec_max {n y} : specg91 n y -> max i n <= a + y. 
  Proof.
    intros sp; induction sp as [ n lin | n lni y1 y2 sp1 Hsp1 sp2 Hsp2].
    - rewrite max_r; [ rewrite plus_comm; apply sub_add_le | apply lin].
    - refine (le_trans _ _ _ _ Hsp2). apply max_le_compat_l. 
      rewrite <- plus_n_Sm_p in Hsp1. apply (max_plus_insert Hsp1).
  Qed.
  
  Fixpoint loop n (b : bar i n) { struct b } : {y : nat | specg91 n y}.
    refine (
        match le_lt_dec i n with
        | left lin => exist _ (n - a)   (G91_stop lin)
        | right lni =>
          let (y1, sp1) := loop (a+d + (S n)) _ in
          let (y2, sp2) := loop y1 _ in
          exist _ y2  (G91_again lni sp1 sp2)
        end); apply (inv_bar lni b). 
    Proof.
      - apply le_plus_r.
      - apply (max_plus_insert (spec_max sp1)).
    Defined.
    
    Definition g91 x : {y : nat | specg91 x y} := loop x (bar_any i x).
    
    Theorem result_when_d_is_0 :
      d = 0 -> forall n y, specg91 n y -> y = max i n - a.
    Proof.
      intros ed0 n y sp. induction sp as [ n lin | n lni y1 y2 sp1 Hsp1 sp2 Hsp2].
      - rewrite max_r.
        + reflexivity.
        + apply lin.
      - rewrite Hsp2. rewrite (max_l _ _ (lt_le_incl _ _ lni)).
        destruct (max_spec i (a + d + S n)) as [ [l e] | [l e] ]; rewrite e in Hsp1.
        + rewrite <- plus_assoc in Hsp1. rewrite plus_comm in Hsp1. rewrite add_sub in Hsp1.
          rewrite Hsp1. rewrite ed0; simpl. rewrite (max_l _ _ lni). reflexivity.
        + rewrite (max_l i y1); [ reflexivity | idtac ]. rewrite Hsp1. apply le_sub_l.
    Qed.
    
End Loop.

Print Assumptions g91.

Definition f91 := g91 101 10 0.

Extraction "g91.ml" loop g91 f91.