Require Export Arith.
 
Inductive aExp : Set :=
  Loc: nat ->  aExp
 | Num: nat ->  aExp
 | Plus: aExp -> aExp ->  aExp
 | Minus: aExp -> aExp ->  aExp
 | Mult: aExp -> aExp ->  aExp .
 
Inductive bExp : Set :=
  IMPtrue: bExp
 | IMPfalse: bExp
 | Equal: aExp -> aExp ->  bExp
 | LessEqual: aExp -> aExp ->  bExp
 | Not: bExp ->  bExp
 | Or: bExp -> bExp ->  bExp
 | aAnd: bExp -> bExp ->  bExp .
 
Inductive com : Set :=
  Skip: com
 | Assign: nat -> aExp ->  com
 | Scolon: com -> com ->  com
 | IfThenElse: bExp -> com -> com ->  com
 | WhileDo: bExp -> com ->  com .
 
Inductive state : Set :=
  no_location: state
 | one_location: nat -> nat -> state ->  state .
 
Theorem eq_nat_dec: (n, m : nat)  {n = m}+{~ n = m}.
Induction n; Induction m; Auto.
Intros q H'; Elim (H q); Auto.
Defined.
 
Lemma le_lt_dec: (n, m : nat)  {(le n m)}+{(lt m n)}.
Induction n.
Auto with arith.
Induction m.
Auto with arith.
Intros q H'; Elim (H q); Auto with arith.
Defined.
 
Fixpoint update_rec [s : state] : nat -> nat ->  state :=
 [v, n : nat]  Cases s of
                 no_location => s
                | (one_location v1 n1 s1) =>
                    Cases (eq_nat_dec v1 v) of
                      (left h) => (one_location v1 n s1)
                     | (right h) => (one_location v1 n1 (update_rec s1 v n))
                    end
               end.
 
Fixpoint value_rec [s : state] : nat ->  nat :=
 [v : nat]
  Cases s of
    no_location => O
   | (one_location v1 n1 s1) =>
       Cases (eq_nat_dec v1 v) of (left h) => n1 | (right h) => (value_rec s1 v)
       end
  end.
 
Inductive update_ind : state -> nat -> nat -> state ->  Prop :=
  update_no_location: (v, n : nat)  (update_ind no_location v n no_location)
 | update_first:
     (v, n1, n2 : nat)
     (s1 : state)
      (update_ind (one_location v n1 s1) v n2 (one_location v n2 s1))
 | update_rest:
     (v1, v2, n1, n2 : nat)
     (s1, s2 : state)
     ~ v1 = v2 ->
     (update_ind s1 v2 n2 s2) ->
      (update_ind (one_location v1 n1 s1) v2 n2 (one_location v1 n1 s2)) .
 
Inductive value_ind : state -> nat -> nat ->  Prop :=
  no_such_location: (v : nat)  (value_ind no_location v O)
 | first: (v, n : nat) (s : state)  (value_ind (one_location v n s) v n)
 | rest:
     (v, v1, n, n1 : nat)
     (s : state)
     ~ v = v1 -> (value_ind s v n) ->  (value_ind (one_location v1 n1 s) v n) .
 
Fixpoint evalaExp_rec [a : aExp] : state ->  nat :=
 [s : state]
  Cases a of
    (Loc v) => (value_rec s v)
   | (Num n) => n
   | (Plus a1 a2) => (plus (evalaExp_rec a1 s) (evalaExp_rec a2 s))
   | (Minus a1 a2) => (minus (evalaExp_rec a1 s) (evalaExp_rec a2 s))
   | (Mult a1 a2) => (mult (evalaExp_rec a1 s) (evalaExp_rec a2 s))
  end.
 
Inductive evalaExp_ind : aExp -> state -> nat ->  Prop :=
  eval_Loc:
    (v, n : nat) (s : state) (value_ind s v n) ->  (evalaExp_ind (Loc v) s n)
 | eval_Num: (n : nat) (s : state)  (evalaExp_ind (Num n) s n)
 | eval_Plus:
     (a0, a1 : aExp)
     (n0, n1, n : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) ->
     n = (plus n0 n1) ->  (evalaExp_ind (Plus a0 a1) s n)
 | eval_Minus:
     (a0, a1 : aExp)
     (n0, n1, n : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) ->
     n = (minus n0 n1) ->  (evalaExp_ind (Minus a0 a1) s n)
 | eval_Mult:
     (a0, a1 : aExp)
     (n0, n1, n : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) ->
     n = (mult n0 n1) ->  (evalaExp_ind (Mult a0 a1) s n) .
 
Fixpoint evalbExp_rec [b : bExp] : state ->  bool :=
 [s : state]
  Cases b of
    IMPtrue => true
   | IMPfalse => false
   | (Equal a1 a2) =>
       Cases (eq_nat_dec (evalaExp_rec a1 s) (evalaExp_rec a2 s)) of
       (left h) => true | (right h) => false end
   | (LessEqual a1 a2) =>
       Cases (le_lt_dec (evalaExp_rec a1 s) (evalaExp_rec a2 s)) of
       (left h) => true | (right h) => false end
   | (Not b1) =>
       Cases (evalbExp_rec b1 s) of true => false | false => true end
   | (Or b1 b2) =>
       Cases (evalbExp_rec b1 s) of true => true | false => (evalbExp_rec b2 s)
       end
   | (aAnd b1 b2) =>
       Cases (evalbExp_rec b1 s) of false => false | true => (evalbExp_rec b2 s)
       end
  end.
 
