Changeset 3538

Timestamp:

Mar 16, 2015, 7:01:08 PM (6 years ago)

Author:

pellitta

Message:

 

File:

• LTS/imp.ma (modified) (8 diffs)

LTS/imp.ma

@@ -17 +17 @@
 include "basics/bool.ma".
 include "Language.ma".
+include "basics/finset.ma".
 
 (* Tools *)
@@ -34 +35 @@
 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
 #b #b' cases b normalize #H destruct % qed.
-
-let rec neqb n m ≝ 
-match n with 
-  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
-  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
-  ].
-  
-axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
-
-definition DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq.
-
-lemma neqb_refl:∀n.neqb n n=true.
-#n elim n [%|#n' normalize * %]qed.
-
-lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
-#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
-% qed.
 
 (* Syntax *)
@@ -67 +51 @@
 
 let rec expr_eq (e1:expr) (e2:expr):bool≝
-match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
-|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
+match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2|_⇒ false]
+|Const v1⇒ match e2 with [Const v2⇒ v1==v2|_⇒ false]
 |Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
 |Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
@@ -74 +58 @@
 
 lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
-#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ * %
+#e elim e [1,2: #v change with (v==v = true); @(\b ?) %
 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
 
 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
 #e1 #e2 % [2:* lapply e2 -e2 elim e1
