(**************************************************************)
(*   Copyright                                                *)
(*             Jean-François Monin           [+]              *)
(*             Dominique Larchey-Wendling    [*]              *)
(*                                                            *)
(*            [+] Affiliation VERIMAG - Univ. Grenoble-Alpes  *)
(*            [*] Affiliation LORIA -- CNRS                   *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import Utf8 Extraction.

(* Target : nb of g steps to get some condition b
      let rec  ns x = match b x with true => 0 | false => S (ns (g x))
   Easy case: b corresponds to a constructor, say O in nat
      let  rec ns0 x = match x with O => 0 | S _ => S (ns0 (g x))
   Algorithm using an accumulator
    let rec nsa x n = match b x with true => n | false => nsa (g x) (S n)
    let rec ns0a x n = match x with O => n | S _ => ns0a (g x) (S n)
   We prove that ns0/ns computes the same result as ns0a/nsa
*)

Section sec_nb_steps.

Variable (X : Type) (g : X -> X) (b : X -> bool).

Let is_false (x: bool) := match x with false => True | _ => False end.

Unset Elimination Schemes.

Inductive 𝔻ns (x: X) : Prop :=
  | 𝔻ns_tr : b x = true → 𝔻ns x
  | 𝔻ns_fa : b x = false → 𝔻ns (g x) → 𝔻ns x
.

Scheme 𝔻ns_ind := Induction for 𝔻ns Sort Prop.
Check 𝔻ns_ind.
(*
∀ P : ∀ x : X, 𝔻ns x → Prop,
      (∀ (x : X) (e : b x = true), P x (𝔻ns_tr x e))
    → (∀ (x : X) (e : b x = false) (𝔻 : 𝔻ns (g x)), P (g x) 𝔻 → P x (𝔻ns_fa x e 𝔻))
    → ∀ (x : X) (𝔻 : 𝔻ns x), P x 𝔻
 *)


(* prj_𝔻ns a little bit more complicated *)

Let false_true {x} : x = false -> x = true -> False.
Proof. intros ->; discriminate. Qed.

Print false_true.

Definition prj_𝔻ns {x} (E: b x = false) (D :  𝔻ns x) :  𝔻ns (g x) :=
  match D with
  | 𝔻ns_tr _ E'   => match false_true E E' with end
  | 𝔻ns_fa _ _ D  => D
  end.

Section sec_direct_ns.
(* "Let" in order to forget ns and nsa after this section *)  
Let
Fixpoint ns x (D: 𝔻ns x) : nat :=
  match b x as bx return b x = bx → _ with
  | true => λ E, 0
  | false => λ E, S (ns (g x) (prj_𝔻ns E D))
  end eq_refl.

Let
Fixpoint nsa x (n: nat) (D: 𝔻ns x) : nat :=
  match b x as bx return b x = bx → _ with
  | true => λ E, n
  | false => λ E, nsa (g x) (S n) (prj_𝔻ns E D)
  end eq_refl.

Lemma ns_nsa_n_direct : ∀x (D: 𝔻ns x) n, nsa x n D = ns x D + n.
Proof.
 induction D as [x E | x E D IHD]; intro n; simpl.
  - rewrite E. reflexivity.
  - rewrite IHD. rewrite E. rewrite <- plus_n_Sm. reflexivity.
Qed.

Corollary ns_nsa_direct : ∀x (D: 𝔻ns x), nsa x 0 D = ns x D.
Proof. intros x D. now rewrite ns_nsa_n_direct, plus_n_O. Qed.

End sec_direct_ns.

Set Elimination Schemes.

(* ---------------------------------------------------------------------- *)

Reserved Notation "x '⟼ns' y" (at level 70, no associativity).
Inductive 𝔾ns (x: X) : nat → Prop :=
  | in_grns_0   : b x = true  →  x ⟼ns 0
  | in_grns_1 o : b x = false →  g x ⟼ns o  →  x ⟼ns S o
where "x ⟼ns o" := (𝔾ns x o).

Reserved Notation "x ',' n '⟼nsa' y" (at level 70, no associativity).
Inductive 𝔾nsa (x: X) (n: nat) : nat → Prop :=
  | in_grnsa_0   : b x = true  →  x, n ⟼nsa n
  | in_grnsa_1 o : b x = false →  g x, S n ⟼nsa o  →  x, n ⟼nsa o
where "x , n ⟼nsa o" := (𝔾nsa x n o).

Fact 𝔾ns_fun x u v : x ⟼ns u  →  x ⟼ns v  →  u = v.
Proof.
  intros H; revert H v.
  induction 1 as [ x E | x o E H1 IH1 ]; inversion 1; auto.
  - rewrite E in H0. discriminate H0.
  - rewrite E in H0. discriminate H0.
Qed.

Fact 𝔾nsa_fun x n u v : x, n ⟼nsa u  →  x, n ⟼nsa v  →  u = v.
Proof.
  intros H; revert H v.
  induction 1 as [ x n E | x n o E H1 IH1 ]; inversion 1; auto.
  - rewrite E in H0. discriminate H0.
  - rewrite E in H0. discriminate H0.
Qed.


Let Fixpoint ns_pwc x (D: 𝔻ns x) : {o | x ⟼ns o}.
Proof. refine(
   match b x as bx return b x = bx → _ with
   | true => λ E, exist _ 0 _
   | false => λ E, let (o,Go) := ns_pwc (g x) (prj_𝔻ns E D)
                   in exist _ (S o) _
   end eq_refl).
  - constructor 1; exact E.
  - constructor 2; assumption.
Defined.

Let Fixpoint nsa_pwc x n (D: 𝔻ns x) : {o | x, n ⟼nsa o}.
Proof. refine(
   match b x as bx return b x = bx → _ with
   | true => λ E, exist _ n _
   | false => λ E, let (o,Go) := nsa_pwc (g x) (S n) (prj_𝔻ns E D)
                   in exist _ o _
   end eq_refl).
  - constructor 1; exact E.
  - constructor 2; assumption.
Defined.

Definition ns (x: X) D : nat := proj1_sig (ns_pwc x D).

(* ns is correct wrt its agnostic specification *)
Fact ns_correct {x} D : x ⟼ns ns x D.
Proof. apply (proj2_sig _). Qed.

(* ns is complete wrt its agnostic specification *)
Lemma ns_complete {x o} : x ⟼ns o  ->  ∀D, o = ns x D.
Proof.
  intros G D.
  assert (G': x ⟼ns ns x D) by (apply (ns_correct D)).
  apply (𝔾ns_fun x); assumption.
Qed.

Definition nsa (x: X) (n: nat) D : nat := proj1_sig (nsa_pwc x n D).

(* nsa is correct wrt its agnostic specification *)
Fact nsa_correct {x n} D : x, n ⟼nsa nsa x n D.
Proof. apply (proj2_sig _). Qed.

(* nsa is complete wrt its agnostic specification *)
Lemma nsa_complete {x n o} : x,n ⟼nsa o  ->  ∀D, o = nsa x n D.
Proof.
  intros G D.
  assert (G': x,n ⟼nsa nsa x n D) by (apply (nsa_correct D)).
  apply (𝔾nsa_fun x n); assumption.
Qed.

(* The specification of ns satifies the specification of nsa in some sense *)
Lemma gr_ns_nsa_n : ∀{x o}, x ⟼ns o  ->  ∀n, x, n ⟼nsa (o + n).
Proof.
  intros x o G. induction G as [ x E | x o E G IH]; intro n.
  - constructor 1. exact E.
  - constructor 2.
    + exact E.
    + change (S o + n) with (S (o + n)). rewrite plus_n_Sm. apply (IH (S n)).
Qed.

Corollary gr_ns_nsa : ∀{x o}, x ⟼ns o  ->  x, 0 ⟼nsa o.
Proof. intros x o G. rewrite plus_n_O. apply gr_ns_nsa_n, G. Qed.

(* The desired theorem follows *)
Theorem ns_nsa : ∀x (D: 𝔻ns x), nsa x 0 D = ns x D.
Proof.
  intros x D.
  rewrite <- (nsa_complete (gr_ns_nsa (ns_correct D))).
  reflexivity.
Qed.

End sec_nb_steps.


Extract Inductive bool => "bool" [ "true" "false" ].
Recursive Extraction ns nsa.

(*
let rec ns g b x =
  if b x then O else S (ns g b (g x))

let rec nsa g b x n =
  if b x then n else nsa g b (g x) (S n)
*)