Changeset 1516 for src/Clight/CexecComplete.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (9 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/Clight/CexecComplete.ma (modified) (15 diffs)

src/Clight/CexecComplete.ma

@@ -30 +30 @@
 
 lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
-#A #a #v' cases a; // #m whd in ⊢ (% → ?) *;
+#A #a #v' cases a; // #m whd in ⊢ (% → ?); *;
 qed. 
 
@@ -65 +65 @@
 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16
 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26
->e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14
+>e11 in e21; #e1 >(?:ge1 = ge2) in e13 e14;
 [ 2: destruct (e1) skip (e11); @refl ]
 #e13 #e14
 
->e12 in e22 #e2 destruct (e2) skip (e12);
-
->e13 in e23 #e3 >(?:b1 = b2) in e14
+>e12 in e22; #e2 destruct (e2) skip (e12);
+
+>e13 in e23; #e3 >(?:b1 = b2) in e14;
 [ >e24 #e4 >(?:f2 = f1)
   [ //;
@@ -88 +88 @@
 >e2
 whd in ⊢ (??%?);
-change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
+change in e1:(??%?); with (make_global (mk_program ?? globs fns main))
 >e1
 >e3
@@ -100 +100 @@
 #m #v #ty #ty' #v' #H
 elim H;
-[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
+[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
 | #m #f #sz #szi #sg @refl
-| #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
+| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
 | #m #f #sz #sz' @refl
 | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
-    elim H1 in pc ⊢ % [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
-    whd in ⊢ (??%?)
-    [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ]
+    elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
+    whd in ⊢ (??%?);
+    [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?); ]
     elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]
-    #pc' whd in ⊢ (??%?) 
+    #pc' whd in ⊢ (??%?); 
     @(dec_true ? (pointer_compat_dec b sp2) pc') //
-| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
-  >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
+| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?);
+  >intsize_eq_elim_true whd in ⊢ (??%?); cases sz //;
 | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
     whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
@@ -132 +132 @@
 lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
 #v #ty #r #H elim H; #v #t #H' elim H';
-  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
+  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
     >(eq_bv_false … ne) //
   | #r #b #pc #i #i0 #s %{ true} % //
   | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
-  | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
+  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
   | #r #r' #t %{ false} % //;
   | #s %{ false} % //; whd; >(Feq_zero_true …) //;
@@ -144 +144 @@
 lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
 #v #ty #H elim H;
-  [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
+  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
   | #p #b #i #i0 #s //
   | #f #s #ne whd; >(Feq_zero_false … ne) //;
@@ -152 +152 @@
 lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
 #v #ty #H elim H;
-  [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
+  [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //;
   | #r #r' #t //;
   | #s whd; >(Feq_zero_true …) //;
@@ -165 +165 @@
   (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
   (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
-[ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
+[ #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl
 | #f #ty @refl
 | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
     [ #id | #e' | #e' #id ] #H3
-    whd in ⊢ (??%?)
-    [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty)
-    | change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty)
-    | change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty)
+    whd in ⊢ (??%?);
+    [ change in H3:(??%?); with (exec_lvalue' ge env m (Evar id) ty)
+    | change in H3:(??%?); with (exec_lvalue' ge env m (Ederef e') ty)
+    | change in H3:(??%?); with (exec_lvalue' ge env m (Efield e' id) ty)
     ]
     >(yields_eq ??? H3)
-    whd in ⊢ (??%?) change in H2:(??%?) with (load_value_of_type' ty m 〈l,off〉)
+    whd in ⊢ (??%?); change in H2:(??%?); with (load_value_of_type' ty m 〈l,off〉)
     >H2 @refl
 | #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
-    >(yields_eq ??? H2) whd in ⊢ (??%?)
+    >(yields_eq ??? H2) whd in ⊢ (??%?);
     @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
     @refl
@@ -326 +326 @@
 [ #env'' #m'' %
 | #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
-  < H3 whd in H1:(??%?) ⊢ (??%?)
+  < H3 whd in H1:(??%?) ⊢ (??%?);
   < (pair_eq1 ?????? H1) < (pair_eq2 ?????? H1)
   @refl
@@ -337 +337 @@
 [ //;
 | #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4
-    whd in ⊢ (??%?)
+    whd in ⊢ (??%?);
     >H1 whd in ⊢ (??%?);
     >H2 whd in ⊢ (??%?);
@@ -345 +345 @@
 lemma eventval_match_complete': ∀ev,ty,v.
   eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
-#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
+#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl qed.
 
 lemma eventval_list_match_complete: ∀vs,tys,evs.
@@ -351 +351 @@
 #vs #tys #evs #H elim H;
 [ //
-| #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?)
-    >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?)
-    >(yields_eq ??? H3) whd in ⊢ (??%?) //
+| #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?);
+    >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?);
+    >(yields_eq ??? H3) whd in ⊢ (??%?); //
 ] qed.
 
@@ -360 +360 @@
 #ge #s #tr #s' #H elim H;
 [ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
-    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?)
-    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?)
-    change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
+    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
+    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
+    change in H3:(??%?); with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
     >H3 @refl
 | #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
@@ -446 +446 @@
     //
 | #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
-    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2
+    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2;
     #H1 #H2
     >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
@@ -453 +453 @@
 | #v #f #env #k #m @refl
 | #v #f #env #k #m1 #m2 #loc #ofs #ty
-    change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v)
-    #H whd in ⊢ (??%?) >H @refl
+    change in ⊢ (??%? → ?); with (store_value_of_type' ty m1 〈loc,ofs〉 v)
+    #H whd in ⊢ (??%?); >H @refl
 | #f #l #s #k #env #m @refl
 ] qed.