Inductive evalbExp_ind : bExp -> state -> bool ->  Prop :=
  eval_IMPtrue: (s : state)  (evalbExp_ind IMPtrue s true)
 | eval_IMPfalse: (s : state)  (evalbExp_ind IMPfalse s false)
 | eval_Equal:
     (a0, a1 : aExp)
     (n0, n1 : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) -> n0 = n1 ->  (evalbExp_ind (Equal a0 a1) s true)
 | eval_UnEqual:
     (a0, a1 : aExp)
     (n0, n1 : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) ->
     ~ n0 = n1 ->  (evalbExp_ind (Equal a0 a1) s false)
 | eval_LessEqual:
     (a0, a1 : aExp)
     (n0, n1 : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) ->
     (le n0 n1) ->  (evalbExp_ind (LessEqual a0 a1) s true)
 | eval_NotLessEqual:
     (a0, a1 : aExp)
     (n0, n1 : nat)
     (s : state)
     (evalaExp_ind a0 s n0) ->
     (evalaExp_ind a1 s n1) ->
     ~ (le n0 n1) ->  (evalbExp_ind (LessEqual a0 a1) s false)
 | eval_Not_true:
     (b : bExp)
     (s : state) (evalbExp_ind b s true) ->  (evalbExp_ind (Not b) s false)
 | eval_Not_false:
     (b : bExp)
     (s : state) (evalbExp_ind b s false) ->  (evalbExp_ind (Not b) s true)
 | eval_Or_false:
     (b0, b1 : bExp)
     (s : state)
     (evalbExp_ind b0 s false) ->
     (evalbExp_ind b1 s false) ->  (evalbExp_ind (Or b0 b1) s false)
 | eval_Or_true:
     (b0, b1 : bExp)
     (s : state)
     (t0, t1 : bool)
     (evalbExp_ind b0 s t0) ->
     (evalbExp_ind b1 s t1) ->
     t0 = true \/ t1 = true ->  (evalbExp_ind (Or b0 b1) s true)
 | eval_And_true:
     (b0, b1 : bExp)
     (s : state)
     (evalbExp_ind b0 s true) ->
     (evalbExp_ind b1 s true) ->  (evalbExp_ind (aAnd b0 b1) s true)
 | eval_And_false:
     (b0, b1 : bExp)
     (s : state)
     (t0, t1 : bool)
     (evalbExp_ind b0 s t0) ->
     (evalbExp_ind b1 s t1) ->
     t0 = false \/ t1 = false ->  (evalbExp_ind (aAnd b0 b1) s false) .
 
Definition evalcom_rec_F : (com -> state ->  state) -> com -> state ->  state :=
   [evalcom_rec : com -> state ->  state]
   [c : com]
   [s : state]
    Cases c of
      Skip => s
     | (Assign v a) => (update_rec s v (evalaExp_rec a s))
     | (Scolon c1 c2) => (evalcom_rec c2 (evalcom_rec c1 s))
     | (IfThenElse b c1 c2) =>
         Cases (evalbExp_rec b s) of
         true => (evalcom_rec c1 s) | false => (evalcom_rec c2 s) end
     | (WhileDo b c) =>
         Cases (evalbExp_rec b s) of
           true => (evalcom_rec (WhileDo b c) (evalcom_rec c s))
          | false => s end
    end.
 
Inductive evalcom_ind : com -> state -> state ->  Prop :=
  eval_Skip: (s : state)  (evalcom_ind Skip s s)
 | eval_Assign:
     (s, s1 : state)
     (v, n : nat)
     (a : aExp)
     (evalaExp_ind a s n) ->
     (update_ind s v n s1) ->  (evalcom_ind (Assign v a) s s1)
 | eval_Scolon:
     (s1, s2, s3 : state)
     (c1, c2 : com)
     (evalcom_ind c1 s1 s2) ->
     (evalcom_ind c2 s2 s3) ->  (evalcom_ind (Scolon c1 c2) s1 s3)
 | eval_IfThenElse_true:
     (b : bExp)
     (s, s1 : state)
     (c1, c2 : com)
     (evalbExp_ind b s true) ->
     (evalcom_ind c1 s s1) ->  (evalcom_ind (IfThenElse b c1 c2) s s1)
 | eval_IfThenElse_false:
     (b : bExp)
     (s, s2 : state)
     (c1, c2 : com)
     (evalbExp_ind b s false) ->
     (evalcom_ind c2 s s2) ->  (evalcom_ind (IfThenElse b c1 c2) s s2)
 | eval_WhileDo_false:
     (b : bExp)
     (s : state)
     (c : com) (evalbExp_ind b s false) ->  (evalcom_ind (WhileDo b c) s s)
 | eval_WhileDo_true:
     (b : bExp)
     (c : com)
     (s, s1, s2 : state)
     (evalbExp_ind b s true) ->
     (evalcom_ind c s s2) ->
     (evalcom_ind (WhileDo b c) s2 s1) ->  (evalcom_ind (WhileDo b c) s s1) .
 