-  [1,2:#n #_ normalize >neqb_refl %
+  [1,2:#n #_ change with (n==n = true) @(\b ?) %
   |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]
 |lapply e2 -e2 elim e1
-  [1,2: #v1 #e2 cases e2 normalize
-    [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ %
-    |3,4,7,8: #e #f #ABS destruct]
+  [1,2: #v1 #e2 cases e2
+    [1,6: #v2 #H >(\P H) %
+    |2,5: #v2 #H normalize in H; destruct
+    |3,4,7,8: #e #f normalize #ABS destruct]
   |3,4: #e #e2 #H #K #f cases f 
     [1,2,5,6: #v2 normalize #ABS destruct
@@ -93 +78 @@
 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
  sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
-|sAss ⇒ match s2 with [sAss ⇒ true| _⇒ false]
-|sInc ⇒ match s2 with [sInc ⇒ true| _⇒ false]
+|sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false]
+|sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false]
 ].
-lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2
-cases s1 cases s2 normalize % #H destruct % qed.
-
-inductive io_i:Type[0]≝.
-definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true.
-lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2
-cases i1 qed.
-
-(*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
-axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*)
-lemma neqb_refl:∀n.neqb n n=true.
-#n elim n [%|#n' normalize * %]qed.
-lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
-#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
-% qed.
+
+lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
+#s cases s try(#v) try(#e) try %
+[ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
+| change with (v==v = true); >(\b ?) %] qed.
+
+lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
+#s1 #s2 % [2: * elim s1 [2,3:#v try(#e)] @seq_i_eq_refl
+|lapply s2 -s2 elim s1 [2,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5: #e']
+[2,3,4,6,7,8: normalize #H destruct
+|1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct]
+ #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_
+ >(proj1 … (expr_eq_equality …) H) >(\P EQ) %
+|5: #H >(\P H) %
+| // ]
+qed.
 
 definition cond_i:Type[0]≝condition.
-let rec expr_eq (e1:expr) (e2:expr):bool≝
-match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
-|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
-|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
-|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
-].
+
 let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
 match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ 
@@ -124 +105 @@
 |Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
 
-lemma expr_eq_aux:∀e:expr.expr_eq e e=true.
-#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_refl
-|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
-
-
-lemma expr_eq_plus:∀e1,e2,f1,f2:expr.expr_eq (Plus e1 e2) (Plus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true).
-#e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
-|inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
-
-lemma expr_eq_minus:∀e1,e2,f1,f2:expr.expr_eq (Minus e1 e2) (Minus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true).
-#e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
-|inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
-
-
-lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2.
-#e1 elim e1
-[1,2: #v1 * normalize
-  [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) #A destruct >(A H) %
-  |3,4,7,8: #e #f #ABS destruct]
-|3,4: #e * 
-  [1,2,5: #v2 #H #K * [1,2,5,6,9,10:#n #ABS normalize in ABS; destruct
-  |3,4,7,8,11,12:#f1 #f2 #T [2,4,5: normalize in T; destruct|1,3,6: >(H f1) >(K f2)
-  [1,5,9:%  
-  |2,4,10,12: inversion(f2) [2,6,10,14:#n #Hf2 >Hf2 in T; 
-  inversion(expr_eq e f1) #Heqef1 normalize >Heqef1 normalize #ABS destruct(ABS)
-  |3,4,7,8,11,12,15,16:#f1 #f2 #_ #H1 #H2 
-  >H2 in T; normalize >ifthenelse_aux * %
-  |1,5,9,13:#v #H2 >H2 in T; normalize #Hite >(ifthenelse_mm (expr_eq e f1) (neqb v2 v))
-[1,3,5,7:%|2,4,6,8:assumption]]
-|3:lapply(expr_eq_plus e (Var v2) f1 f2)|6,7,8:lapply(expr_eq_plus e (Const v2) f1 f2)
-|11:lapply(expr_eq_minus e (Var v2) f1 f2)]* try(#H1 #H2) assumption]]
-|6:#n #H #K #f cases f [1,2:#k|3,4:#f1 #f2] #T normalize in T; destruct(T)
->(K f2) [>(H f1) [%|inversion (expr_eq e f1) #II try(%) >II in T; #ABS normalize in ABS; destruct]
-|inversion(f2) [#v #IHf >IHf in T; normalize >ifthenelse_aux * %
-|#v #IHf >IHf in T; normalize inversion(neqb n v) #IHnenv #T try (%) >ifthenelse_aux in T; * %
-|3,4: #g1 #g2 #Hg1 #Hg2 #Hf2 >Hf2 in T; normalize >ifthenelse_aux * %]]
-|3,4,7,8:#f1 #f2 #H #K * [1,2,5,6,9,10:#n #T normalize in T; destruct
-|3,4,7,8,9,11,12,15,16: #g1 #g2|13,14:#n] #T normalize in T; destruct
->(H g1) [1,3,5: >(K g2) [1,3,5:%|2,4,6: /2 by sym_eq, ifthenelse_mm/]
-|2,4,6,8: /2 by ifthenelse_mm2/|7:>(K g2) [%|/2 by ifthenelse_mm/ qed.
-
-lemma expr_eq_equality_two:∀e1,e2.e1=e2→ expr_eq e1 e2=true.
-#e1 #e2 * elim e1 [1,2:#n normalize >neqb_refl %|3,4:#f1 #f2 normalize
-#H1 >H1 #H2 >H2 normalize %]qed.
-
-lemma expr_eq_equality:∀e1,e2.expr_eq e1 e2=true ↔ e1=e2.
-#e1 #e2 % [@expr_eq_equality_one|@expr_eq_equality_two] qed.
-
 (*
-lemma expr_eq_equality_two':∀e1,e2.e1≠e2→ expr_eq e1 e2=false.
-#e1 #e2 * lapply e2 -e2 #e2 elim e1 [1,2:#n normalize /3 by _/|3,4:#f1 #f2 normalize
-#H1 >H1 #H2 >H2 normalize %]qed.
-*)
-lemma expr_eq_refl:∀e.expr_eq e e=true.
-#e >expr_eq_equality_two % qed.
-
 lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1.
-#e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' normalize >neqb_sym %
+#e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' try % 
+ change with (n==n' = (n'==n)) inversion (n==n') #H
+ [ lapply(\P H) // | 
 |#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize %
 |#n normalize //]
 |3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) %
-|4,7:#_ #_ %] qed.
-
-(*
-
-lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
-#e1 elim e1
-[ #v1 *
-  [ #v2 normalize % #H cases (neqb_true_to_eq v1 v2) #H1 #H2
-    >H1 // destruct /2/
-  | #c normalize % #H destruct
-  |*: cases daemon ]
-|
-| #e1 #e2 #IH1 #IH2 *
-  [3: #f1 #f2 normalize %
-      [ inversion (expr_eq e1 f1) normalize #H1 #H2 [2: destruct ]
-        cases (IH1 f1) cases (IH2 f2) /4 by eq_f2, sym_eq/
-      | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4
-        >H4/2 by /
-*)      
-
-lemma condition_eq_sym:∀c:condition.cond_i_eq c c=true.
-#c elim c [#e #f normalize >expr_eq_aux >expr_eq_aux normalize %
+|4,7:#_ #_ %] qed. *)
+
+lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
+#c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl normalize %
 |#c' normalize * %] qed.
 
 lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
-#c1 #c2 % [2: * @condition_eq_sym
-| lapply c2 -c2 elim c1 normalize
-  [ #e1 #e2 * normalize
-    [ #f1 #f2 inversion(expr_eq f1 e1) normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize
-#H destruct [1,2:>(neqb_true_to_eq n2 n1 H) cases f2 cases e2
-[1,2,5,6,17,18,21,22:#k1 #k2 >neqb_refl normalize #K destruct >(neqb_true_to_eq k1 k2 K) %
-|3,4,7,8,11,12,15,16,19,20,23,24,27,28,31,32:#g1 #g2 [1,2,3,4,9,10,11,12:#n normalize
-#ABS destruct|5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct
-|1,4,5,6,7,8: inversion(expr_eq h1 g1) #INV1 >INV1 normalize #INV2 destruct
--c1 try(-c2) -e1 -e2 -f1 -f2 -H >INV1 in INV2; >neqb_refl >INV1 normalize
-#INV2 >expr_eq_sym in INV1; #INV1 >INV1 in INV2; normalize #INV2 >expr_eq_sym in INV1;
-#INV1 destruct >(expr_eq_equality_one g2 h2 INV2) >expr_eq_sym in INV1; #INV1
->(expr_eq_equality_one g1 h1 INV1) %] >neqb_refl in ABS; normalize #ABS destruct]
->neqb_refl in ABS; normalize #ABS destruct
-|9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS >neqb_refl in ABS; normalize #ABS destruct]
-|3,4,5,6:#ABS destruct >neqb_sym in H; #H >H in ABS; normalize #ABS destruct]
-|9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS1 #ABS2 destruct
-|11,12,15,16,27,28,31,32:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1)
-#INV1 >INV1 normalize #INV2 #E destruct >INV1 in E; normalize #E >expr_eq_sym in INV1; #INV1; >INV1 in E;
-normalize #E destruct >expr_eq_sym in INV1; #INV1 >(expr_eq_equality_one h1 g1 INV1)
->expr_eq_sym in INV2; #INV2 >INV2 in E; normalize #E destruct >expr_eq_sym in INV2; #INV2
->(expr_eq_equality_one h2 g2 INV2) >expr_eq_sym in E; #E >(expr_eq_equality_one f2 e2 E) %
-]#f1 #f2 #n normalize #ABS1 #ABS2 destruct
-|#c2 #ABS destruct]|#c2 #H #c' cases c' [#e1 #e2 normalize #ABS destruct|#c3 normalize #K
->(H c3 K) % qed.
-
-
-(*
-inductive cond_i:Type[0]≝cIfThenElse: cond_i.
-definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true.
-lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2
-cases c1 cases c2 % #_ % qed.
-*)
+#c1 #c2 % [2: * // ]
+lapply c2 -c2 elim c1 [ #e1 #e2 *
+[ #f1 #f2 whd in ⊢ (??%? → ?);
+  inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1
+  >(proj1 … (expr_eq_equality …) … H1)
+  inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 #_
+  >(proj1 … (expr_eq_equality …) … H2) %
+| normalize #c #H destruct
+]| #c2 #IH *
+[ normalize #e1 #e2 #H destruct
+| #c3 #H >(IH … H) % ]]
+qed.
 
 inductive loop_i:Type[0]≝lWhile: loop_i.
@@ -248 +137 @@
 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
 cases l1 cases l2 % #_ % qed.
+
+definition io_i ≝ False.
+
+definition io_i_eq ≝ λi1,i2:False. true.
+
+lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
 
 (*
@@ -336 +231 @@
 
 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
-normalize #s inversion(s) #INV #env [@(Some ? n)|@(Some ? n)|@(Some ? (S n))]qed.
+normalize * [| 2: #v #e |3: #v ] #env [@(Some ? env)|@(Some ? n)|@(Some ? (S n))]qed.
 
 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.