Changeset 2254 for src/Cminor

Timestamp:

Jul 24, 2012, 7:40:23 PM (9 years ago)

Author:

campbell

Message:

Fix up invariants in Cminor semantics.

File:

• src/Cminor/semantics.ma (modified) (5 diffs)

src/Cminor/semantics.ma

@@ -169 +169 @@
 //
 try @(π2 Inv)
-try @(π2 (π1 Inv))
-[ % [ @(π2 Inv) | @kInv ]
+try @(π1 (π2 Inv))
+try @(π2 (π2 Inv))
+[ % [ @(π2 (π2 Inv)) | @kInv ]
 | % [ @(π2 Inv) | @kInv ]
 ] qed. 
@@ -180 +181 @@
 try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) ) 
 [ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
-  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
+  lapply (IH1 (Kseq s2 k) f en (π1 (π2 Inv)) (conj ?? (π2 (π2 Inv)) kInv))
   cases (find_label l s1 (Kseq s2 k) f en ??)
   [ #H1 whd in ⊢ (??%? → ?);
-    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
+    lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??)
     [ #H2 #_ % #H cases (Exists_append … H)
       [ #H' cases (H1 (refl ??)) /2/
@@ -193 +194 @@
   ]
 | #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
-  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
+  lapply (IH1 k f en (π1 (π2 Inv)) kInv)
   cases (find_label l s1 k f en ??)
   [ #H1 whd in ⊢ (??%? → ?);
-    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
+    lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??)
     [ #H2 #_ % #H cases (Exists_append … H)
       [ #H' cases (H1 (refl ??)) /2/
@@ -382 +383 @@
 try @kInv
 try @(π1 (π1 Inv))
-try (@cont_inv_update @kInv)
-try @(π2 (π1 (π1 Inv)))
+try (@cont_inv_update @kInv) 
+try @(π2 (π1 (π1 Inv))) 
 try @(π1 (π1 (π1 Inv)))
-try @(π1 Inv)
 try @(π2 Inv)
+try @(π1 (π2 Inv))
 [ @fInv
 | @(π2 Inv')
 | @(π1 Inv')
-| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
-| % [ @(π2 Inv) | @kInv ]
+| cases b [ @(π1 (π2 Inv)) | @(π2 (π2 Inv)) ]
+| % [ @(π2 (π2 Inv)) | @kInv ]
+| @(π1 (π1 (π1 (π1 Inv))))
+| @(π2 (π1 (π1 (π1 Inv))))
+| /3/
 | @stmt_inv_update @fInv
-| 7,8:
+| /3/
+| /3/
+| 12,13:
   @(stmt_P_mp … (f_inv f))
   #s * #V #L #R %
@@ -406 +412 @@
 | @I
 | @cont_inv_update @Inv
+| /3/
 | @stmt_inv_update @fInv
 | @Inv
+| /3/
 | @fInv
 ] qed.