Fixpoint iter [A, B : Set; f : (A ->  B) -> A ->  B; k : nat] :
 (A ->  B) -> A ->  B :=
 [a : A ->  B]  Cases k of
                  O => a
                 | (S p) => (f [a' : A]  (iter A B f p a a'))
                end.
 
Theorem equality_update:
 (s1, s2 : state)
 (v, n : nat) (update_ind s1 v n s2) ->  (update_rec s1 v n) = s2.
Proof.
Intros s1 s2 v n H; Elim H.
Intros v0 n0.
Simpl.
Trivial.
Intros v0 n1 n2 s3.
Simpl.
Case (eq_nat_dec v0 v0).
Auto.
Intros Habs.
Absurd v0 = v0.
Assumption.
Trivial.
Intros v1 v2 n1 n2 s3 s4 H1 H2 H3.
Simpl.
Case (eq_nat_dec v1 v2).
Intros Habs.
Absurd v1 = v2; Assumption.
Intros H4.
Rewrite H3.
Trivial.
Qed.
 
Theorem equality_value:
 (n, n1 : nat) (s : state) (value_ind s n n1) ->  (value_rec s n) = n1.
Intros.
Elim H.
Simpl.
Auto.
Simpl.
Intros.
Case (eq_nat_dec v v).
Auto.
Intros.
Elim n2.
Auto.
Intros.
Simpl.
Case (eq_nat_dec v1 v).
Intros.
Elim H0.
Auto.
Intros.
Try Exact H2.
Qed.
Hints Resolve equality_value .
 
Theorem equality_aExp:
 (a : aExp)
 (s : state) (n : nat) (evalaExp_ind a s n) ->  (evalaExp_rec a s) = n.
Intros a s n H; Elim H; Simpl; Auto; Intros; Rewrite H3; Rewrite H4; Rewrite H1;
 Auto.
Qed.
 
Theorem equality_bExp:
 (b : bExp)
 (s : state) (t : bool) (evalbExp_ind b s t) ->  (evalbExp_rec b s) = t.
Intros.
Elim H.
Simpl.
Reflexivity.
Simpl.
Reflexivity.
Intros.
Simpl.
Rewrite equality_aExp with 1 := H0.
Rewrite equality_aExp with 1 := H1.
Rewrite H2.
Case (eq_nat_dec n1 n1).
Auto.
Intros.
Elim n.
Reflexivity.
Intros.
Simpl.
Rewrite equality_aExp with 1 := H0.
Rewrite equality_aExp with 1 := H1.
Case (eq_nat_dec n0 n1).
Intros.
Elim H2.
Apply e.
Intros n.
Reflexivity.
Intros a0 a1 n0 n1 s0 H0 H1 H2; Try Assumption.
Simpl.
Rewrite equality_aExp with 1 := H0.
Rewrite equality_aExp with 1 := H1.
Case (le_lt_dec n0 n1).
Auto.
Intros.
Elim le_not_lt with 1 := H2.
Exact l.
Intros.
Simpl.
Rewrite equality_aExp with 1 := H0.
Rewrite equality_aExp with 1 := H1.
Case (le_lt_dec n0 n1).
Intros.
Elim H2.
Exact l.
Intros.
Reflexivity.
Intros.
Simpl.
Rewrite H1.
Reflexivity.
Intros.
Simpl.
Rewrite H1.
Reflexivity.
Intros.
Simpl.
Rewrite H1.
Rewrite H3.
Reflexivity.
Intros.
Simpl.
Rewrite H1.
Rewrite H3.
Cut <bool> t0 = true \/ <bool> t1 = true.
Case t0.
Auto.
Case t1.
Auto.
Intros H5; (Elim H5; [Intros H6; Clear H5 | Intros H6; Clear H5; Try Exact H6]).
Auto.
Try Exact H4.
Intros.
Simpl.
Rewrite H3.
Rewrite H1.
Reflexivity.
Intros.
Simpl.
Rewrite H3.
Rewrite H1.
Cut <bool> t0 = false \/ <bool> t1 = false.
Case t1.
Case t0.
Intros H5; (Elim H5; [Intros H6; Clear H5 | Intros H6; Clear H5; Try Exact H6]).
Try Exact H6.
Intros.
Auto.
Case t0.
Auto.
Auto.
Auto.
Qed.
 
