Inductive aexp :=
| Aco : nat -> aexp
| Ava : nat -> aexp
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Asu : aexp -> aexp -> aexp
.

Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp -> bexp
| Band : bexp -> bexp -> bexp
| Bor : bexp -> bexp -> bexp
| Beq : bexp -> bexp -> bexp
| Beqnat : aexp -> aexp -> bexp
.

Inductive winstr :=
| Skip   : winstr
| Assign : nat -> aexp -> winstr
| Seq    : winstr -> winstr -> winstr
| If     : bexp -> winstr -> winstr -> winstr
| While  : bexp -> winstr -> winstr
.

Require Import List.
Import ListNotations.

Definition state := list nat.

Fixpoint get (i:nat) (s:state) : nat :=
  match i,s with
  | 0   ,  v :: _   => v
  | S i',  _ :: s'  => get i' s'
  | _   ,  _        => 0
  end.

Fixpoint update (s:state) (i:nat) (v:nat) : state :=
  match i,s with
  | 0   , a :: s' => v :: s'
  | 0   , []      => v :: nil
  | S i', a :: s' => a :: (update s' i' v)
  | S i', []      => 0 :: (update [] i' v)
  end.

Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n     =>  n
  | Ava x     =>  get x s
  | Apl a1 a2 =>  evalA a1 s + evalA a2 s
  | Amu a1 a2 =>  evalA a1 s * evalA a2 s
  | Asu a1 a2 =>  evalA a1 s - evalA a2 s
  end.

Definition eqboolb b1 b2 : bool :=
  match b1, b2  with
  | true , true  => true
  | false, false => true
  | _    , _     => false
  end.

Fixpoint eqnatb n1 n2 : bool :=
  match n1, n2 with
  | O    , O     => true
  | S n1', S n2' => eqnatb n1' n2'
  | _    , _     => false
  end.

Fixpoint evalB (b : bexp) (s : state) : bool :=
  match b with
  | Btrue => true
  | Bfalse => false
  | Bnot b => negb (evalB b s)
  | Band e1 e2 => (evalB e1 s) && (evalB e2 s)
  | Bor e1 e2 => (evalB e1 s) || (evalB e2 s)
  | Beq e1 e2 => eqboolb (evalB e1 s) (evalB e2 s)
  | Beqnat n1 n2 => eqnatb (evalA n1 s) (evalA n2 s)
  end.

