Changeset 3538 for LTS/imp.ma


Ignore:
Timestamp:
Mar 16, 2015, 7:01:08 PM (5 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3536 r3538  
    1717include "basics/bool.ma".
    1818include "Language.ma".
     19include "basics/finset.ma".
    1920
    2021(* Tools *)
     
    3435lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
    3536#b #b' cases b normalize #H destruct % qed.
    36 
    37 let rec neqb n m ≝
    38 match n with
    39   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
    40   | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
    41   ].
    42  
    43 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
    44 
    45 definition DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq.
    46 
    47 lemma neqb_refl:∀n.neqb n n=true.
    48 #n elim n [%|#n' normalize * %]qed.
    49 
    50 lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
    51 #n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
    52 % qed.
    5337
    5438(* Syntax *)
     
    6751
    6852let rec expr_eq (e1:expr) (e2:expr):bool≝
    69 match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
    70 |Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
     53match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2|_⇒ false]
     54|Const v1⇒ match e2 with [Const v2⇒ v1==v2|_⇒ false]
    7155|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    7256|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
     
    7458
    7559lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
    76 #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ * %
     60#e elim e [1,2: #v change with (v==v = true); @(\b ?) %
    7761|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    7862
    7963lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
    8064#e1 #e2 % [2:* lapply e2 -e2 elim e1
    81   [1,2:#n #_ normalize >neqb_refl %
     65  [1,2:#n #_ change with (n==n = true) @(\b ?) %
    8266  |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]
    8367|lapply e2 -e2 elim e1
    84   [1,2: #v1 #e2 cases e2 normalize
    85     [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ %
    86     |3,4,7,8: #e #f #ABS destruct]
     68  [1,2: #v1 #e2 cases e2
     69    [1,6: #v2 #H >(\P H) %
     70    |2,5: #v2 #H normalize in H; destruct
     71    |3,4,7,8: #e #f normalize #ABS destruct]
    8772  |3,4: #e #e2 #H #K #f cases f
    8873    [1,2,5,6: #v2 normalize #ABS destruct
     
    9378definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
    9479 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
    95 |sAss ⇒ match s2 with [sAss ⇒ true| _⇒ false]
    96 |sInc ⇒ match s2 with [sInc ⇒ true| _⇒ false]
     80|sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false]
     81|sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false]
    9782].
    98 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2
    99 cases s1 cases s2 normalize % #H destruct % qed.
    100 
    101 inductive io_i:Type[0]≝.
    102 definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true.
    103 lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2
    104 cases i1 qed.
    105 
    106 (*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
    107 axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*)
    108 lemma neqb_refl:∀n.neqb n n=true.
    109 #n elim n [%|#n' normalize * %]qed.
    110 lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
    111 #n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
    112 % qed.
     83
     84lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
     85#s cases s try(#v) try(#e) try %
     86[ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
     87| change with (v==v = true); >(\b ?) %] qed.
     88
     89lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
     90#s1 #s2 % [2: * elim s1 [2,3:#v try(#e)] @seq_i_eq_refl
     91|lapply s2 -s2 elim s1 [2,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5: #e']
     92[2,3,4,6,7,8: normalize #H destruct
     93|1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct]
     94 #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_
     95 >(proj1 … (expr_eq_equality …) H) >(\P EQ) %
     96|5: #H >(\P H) %
     97| // ]
     98qed.
    11399
    114100definition cond_i:Type[0]≝condition.
    115 let rec expr_eq (e1:expr) (e2:expr):bool≝
    116 match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
    117 |Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
    118 |Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    119 |Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    120 ].
     101
    121102let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
    122103match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒
     
    124105|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
    125106
    126 lemma expr_eq_aux:∀e:expr.expr_eq e e=true.
    127 #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_refl
    128 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    129 
    130 
    131 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).
    132 #e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
    133 |inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
    134 
    135 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).
    136 #e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
    137 |inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
    138 
    139 
    140 lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2.
    141 #e1 elim e1
    142 [1,2: #v1 * normalize
    143   [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) #A destruct >(A H) %
    144   |3,4,7,8: #e #f #ABS destruct]
    145 |3,4: #e *
    146   [1,2,5: #v2 #H #K * [1,2,5,6,9,10:#n #ABS normalize in ABS; destruct
    147   |3,4,7,8,11,12:#f1 #f2 #T [2,4,5: normalize in T; destruct|1,3,6: >(H f1) >(K f2)
    148   [1,5,9:% 
    149   |2,4,10,12: inversion(f2) [2,6,10,14:#n #Hf2 >Hf2 in T;
    150   inversion(expr_eq e f1) #Heqef1 normalize >Heqef1 normalize #ABS destruct(ABS)
    151   |3,4,7,8,11,12,15,16:#f1 #f2 #_ #H1 #H2
    152   >H2 in T; normalize >ifthenelse_aux * %
    153   |1,5,9,13:#v #H2 >H2 in T; normalize #Hite >(ifthenelse_mm (expr_eq e f1) (neqb v2 v))
    154 [1,3,5,7:%|2,4,6,8:assumption]]
    155 |3:lapply(expr_eq_plus e (Var v2) f1 f2)|6,7,8:lapply(expr_eq_plus e (Const v2) f1 f2)
    156 |11:lapply(expr_eq_minus e (Var v2) f1 f2)]* try(#H1 #H2) assumption]]
    157 |6:#n #H #K #f cases f [1,2:#k|3,4:#f1 #f2] #T normalize in T; destruct(T)
    158 >(K f2) [>(H f1) [%|inversion (expr_eq e f1) #II try(%) >II in T; #ABS normalize in ABS; destruct]
    159 |inversion(f2) [#v #IHf >IHf in T; normalize >ifthenelse_aux * %
    160 |#v #IHf >IHf in T; normalize inversion(neqb n v) #IHnenv #T try (%) >ifthenelse_aux in T; * %
    161 |3,4: #g1 #g2 #Hg1 #Hg2 #Hf2 >Hf2 in T; normalize >ifthenelse_aux * %]]
    162 |3,4,7,8:#f1 #f2 #H #K * [1,2,5,6,9,10:#n #T normalize in T; destruct
    163 |3,4,7,8,9,11,12,15,16: #g1 #g2|13,14:#n] #T normalize in T; destruct
    164 >(H g1) [1,3,5: >(K g2) [1,3,5:%|2,4,6: /2 by sym_eq, ifthenelse_mm/]
    165 |2,4,6,8: /2 by ifthenelse_mm2/|7:>(K g2) [%|/2 by ifthenelse_mm/ qed.
    166 
    167 lemma expr_eq_equality_two:∀e1,e2.e1=e2→ expr_eq e1 e2=true.
    168 #e1 #e2 * elim e1 [1,2:#n normalize >neqb_refl %|3,4:#f1 #f2 normalize
    169 #H1 >H1 #H2 >H2 normalize %]qed.
    170 
    171 lemma expr_eq_equality:∀e1,e2.expr_eq e1 e2=true ↔ e1=e2.
    172 #e1 #e2 % [@expr_eq_equality_one|@expr_eq_equality_two] qed.
    173 
    174107(*
    175 lemma expr_eq_equality_two':∀e1,e2.e1≠e2→ expr_eq e1 e2=false.
    176 #e1 #e2 * lapply e2 -e2 #e2 elim e1 [1,2:#n normalize /3 by _/|3,4:#f1 #f2 normalize
    177 #H1 >H1 #H2 >H2 normalize %]qed.
    178 *)
    179 lemma expr_eq_refl:∀e.expr_eq e e=true.
    180 #e >expr_eq_equality_two % qed.
    181 
    182108lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1.
    183 #e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' normalize >neqb_sym %
     109#e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' try %
     110 change with (n==n' = (n'==n)) inversion (n==n') #H
     111 [ lapply(\P H) // |
    184112|#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize %
    185113|#n normalize //]
    186114|3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) %
    187 |4,7:#_ #_ %] qed.
    188 
    189 (*
    190 
    191 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
    192 #e1 elim e1
    193 [ #v1 *
    194   [ #v2 normalize % #H cases (neqb_true_to_eq v1 v2) #H1 #H2
    195     >H1 // destruct /2/
    196   | #c normalize % #H destruct
    197   |*: cases daemon ]
    198 |
    199 | #e1 #e2 #IH1 #IH2 *
    200   [3: #f1 #f2 normalize %
    201       [ inversion (expr_eq e1 f1) normalize #H1 #H2 [2: destruct ]
    202         cases (IH1 f1) cases (IH2 f2) /4 by eq_f2, sym_eq/
    203       | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4
    204         >H4/2 by /
    205 *)     
    206 
    207 lemma condition_eq_sym:∀c:condition.cond_i_eq c c=true.
    208 #c elim c [#e #f normalize >expr_eq_aux >expr_eq_aux normalize %
     115|4,7:#_ #_ %] qed. *)
     116
     117lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
     118#c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl normalize %
    209119|#c' normalize * %] qed.
    210120
    211121lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    212 #c1 #c2 % [2: * @condition_eq_sym
    213 | lapply c2 -c2 elim c1 normalize
    214   [ #e1 #e2 * normalize
    215     [ #f1 #f2 inversion(expr_eq f1 e1) normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize
    216 #H destruct [1,2:>(neqb_true_to_eq n2 n1 H) cases f2 cases e2
    217 [1,2,5,6,17,18,21,22:#k1 #k2 >neqb_refl normalize #K destruct >(neqb_true_to_eq k1 k2 K) %
    218 |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
    219 #ABS destruct|5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct
    220 |1,4,5,6,7,8: inversion(expr_eq h1 g1) #INV1 >INV1 normalize #INV2 destruct
    221 -c1 try(-c2) -e1 -e2 -f1 -f2 -H >INV1 in INV2; >neqb_refl >INV1 normalize
    222 #INV2 >expr_eq_sym in INV1; #INV1 >INV1 in INV2; normalize #INV2 >expr_eq_sym in INV1;
    223 #INV1 destruct >(expr_eq_equality_one g2 h2 INV2) >expr_eq_sym in INV1; #INV1
    224 >(expr_eq_equality_one g1 h1 INV1) %] >neqb_refl in ABS; normalize #ABS destruct]
    225 >neqb_refl in ABS; normalize #ABS destruct
    226 |9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS >neqb_refl in ABS; normalize #ABS destruct]
    227 |3,4,5,6:#ABS destruct >neqb_sym in H; #H >H in ABS; normalize #ABS destruct]
    228 |9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS1 #ABS2 destruct
    229 |11,12,15,16,27,28,31,32:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1)
    230 #INV1 >INV1 normalize #INV2 #E destruct >INV1 in E; normalize #E >expr_eq_sym in INV1; #INV1; >INV1 in E;
    231 normalize #E destruct >expr_eq_sym in INV1; #INV1 >(expr_eq_equality_one h1 g1 INV1)
    232 >expr_eq_sym in INV2; #INV2 >INV2 in E; normalize #E destruct >expr_eq_sym in INV2; #INV2
    233 >(expr_eq_equality_one h2 g2 INV2) >expr_eq_sym in E; #E >(expr_eq_equality_one f2 e2 E) %
    234 ]#f1 #f2 #n normalize #ABS1 #ABS2 destruct
    235 |#c2 #ABS destruct]|#c2 #H #c' cases c' [#e1 #e2 normalize #ABS destruct|#c3 normalize #K
    236 >(H c3 K) % qed.
    237 
    238 
    239 (*
    240 inductive cond_i:Type[0]≝cIfThenElse: cond_i.
    241 definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true.
    242 lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2
    243 cases c1 cases c2 % #_ % qed.
    244 *)
     122#c1 #c2 % [2: * // ]
     123lapply c2 -c2 elim c1 [ #e1 #e2 *
     124[ #f1 #f2 whd in ⊢ (??%? → ?);
     125  inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1
     126  >(proj1 … (expr_eq_equality …) … H1)
     127  inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 #_
     128  >(proj1 … (expr_eq_equality …) … H2) %
     129| normalize #c #H destruct
     130]| #c2 #IH *
     131[ normalize #e1 #e2 #H destruct
     132| #c3 #H >(IH … H) % ]]
     133qed.
    245134
    246135inductive loop_i:Type[0]≝lWhile: loop_i.
     
    248137lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
    249138cases l1 cases l2 % #_ % qed.
     139
     140definition io_i ≝ False.
     141
     142definition io_i_eq ≝ λi1,i2:False. true.
     143
     144lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
    250145
    251146(*
     
    336231
    337232definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
    338 normalize #s inversion(s) #INV #env [@(Some ? n)|@(Some ? n)|@(Some ? (S n))]qed.
     233normalize * [| 2: #v #e |3: #v ] #env [@(Some ? env)|@(Some ? n)|@(Some ? (S n))]qed.
    339234
    340235definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
Note: See TracChangeset for help on using the changeset viewer.