Theorem iter_plus_equal:
 (A, B : Set)
 (F : (A ->  B) -> A ->  B)
 (x : A ->  B)
 (k, k' : nat)  (iter A B F (plus k k') x) = (iter A B F k (iter A B F k' x)).
Intros A B F x k; Elim k; Auto.
Intros n H k'; Simpl.
Rewrite H; Auto.
Qed.
 
Theorem equality_com_ind2rec:
 (c : com)
 (s1, s2 : state)
 (evalcom_ind c s1 s2) ->
  (ex
   nat
   [k : nat]
   (evalcom_rec : com -> state ->  state)
    (iter com state ->  state evalcom_rec_F k evalcom_rec c s1) = s2).
Intros c s1 s2 H.
Elim H.
Intros.
Exists (S O).
Auto.
Intros.
Exists (S O).
Simpl.
Intros.
Rewrite equality_aExp with 1 := H0.
Apply equality_update with 1 := H1.
Intros.
Elim H1; Intros k H4; Clear H1; Try Exact H4.
Elim H3; Intros k0 H1; Clear H3; Try Exact H1.
Exists (plus (S O) (plus k k0)).
Intros evalcom_rec.
Simpl.
Pattern 1 (plus k k0); Rewrite plus_sym.
Rewrite (iter_plus_equal com state ->  state evalcom_rec_F evalcom_rec k k0).
Rewrite H4.
Rewrite (iter_plus_equal com state ->  state evalcom_rec_F evalcom_rec k0 k).
Rewrite H1.
Reflexivity.
Intros.
Elim H2; Intros k H3; Clear H2; Try Exact H3.
Exists (plus (S O) k).
Intros evalcom_rec.
Simpl.
Rewrite equality_bExp with 1 := H0.
Apply H3.
Intros.
Elim H2; Intros k H3; Clear H2; Try Exact H3.
Exists (plus (S O) k).
Intros evalcom_rec.
Simpl.
Rewrite equality_bExp with 1 := H0.
Apply H3.
Intros.
Exists (S O).
Intros evalcom_rec.
Simpl.
Rewrite equality_bExp with 1 := H0.
Reflexivity.
Intros.
Elim H2; Intros k H5; Clear H2; Try Exact H5.
Elim H4; Intros k0 H2; Clear H4; Try Exact H2.
Exists (S (plus k k0)).
Intros evalcom_rec.
Simpl.
Rewrite equality_bExp with 1 := H0.
Pattern 1 (plus k k0); Rewrite plus_sym.
Rewrite (iter_plus_equal com state ->  state evalcom_rec_F evalcom_rec k k0).
Rewrite H5.
Rewrite (iter_plus_equal com state ->  state evalcom_rec_F evalcom_rec k0 k).
Rewrite H2.
Reflexivity.
Qed.
 
Tactic Definition CaseEq f :=
 Generalize (refl_equal ? f); Pattern -1 f; Case f.
 
Inductive comAcc : com -> state -> nat -> (com -> state ->  state) ->  Prop :=
  accSkip:
    (s : state) (k : nat) (f : com -> state ->  state)  (comAcc Skip s (S k) f)
 | accAssign:
     (v : nat)
     (a : aExp)
     (s : state)
     (k : nat) (f : com -> state ->  state)  (comAcc (Assign v a) s (S k) f)
 | accScolon:
     (c1, c2 : com)
     (s : state)
     (k : nat)
     (f : com -> state ->  state)
     (comAcc c1 s k f) ->
     (comAcc c2 (iter com state ->  state evalcom_rec_F k f c1 s) k f) ->
      (comAcc (Scolon c1 c2) s (S k) f)
 | accIftrue:
     (b : bExp)
     (c1, c2 : com)
     (s : state)
     (k : nat)
     (f : com -> state ->  state)
     (evalbExp_ind b s true) ->
     (comAcc c1 s k f) ->  (comAcc (IfThenElse b c1 c2) s (S k) f)
 | accIffalse:
     (b : bExp)
     (c1, c2 : com)
     (s : state)
     (k : nat)
     (f : com -> state ->  state)
     (evalbExp_ind b s false) ->
     (comAcc c2 s k f) ->  (comAcc (IfThenElse b c1 c2) s (S k) f)
 | accWhiletrue:
     (b : bExp)
     (c : com)
     (s : state)
     (k : nat)
     (f : com -> state ->  state)
     (evalbExp_ind b s true) ->
     (comAcc c s k f) ->
     (comAcc (WhileDo b c) (iter com state ->  state evalcom_rec_F k f c s) k f) ->
      (comAcc (WhileDo b c) s (S k) f)
 | accWhilefalse:
     (b : bExp)
     (c : com)
     (s : state)
     (k : nat)
     (f : com -> state ->  state)
     (evalbExp_ind b s false) ->  (comAcc (WhileDo b c) s (S k) f) .
 
Definition comDom : com -> state ->  Set :=
   [c : com]
   [s : state]  {k : nat | (f : com -> state ->  state)  (comAcc c s k f)}.
 
Definition evalcom :
  (c : com) (s : state) (f : com -> state ->  state) (H : (comDom c s))  state :=
   [c : com]
   [s : state]
   [f : com -> state ->  state]
   [H : (comDom c s)]
    Cases H of
      (exist k G) => (iter com state ->  state evalcom_rec_F k f c s)
    end.
 
Theorem equality_update_2:
 (s1, s2 : state)
 (v, n : nat) (update_rec s1 v n) = s2 ->  (update_ind s1 v n s2).
Intros s1; Elim s1.
Simpl.
Intros s2 v n e; Rewrite <- e; Apply update_no_location.
Simpl.
Intros n n0 s H s2 v n1.
Case (eq_nat_dec n v).
Intros e H1; Rewrite <- e; Rewrite <- H1.
Apply update_first.
Auto.
Intros e H1; Rewrite <- H1.
Apply update_rest.
Exact e.
Apply H.
Auto.
Qed.
(* More useful in the following form. *)
 
Lemma update_ind_rec:
 (s : state) (v, n : nat)  (update_ind s v n (update_rec s v n)).
Proof.
Intros s v n.
Apply equality_update_2.
Trivial.
Qed.
 
Theorem equality_value_2:
 (s : state) (v : nat) (n : nat) (value_rec s v) = n ->  (value_ind s v n).
Intros s; Elim s.
Simpl.
Intros v n H; Rewrite <- H.
Apply no_such_location.
Simpl.
Intros n n0 s0 H v n1.
Case (eq_nat_dec n v).
Intros e0 e1; Rewrite <- e0; Rewrite <- e1.
Apply first.
Intros e H0.
Apply rest.
Auto.
Apply H; Exact H0.
Qed.
(* More useful in the following form. *)
 
Lemma value_ind_rec: (s : state) (v : nat)  (value_ind s v (value_rec s v)).
Proof.
Intros s v.
Apply equality_value_2.
Trivial.
Qed.
 
Theorem equality_aExp_2:
 (a : aExp)
 (s : state) (n : nat) (evalaExp_rec a s) = n ->  (evalaExp_ind a s n).
Intros a; Elim a.
Simpl.
Intros; Apply eval_Loc; Apply equality_value_2; Exact H.
Simpl.
Intros; Rewrite H; Apply eval_Num.
Simpl.
Intros.
Apply eval_Plus with n0 := (evalaExp_rec a0 s) n1 := (evalaExp_rec a1 s).
Apply H; Reflexivity.
Apply H0; Reflexivity.
Rewrite H1; Reflexivity.
Simpl.
Intros.
Apply eval_Minus with n0 := (evalaExp_rec a0 s) n1 := (evalaExp_rec a1 s).
Apply H; Reflexivity.
Apply H0; Reflexivity.
Rewrite H1; Reflexivity.
Simpl.
Intros.
Apply eval_Mult with n0 := (evalaExp_rec a0 s) n1 := (evalaExp_rec a1 s).
Apply H; Reflexivity.
Apply H0; Reflexivity.
Rewrite H1; Reflexivity.
Qed.
(* More useful in the following form. *)
 
Lemma evalaExp_ind_rec:
 (a : aExp) (s : state)  (evalaExp_ind a s (evalaExp_rec a s)).
Proof.
Intros a s.
Apply equality_aExp_2.
Trivial.
Qed.
 
Theorem equality_bExp_2:
 (b : bExp)
 (s : state) (t : bool) (evalbExp_rec b s) = t ->  (evalbExp_ind b s t).
Intros b; Elim b.
Simpl.
Intros.
Rewrite <- H; Apply eval_IMPtrue.
Simpl.
Intros.
Rewrite <- H; Apply eval_IMPfalse.
Simpl.
Intros a a0 s t.
Case (eq_nat_dec (evalaExp_rec a s) (evalaExp_rec a0 s)).
Intros e H; Rewrite <- H.
Apply eval_Equal with (evalaExp_rec a s) (evalaExp_rec a0 s).
Apply equality_aExp_2; Reflexivity.
Apply equality_aExp_2; Reflexivity.
Exact e.
Intros e H; Rewrite <- H.
Apply eval_UnEqual with (evalaExp_rec a s) (evalaExp_rec a0 s).
Apply equality_aExp_2; Reflexivity.
Apply equality_aExp_2; Reflexivity.
Exact e.
Simpl.
Intros a a0 s t.
Case (le_lt_dec (evalaExp_rec a s) (evalaExp_rec a0 s)).
Intros e H; Rewrite <- H.
Apply eval_LessEqual with (evalaExp_rec a s) (evalaExp_rec a0 s).
Apply equality_aExp_2; Reflexivity.
Apply equality_aExp_2; Reflexivity.
Exact e.
Intros e H; Rewrite <- H.
Apply eval_NotLessEqual with (evalaExp_rec a s) (evalaExp_rec a0 s).
Apply equality_aExp_2; Reflexivity.
Apply equality_aExp_2; Reflexivity.
Auto with arith.
Simpl.
Intros b0 H s.
Generalize (H s).
Case (evalbExp_rec b0 s).
Intros H1 t e; Rewrite <- e.
Apply eval_Not_true.
Apply H1; Reflexivity.
Intros H1 t e; Rewrite <- e.
Apply eval_Not_false.
Apply H1; Reflexivity.
Simpl.
Intros b0 H0 b1 H1 s t.
Generalize (H0 s).
Case (evalbExp_rec b0 s).
Intros H2 t1; Rewrite <- t1.
Apply eval_Or_true with true (evalbExp_rec b1 s).
Apply H2; Reflexivity.
Apply H1; Reflexivity.
Apply or_introl; Reflexivity.
Generalize (H1 s).
Case (evalbExp_rec b1 s).
Intros H2 H3 t1; Rewrite <- t1.
Apply eval_Or_true with false true.
Apply H3; Reflexivity.
Apply H2; Reflexivity.
Apply or_intror; Reflexivity.
Intros H2 H3 t1; Rewrite <- t1.
Apply eval_Or_false.
Apply H3; Reflexivity.
Apply H2; Reflexivity.
Simpl.
Intros b0 H0 b1 H1 s t.
Generalize (H0 s).
Case (evalbExp_rec b0 s).
Generalize (H1 s).
Case (evalbExp_rec b1 s).
Intros H2 H3 t1; Rewrite <- t1.
Apply eval_And_true.
Apply H3; Reflexivity.
Apply H2; Reflexivity.
Intros H2 H3 t1; Rewrite <- t1.
Apply eval_And_false with true false.
Apply H3; Reflexivity.
Apply H2; Reflexivity.
Apply or_intror; Reflexivity.
Intros H2 t1; Rewrite <- t1.
Apply eval_And_false with false (evalbExp_rec b1 s).
Apply H2; Reflexivity.
Apply H1; Reflexivity.
Apply or_introl; Reflexivity.
Qed.
(* More useful in the following form. *)
 
Lemma evalbExp_ind_rec:
 (b : bExp) (s : state)  (evalbExp_ind b s (evalbExp_rec b s)).
Proof.
Intros b s.
Apply equality_bExp_2.
Trivial.
Qed.
 
Theorem comAcc_evalcom_ind:
 (c : com)
 (s : state)
 (k : nat)
 (f : com -> state ->  state)
 (comAcc c s k f) ->
  (evalcom_ind c s (iter com state ->  state evalcom_rec_F k f c s)).
Intros c s k f H; Elim H.
Intros.
Simpl.
Apply eval_Skip.
Intros; Simpl.
Apply eval_Assign with n := (evalaExp_rec a s0).
Apply evalaExp_ind_rec.
Apply update_ind_rec.
Intros c1 c2 s0 k0 f0 Hc1 IHc1 Hc2 IHc2.
Apply eval_Scolon
     with s2 := (iter com state ->  state evalcom_rec_F k0 f0 c1 s0).
Apply IHc1.
Apply IHc2.
Intros b c1 c2 s0 k0 f0 Hbtrue Hc1 IHc1.
Apply eval_IfThenElse_true.
Assumption.
Simpl.
Cut (evalbExp_rec b s0) = true.
Intros Hb_rec; Rewrite Hb_rec.
Assumption.
Apply equality_bExp.
Assumption.
Intros b c1 c2 s0 k0 f0 Hbfalse Hc2 IHc2.
Apply eval_IfThenElse_false.
Assumption.
Simpl.
Cut (evalbExp_rec b s0) = false.
Intros Hb_rec; Rewrite Hb_rec.
Assumption.
Apply equality_bExp.
Assumption.
Intros b c0 s0 k0 f0 Hbtrue Hc0 IHc0 HWhile IHWhile.
Apply eval_WhileDo_true
     with s2 := (iter com state ->  state evalcom_rec_F k0 f0 c0 s0).
Assumption.
Assumption.
Simpl.
Cut (evalbExp_rec b s0) = true.
Intros Hb_rec; Rewrite Hb_rec.
Assumption.
Apply equality_bExp.
Assumption.
Intros b c0 s0 k0 f0 Hbfalse.
Simpl.
Cut (evalbExp_rec b s0) = false.
Intros Hb_rec; Rewrite Hb_rec.
Apply eval_WhileDo_false.
Assumption.
Apply equality_bExp.
Assumption.
Qed.
 
Theorem evalcom_correctness:
 (c : com)
 (s : state)
 (f : com -> state ->  state)
 (h : (comDom c s))  (evalcom_ind c s (evalcom c s f h)).
Intros c s f h.
Red in h.
Elim h.
Intros k Hf.
Simpl.
Apply comAcc_evalcom_ind.
Apply Hf.
Qed.
 
Theorem equality_com_rec2ind:
 (c : com)
 (s1, s2 : state)
 (f : com -> state ->  state)
 (H : (comDom c s1)) (evalcom c s1 f H) = s2 ->  (evalcom_ind c s1 s2).
Intros c s1 s2 f H Heq.
Rewrite <- Heq.
Apply evalcom_correctness.
Qed.
 
Theorem evalcom_ind_converge:
 (c : com)
 (s1 : state)
 (s2 : state)
 (evalcom_ind c s1 s2) -> (s3 : state) (evalcom_ind c s1 s3) ->  s2 = s3.
Intros c s1 s2 H_ind s3 H_ind'.
Elim (equality_com_ind2rec c s1 s2); Auto.
Intros k1 Heq1.
Elim (equality_com_ind2rec c s1 s3); Auto.
Intros k2 Heq2.
Rewrite <- Heq2 with evalcom_rec :=
                     (iter com state ->  state evalcom_rec_F k1 [c, s : ?]  s).
Rewrite <- Heq1 with evalcom_rec :=
                     (iter com state ->  state evalcom_rec_F k2 [c, s : ?]  s).
Repeat Rewrite <- iter_plus_equal.
Rewrite plus_sym; Auto.
Qed.
 
Theorem equality_com_ind2rec_1:
 (c : com)
 (s1, s2 : state)
 (f : com -> state ->  state)
 (evalcom_ind c s1 s2) -> (H : (comDom c s1))  (evalcom c s1 f H) = s2.
Intros c s1 s2 f Hyp1 Hyp2.
Apply evalcom_ind_converge
     with c := c s1 := s1 s2 := (evalcom c s1 f Hyp2) s3 := s2.
Apply evalcom_correctness.
Try Exact Hyp1.
Qed.
 
Theorem iteration_stability:
 (c : com)
 (s : state)
 (f : com -> state ->  state)
 (k1 : nat)
 (comAcc c s k1 f) ->
 (g : com -> state ->  state)
 (k2 : nat)
 (le k1 k2) ->
  (iter com state ->  state evalcom_rec_F k1 f c s) =
  (iter com state ->  state evalcom_rec_F k2 g c s).
Intros c s f k1 Hcom; Elim Hcom.
Intros s0 k f0 g k2; Case k2.
Intros Hle; Inversion Hle.
Auto.
Intros v a s0 k f0 g k2; Case k2.
Intros Hle; Inversion Hle.
Auto.
Intros c1 c2 s0 k f0 H Hrec0 H1 Hrec1 g k2.
Case k2.
Intros Hle; Inversion Hle.
Intros k3 Hle.
Simpl.
Rewrite <- Hrec0 with k2 := k3.
Apply Hrec1.
Apply le_S_n; Auto.
Apply le_S_n; Auto.
Intros b c1 c2 s0 k f0 H H0 Hrec g k2.
Case k2.
Intros Hle; Inversion Hle.
Intros k3.
Intros Hle; Simpl.
Rewrite equality_bExp with 1 := H.
Apply Hrec; Apply le_S_n; Auto.
Intros b c1 c2 s0 k f0 H H0 Hrec g k2.
Case k2.
Intros Hle; Inversion Hle.
Intros k3.
Intros Hle; Simpl.
Rewrite equality_bExp with 1 := H.
Apply Hrec; Apply le_S_n; Auto.
Intros b c0 s0 k f0 H H0 Hrec0 H2 Hrec1 g k2.
Case k2.
Intros Hle; Inversion Hle.
Intros k3.
Intros Hle; Simpl.
Rewrite equality_bExp with 1 := H.
Rewrite <- Hrec0 with k2 := k3.
Apply Hrec1.
Apply le_S_n; Auto.
Apply le_S_n; Auto.
Intros b c0 s0 k f0 H g k2.
Case k2.
Intros Hle; Inversion Hle.
Intros k3.
Intros Hle; Simpl.
Rewrite equality_bExp with 1 := H.
Auto.
Qed.
 
Theorem comAcc_converge:
 (k, k1 : nat)
 (c : com)
 (s : state)
 (f : com -> state ->  state)
 (le k1 k) -> (comAcc c s k1 f) ->  (comAcc c s k f).
Intros k k1 c s f Hyp1 Hyp2; Elim Hyp1.
Try Exact Hyp2.
Intros.
Elim H0.
Intros.
Apply accSkip.
Intros v a s0 k0 f0.
Apply accAssign.
Intros c1 c2 s0 k0 f0 Hyp3 Hyp4 Hyp5 Hyp6.
Apply accScolon.
Try Exact Hyp4.
Cut (le k0 (S k0)).
Intros Hle.
Rewrite (iteration_stability c1 s0 f0 k0 Hyp3 f0 (S k0) Hle) in Hyp6.
Try Exact Hyp6.
Apply le_n_Sn.
Intros b c1 c2 s0 k0 f0 Hyp3 Hyp4 Hyp5.
Apply accIftrue.
Try Exact Hyp3.
Try Exact Hyp5.
Intros b c1 c2 s0 k0 f0 Hyp3 Hyp4 Hyp5.
Apply accIffalse.
Try Exact Hyp3.
Try Exact Hyp5.
Intros b c0 s0 k0 f0 Hyp3 Hyp4 Hyp5 Hyp6 Hyp7.
Apply accWhiletrue.
Try Exact Hyp3.
Try Exact Hyp5.
Cut (le k0 (S k0)).
Intros Hle.
Rewrite (iteration_stability c0 s0 f0 k0 Hyp4 f0 (S k0) Hle) in Hyp7.
Try Exact Hyp7.
Apply le_n_Sn.
Intros b c0 s0 k0 f0 Hyp3.
Apply accWhilefalse.
Try Exact Hyp3.
Qed.
 
Theorem equality_com_ind2rec_2:
 (c : com)
 (s1, s2 : state)
 (f : com -> state ->  state)
 (evalcom_ind c s1 s2) ->
  (ex (comDom c s1) [H : (comDom c s1)]  (evalcom c s1 f H) = s2).
Intros c s1 s2 f Hyp1.
Elim Hyp1.
Intros.
Cut (comDom Skip s).
Intros E.
Exists E.
Apply equality_com_ind2rec_1.
Apply eval_Skip.
Unfold comDom.
Exists (S O).
Intros.
Apply accSkip with f := f0.
Intros s s3 v n a Hyp2 Hyp3.
Cut (comDom (Assign v a) s).
Intros E.
Exists E.
Apply equality_com_ind2rec_1.
Apply eval_Assign with n := n.
Try Exact Hyp2.
Try Exact Hyp3.
Unfold comDom.
Exists (S O).
Intros.
Apply accAssign with f := f0.
Intros s3 s4 s5 c1 c2 Hyp2 Hyp3 Hyp4 Hyp5.
Case Hyp5.
Intros Hc2 eqc2.
Case Hyp3.
Intros Hc1.
Red in Hc1; Red in Hc2.
Case Hc1; Intros k1 Hacc1 eqc1.
Simpl in eqc1.
Case Hc2; Intros k2 Hacc2.
Cut (comDom (Scolon c1 c2) s3).
Intros E.
Exists E.
Apply equality_com_ind2rec_1.
Apply eval_Scolon with s2 := s4.
Try Exact Hyp2.
Try Exact Hyp4.
Unfold comDom.
Exists (S (plus k1 k2)).
Intros.
Simpl.
Apply accScolon with f := f0.
Apply comAcc_converge with k := (plus k1 k2) k1 := k1 c := c1 s := s3 f := f0.
Apply le_plus_l.
Generalize (Hacc1 f0); Intros H; Try Exact H.
Apply comAcc_converge
     with
      k := (plus k1 k2) k1 := k2 c := c2
      s := (iter com state ->  state evalcom_rec_F (plus k1 k2) f0 c1 s3)
      f := f0.
Apply le_plus_r.
Generalize (iteration_stability c1 s3 f k1).
Intros HH.
Generalize (HH (Hacc1 f) f0 (plus k1 k2)).
Intros Hle.
Cut (le k1 (plus k1 k2)).
Intros leK.
Rewrite <- (Hle leK).
Rewrite eqc1.
Generalize (Hacc2 f0); Intros H; Try Exact H.
Apply le_plus_l.
Intros b s s3 c1 c2 Hyp2 Hyp3 Hyp4.
Case Hyp4.
Intros Hc1.
Red in Hc1.
Case Hc1.
Intros k c0 eqc1.
Cut (comDom (IfThenElse b c1 c2) s).
Intros E; Exists E.
Apply equality_com_ind2rec_1.
Apply eval_IfThenElse_true.
Try Exact Hyp2.
Try Exact Hyp3.
Unfold comDom.
Exists (S k).
Intros f0.
Apply accIftrue with f := f0.
Try Exact Hyp2.
Apply (c0 f0).
Intros b s s3 c1 c2 Hyp2 Hyp3 Hyp4.
Case Hyp4.
Intros Hc2.
Red in Hc2.
Case Hc2; Intros k c0 eqc2.
Cut (comDom (IfThenElse b c1 c2) s).
Intros E; Exists E.
Apply equality_com_ind2rec_1.
Apply eval_IfThenElse_false.
Try Exact Hyp2.
Try Exact Hyp3.
Unfold comDom.
Exists (S k).
Intros f0.
Apply accIffalse with f := f0.
Try Exact Hyp2.
Apply (c0 f0).
Intros b s c0 Hyp2.
Cut (comDom (WhileDo b c0) s).
Intros E; Exists E.
Apply equality_com_ind2rec_1.
Apply eval_WhileDo_false.
Try Exact Hyp2.
Unfold comDom.
Exists (S O).
Intros f0; Apply accWhilefalse with f := f0.
Try Exact Hyp2.
Intros b c0 s s3 s4 Hyp2 Hyp3 Hyp4 Hyp5 Hyp6.
Case Hyp4.
Intros Hc0.
Case Hyp6.
Intros HWhile eqWhile.
Red in Hc0; Red in HWhile.
Case Hc0.
Intros k Hacc0 eqc0.
Simpl in eqc0.
Case HWhile.
Intros k1 HaccWhile.
Cut (comDom (WhileDo b c0) s).
Intros E; Exists E.
Apply equality_com_ind2rec_1.
Apply eval_WhileDo_true with s2 := s4.
Try Exact Hyp2.
Try Exact Hyp3.
Try Exact Hyp5.
Unfold comDom.
Exists (S (plus k k1)).
Intros f0.
Apply accWhiletrue with f := f0.
Try Exact Hyp2.
Apply comAcc_converge with k := (plus k k1) k1 := k c := c0 s := s f := f0.
Apply le_plus_l.
Apply (Hacc0 f0).
Apply comAcc_converge
     with
      k := (plus k k1) k1 := k1 c := (WhileDo b c0)
      s := (iter com state ->  state evalcom_rec_F (plus k k1) f0 c0 s) f := f0.
Apply le_plus_r.
Generalize (iteration_stability c0 s f k).
Intros HH.
Generalize (HH (Hacc0 f) f0 (plus k k1)).
Intros Hle.
Cut (le k (plus k k1)).
Intros leK.
Rewrite <- (Hle leK).
Rewrite eqc0.
Generalize (HaccWhile f0); Intros H; Try Exact H.
Apply le_plus_l.
Qed.
 
Theorem Yves's_strange_idea:
 (c : com)
 (s1, s2 : state)
 (f : com -> state ->  state)
 (H, H' : (comDom c s1))  (evalcom c s1 f H) = (evalcom c s1 f H').
Intros c s1 s2 f H H'.
Generalize (evalcom_correctness c s1 f H).
Intros H_ind.
Apply equality_com_ind2rec_1.
Apply evalcom_correctness.
Qed.