Fail Fixpoint evalW (i : winstr) (s : state) {struct i} : state :=
  match i with
  | Skip       => s
  | Assign x e => update s x (evalA e s)
  | Seq i1 i2  => let s1 := evalW i1 s in evalW i2 s1
               (*   (evalW i2 (evalW i1 s) *)
  | If e i1 i2 => match evalB e s with
                  | true  => evalW i1 s
                  | false => evalW i2 s
                  end
  | While e i1 => match evalB e s with
                  | true  =>
                    let s1 := evalW i1 s in evalW (While e i1) s1
                  | false => s
                  end
  end.

(* Inductive NS : winstr -> state -> state -> SProp := *)
Inductive NS : winstr -> state -> state -> Prop :=
| NS_Skip        : forall s,
                   NS Skip s s
| NS_Assign      : forall x a s,
                   NS (Assign x a) s (update s x (evalA a s))
| NS_Seq         : forall {i1 i2 s s1 s2},
                   NS i1 s s1 -> NS i2 s1 s2 -> NS (Seq i1 i2) s s2
| NS_If_true     : forall {b i1 i2 s s1},
                   (evalB b s = true)  ->  NS i1 s s1 -> NS (If b i1 i2) s s1
| NS_If_false    : forall {b i1 i2 s s2},
                   (evalB b s = false) ->  NS i2 s s2 -> NS (If b i1 i2) s s2
| NS_While_false : forall {b i s},
                   (evalB b s = false) ->  NS (While b i) s s
| NS_While_true  : forall {b i s s1 s2},
                   (evalB b s = true)  ->  NS i s s1 -> NS (While b i) s1 s2 ->
                   NS (While b i) s s2
.

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

Inductive DNS : winstr -> state -> Prop :=
| DNS_Skip        : forall s,
                   DNS Skip s
| DNS_Assign      : forall x a s,
                   DNS (Assign x a) s
| DNS_Seq         : forall {i1 i2 s},
                   DNS i1 s -> (forall s1, NS i1 s s1 -> DNS i2 s1) -> DNS (Seq i1 i2) s
| DNS_If          : forall {b i1 i2 s},
                   (evalB b s = true  ->  DNS i1 s) ->
                   (evalB b s = false ->  DNS i2 s) -> DNS (If b i1 i2) s
| DNS_While       : forall {b i s},
                   (evalB b s = true  ->  DNS i s) ->
                   (evalB b s = true  -> forall s1, NS i s s1 -> DNS (While b i) s1) ->
                   DNS (While b i) s
.

Definition DNS_While_false {b i s} : evalB b s = false ->  DNS (While b i) s.
Proof.
  intro ef.
  refine (@DNS_While b i s _ _).
  - intro et.
    change i with (if true then i else Skip).
    case et; rewrite ef; apply DNS_Skip.
  - intros et s1 _.
    change (While b i) with (if true then While b i else Skip).
    case et; rewrite ef; apply DNS_Skip.
Defined.

Definition DNS_Seq_pi1 {i1 i2 s} (δ : DNS (Seq i1 i2) s) : DNS i1 s :=
  match δ in DNS i s return
        let i1 := match i with Seq i1 i2 => i1 | _ => i1 end in
        let shape := match i with Seq i1 i2 => True | _ => False end in
        shape -> DNS i1 s
  with
  | DNS_Seq δ1 fδ2 => fun _ => δ1
  | _ => fun sh => match sh with end
  end I.

Definition DNS_Seq_pi2 {i1 i2 s} (δ : DNS (Seq i1 i2) s) : forall s1, NS i1 s s1 -> DNS i2 s1 :=
  match δ in DNS i s return
        let i1 := match i with Seq i1 i2 => i1 | _ => i1 end in
        let i2 := match i with Seq i1 i2 => i2 | _ => i2 end in
        let shape := match i with Seq i1 i2 => True | _ => False end in
        shape -> forall s1, NS i1 s s1 -> DNS i2 s1
  with
  | DNS_Seq δ1 fδ2 => fun _ => fδ2
  | _ => fun sh => match sh with end
  end I.

Definition DNS_If_pi1 {b i1 i2 s} (δ : DNS (If b i1 i2) s) : evalB b s = true  ->  DNS i1 s :=
  match δ in DNS i s return
        let b := match i with If b i1 i2 => b | _ => b end in
        let i1 := match i with If b i1 i2 => i1 | _ => i1 end in
        let shape := match i with If b i1 i2 => True | _ => False end in
        shape -> evalB b s = true  ->  DNS i1 s
  with
  | DNS_If fδ1 fδ2 => fun _ => fδ1
  | _ => fun sh => match sh with end
  end I.

Definition DNS_If_pi2 {b i1 i2 s} (δ : DNS (If b i1 i2) s) : evalB b s = false  ->  DNS i2 s :=
  match δ in DNS i s return
        let b := match i with If b i1 i2 => b | _ => b end in
        let i2 := match i with If b i1 i2 => i2 | _ => i2 end in
        let shape := match i with If b i1 i2 => True | _ => False end in
        shape -> evalB b s = false  ->  DNS i2 s
  with
  | DNS_If fδ1 fδ2 => fun _ => fδ2
  | _ => fun sh => match sh with end
  end I.

Definition DNS_While_pi1 {b i s} (δ : DNS (While b i) s) : evalB b s = true  ->  DNS i s :=
  match δ in DNS bi s return
        let b := match bi with While b i => b | _ => b end in
        let i := match bi with While b i => i | _ => i end in
        let shape := match bi with While b i => True | _ => False end in
        shape -> evalB b s = true  ->  DNS i s
  with
  | DNS_While fδ1 fδ2 => fun _ => fδ1
  | _ => fun sh => match sh with end
  end I.

Definition DNS_While_pi2 {b i s} (δ : DNS (While b i) s) :
  evalB b s = true  -> forall s1, NS i s s1 -> DNS (While b i) s1 :=
  match δ in DNS bi s return
        let b := match bi with While b i => b | _ => b end in
        let i := match bi with While b i => i | _ => i end in
        let shape := match bi with While b i => True | _ => False end in
        shape -> evalB b s = true  ->  forall s1, NS i s s1 -> DNS (While b i) s1
  with
  | DNS_While fδ1 fδ2 => fun _ => fδ2
  | _ => fun sh => match sh with end
  end I.

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

Arguments exist {A P}.

Inductive sigNS i s : Set := exist: forall s', NS i s s' -> sigNS i s.
Arguments exist {i s}.

(*Fixpoint evalW (i : winstr) (s : state) (δ : DNS i s) {struct δ} : {s' | NS i s s'} :=*)
Fixpoint evalW (i : winstr) (s : state) (δ : DNS i s) {struct δ} : sigNS i s :=
  match i return DNS i s -> _ with
  | Skip       => fun δ => exist s                                (* *) (NS_Skip s)
  | Assign x e => fun δ => exist (update s x (evalA e s))         (* *) (NS_Assign x e s)
  | Seq i1 i2  => fun δ =>
                  let (s1, γ1) := evalW i1 s  (DNS_Seq_pi1 δ) in
                  let (s2, γ2) := evalW i2 s1 (DNS_Seq_pi2 δ s1 γ1) in
                  exist s2                                        (* *) (NS_Seq γ1 γ2)
  | If e i1 i2 => fun δ =>
                  match evalB e s as b return _ = b -> _ with
                  | true  => fun et =>
                             let (s', γ) := evalW i1 s (DNS_If_pi1 δ et) in
                             exist s'                             (* *) (NS_If_true et γ)
                  | false => fun ef =>
                             let (s', γ) := evalW i2 s (DNS_If_pi2 δ ef) in
                             exist s'                             (* *) (NS_If_false ef γ)
                  end eq_refl
  | While e i as w => fun δ =>
                  match evalB e s as b return _ = b -> _ with
                  | true  => fun et =>
                             let (s1, γ1) := evalW i s  (DNS_While_pi1 δ et) in
                             let (s2, γ2) := evalW w s1 (DNS_While_pi2 δ et s1 γ1) in
                             exist s2                             (* *) (NS_While_true et γ1 γ2)
                  | false => fun ef =>
                             exist s                              (* *) (NS_While_false ef)
                  end eq_refl

  end δ.

Reset evalW.

Inductive rembool b : Set :=
| remtrue  : b = true  -> rembool b
| remfalse : b = false -> rembool b.
Arguments remtrue {b}.
Arguments remfalse {b}.

Definition remb (b : bool) : rembool b :=
  match b as b0 return _ = b0 -> rembool b with
  | true  => fun e => remtrue e
  | false => fun e => remfalse e
  end eq_refl.

Definition remevalB e s := remb (evalB e s).

Fixpoint evalW (i : winstr) (s : state) (δ : DNS i s) {struct δ} : sigNS i s :=
  match i return DNS i s -> _ with
  | Skip       =>                                       fun δ =>
                  exist s                                         (* *) (NS_Skip s)
  | Assign x e =>                                       fun δ =>
                  exist (update s x (evalA e s))                  (* *) (NS_Assign x e s)
  | Seq i1 i2  =>                                       fun δ =>
                  let (s1, γ1) := evalW i1 s            (DNS_Seq_pi1 δ)           in
                  let (s2, γ2) := evalW i2 s1           (DNS_Seq_pi2 δ s1 γ1)     in
                  exist s2                                        (* *) (NS_Seq γ1 γ2)
  | If e i1 i2 =>                                       fun δ =>
                  match remevalB e s with
                  | remtrue et =>
                      let (s', γ) := evalW i1 s         (DNS_If_pi1 δ et)          in
                      exist s'                                    (* *) (NS_If_true et γ)
                  | remfalse ef =>
                      let (s', γ) := evalW i2 s         (DNS_If_pi2 δ ef)          in
                      exist s'                                    (* *) (NS_If_false ef γ)
                  end
  | While e i as w =>                                   fun δ =>
                  match remevalB e s with
                  | remtrue et =>
                      let (s1, γ1) := evalW i s         (DNS_While_pi1 δ et)       in
                      let (s2, γ2) := evalW w s1        (DNS_While_pi2 δ et s1 γ1) in
                      exist s2                                    (* *) (NS_While_true et γ1 γ2)
                  | remfalse ef =>
                      exist s                                     (* *) (NS_While_false ef)
                  end

  end δ.

(** Jjst the reslting state *)
Definition resuW p s δ := let (s', _) := evalW p s δ in s'.

(* -------------------------------------------------------------------------------- *)
(** A WHILE program [P1] corresponding to
    while not (i=0) do {i := i-1; x := 1+x} *)

Example N0 := Aco 0.
Example N1 := Aco 1.
Example N2 := Aco 2.


Example Il := 0.
Example Ir := Ava Il.
Example Xl := 1.
Example Xr := Ava Xl.

Example body_loop := Seq (Assign Il (Asu Ir N1)) (Assign Xl (Apl N1 Xr)).
Example P1 := While (Bnot (Beqnat Ir N0)) body_loop.

(** Here is a While program Psquare corresponding to
    while not (i=n) do {i:= 1+i; x:= y+x ; y:= 2+y} *)

Example Yl := 2.
Example Yr := Ava Yl.

Example incrI := Assign Il (Apl N1 Ir).
Example incrX := Assign Xl (Apl Yr Xr).
Example incrY := Assign Yl (Apl N2 Yr).
Example body_square := Seq incrI (Seq incrX incrY).
Example Psquare_2 := While (Bnot (Beqnat Ir (Aco 2))) body_square.
Example Psquare n := While (Bnot (Beqnat Ir (Aco n))) body_square.

(* -------------------------------------------------- *)
(** Small inversion of NS *)

Inductive NS1_Skip: state -> state -> Prop :=
| NS_Skip'        : forall s,
                    NS1_Skip s s
.
Inductive NS1_Assign (v: nat) (a: aexp) (s : state) : state -> Prop :=
| NS_Assign'      :
                    NS1_Assign v a s (update s v (evalA a s))
.
Inductive NS1_Seq i1 i2 s s2 : Prop :=
| NS_Seq'         : forall s1,
                    NS i1 s s1 -> NS i2 s1 s2 -> NS1_Seq i1 i2 s s2
.
Inductive NS1_If (b: bexp) (i1 i2: winstr) s s' : Prop :=
| NS_If_true'     : (evalB b s = true)  ->  NS i1 s s' -> NS1_If b i1 i2 s s'
| NS_If_false'    : (evalB b s = false) ->  NS i2 s s' -> NS1_If b i1 i2 s s'
.
Inductive NS1_While (b: bexp) (i: winstr) s : state -> Prop :=
| NS_While_false' : (evalB b s = false) ->  NS1_While b i s s
| NS_While_true'  : forall s1 s2,
                    (evalB b s = true)  ->  NS i s s1 -> NS (While b i) s1 s2 ->
                    NS1_While b i s s2.

Definition dispatch (i: winstr) : state -> state -> Prop :=
  match i with
  | Skip => NS1_Skip
  | Assign v a => NS1_Assign v a
  | Seq i1 i2 => NS1_Seq i1 i2
  | If b i1 i2 => NS1_If b i1 i2
  | While b i => NS1_While b i
  end.

Definition NS_inv {i s s2} (ns : NS i s s2) : dispatch i s s2.
Proof. destruct ns; econstructor; eassumption. Defined.

(* -------------------------------------------------- *)
(** Execution of program P1 *)

(** Std lib lemma, transparent version. *)
Lemma sub_0_r n : n - 0 = n.
Proof. destruct n as [ | n]; reflexivity. Defined.

Definition P1_all : forall i x, DNS P1 [i; x].
Proof.
  induction i as [ | i Hi]; intro x.
  - apply DNS_While_false. cbn. reflexivity.
  - apply DNS_While; intro e; clear e (* evalB b s = true trivial & unused *).
    + apply DNS_Seq.
      ++ apply DNS_Assign.
      ++ intros s' nsa. destruct (NS_inv nsa). cbn in *. apply DNS_Assign.
    + intros s' nsb. change (DNS P1 s').
      destruct (NS_inv nsb) as [s1 nsi nsx]; clear nsb.
      destruct (NS_inv nsi); clear nsi. cbn in *. rewrite sub_0_r in nsx.
      destruct (NS_inv nsx); clear nsx. cbn. apply Hi.
Defined.

(** For extraction *)
Definition exec_P1 i x := evalW P1 [i; x] (P1_all i x).

Definition resu_P1 i x := resuW P1 [i; x] (P1_all i x).
Eval lazy in resu_P1 1 0.
Eval lazy in resu_P1 3 2.

(* -------------------------------------------------- *)
(** Execution of program P_square *)

Lemma rev_natind {P : nat -> Prop} :
  forall n : nat, P n -> (forall i : nat, i <> n -> P (S i) -> P i) -> P 0.
Admitted. (* Defined *)

Lemma eqnatb_refl : forall n, eqnatb n n = true.
Proof.
  induction n as [| n Hn]; trivial.
Defined.

Definition contagious_false_true : false = true -> forall {T} (x y : T), x = y.
Proof. intros e *. change y with (if true then y else x). case e. reflexivity. Defined.

Fixpoint eqnatb_true n m : eqnatb n m = true -> n = m :=
  match n, m with
  | 0, 0 => fun _ => eq_refl
  | S n, S m => fun e => f_equal S (eqnatb_true n m e)
  | 0, S m => fun e => contagious_false_true e 0 (S m)
  | S n, 0 => fun e => contagious_false_true e (S n) 0
  end.
Arguments eqnatb_true {n m}.

Definition eqnatb_false {n m} : n <> m -> eqnatb n m = false :=
  fun ne =>
    match remb (eqnatb n m) with
    | remtrue et => match ne (eqnatb_true et) with end
    | remfalse ef => ef
    end.

Lemma plus_assoc n m p : n + (m + p) = n + m + p.
Proof. induction n as [| n Hn]; cbn; [ | case Hn]; reflexivity. Defined.

Lemma plus_n_Sm n m : n + S m = S (n + m).
Proof. induction n as [| n Hn]; cbn; [ | rewrite Hn]; reflexivity. Defined.

Lemma Sn_2 n : S n + S n = S (S (n + n)).
Proof.
Admitted. (* Defined *)

Lemma plus_exch n m x : n + (m + x) = m + (n + x).
Proof.
Admitted. (* Defined *)

Lemma mul_n_Sm n m : n * S m = n + n * m.
Proof.
Admitted. (* Defined *)

Lemma Sn_square n : S n * S n = S (n + n + n * n).
Proof. 
Admitted. (* Defined *)

(** Using std lib *)
(*
Require Import Arith.
Lemma Sn_2 n : S n + S n = S (S (n + n)).
Proof.  ring. Qed.

Lemma Sn_square n : S n * S n = S (n + n + n * n).
Proof. ring. Qed.
*)

Definition Psquare_all : forall n, DNS (Psquare n) [0; 0; 1].
Proof.
  intro n.
  change [0; 0; 1] with [0; 0*0; S(0+0)]. pattern 0. apply (rev_natind n).
  - apply DNS_While_false. cbn. rewrite eqnatb_refl. reflexivity.
  - intros i ne HSi.
    rewrite Sn_2 in HSi. rewrite Sn_square in HSi.
    eapply DNS_While; cbn; intro e; clear e (* evalB b s = true unused *).
    + apply DNS_Seq.
      { apply DNS_Assign. }
      intros s1 nsi. destruct (NS_inv nsi); clear nsi; cbn.
      apply DNS_Seq.
      { apply DNS_Assign. }
      intros s1 nsx. destruct (NS_inv nsx); clear nsx; cbn.
      apply DNS_Assign.
    + intros s3 ns.
      change (DNS (Psquare n) s3).
      destruct (NS_inv ns) as [s1 nsi nsxy]; clear ns.
      destruct (NS_inv nsi); clear nsi; cbn in nsxy.
      destruct (NS_inv nsxy) as [s2 nsx nsy]; clear nsxy.
      destruct (NS_inv nsx); clear nsx; cbn in nsy.
      destruct (NS_inv nsy); clear nsy; cbn.
      apply HSi.
Defined.

(** For extraction *)
Definition exec_Psquare n := evalW (Psquare n) [0; 0; 1] (Psquare_all n).

Definition resu_Psquare n := resuW (Psquare n) [0; 0; 1] (Psquare_all n).
(** Using transparent versions of arithmetic lemmas *)
(*
Eval lazy in resu_Psquare 0.
Eval lazy in resu_Psquare 50.
*)

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

Require Import Extraction.
Recursive Extraction evalW.

Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive rembool => "bool" [ "true" "false" ].
Extraction Inline remb remevalB.
Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Extract Inlined Constant plus => "(+)".
Extract Inlined Constant minus => "(-)".
Extract Inlined Constant mult => "( * )".
Extract Inlined Constant eqnatb => "(=)".
Extract Inlined Constant andb => "(&&)".
Extract Inlined Constant orb => "(||)".
Extract Inlined Constant negb => not.
Extract Inlined Constant eqboolb => "(=)".

(*Extract Inductive sigNS => "state" [""].*)

(*Extraction Inline Xl Xr Il Ir Yl Yr.*)

Recursive Extraction evalW P1 Psquare exec_P1 exec_Psquare.
Extraction "evalwinstr.ml" evalW P1 Psquare exec_P1 exec_Psquare.