Changeset 2937 for src

Timestamp:

Mar 21, 2013, 9:45:59 PM (7 years ago)

Author:

campbell

Message:

Speed up checking of RTLabs/CostInj.ma.

File:

• src/RTLabs/CostInj.ma (modified) (5 diffs)

src/RTLabs/CostInj.ma

@@ -1 @@
-include "RTLabs/RTLabs_traces.ma".
+include "RTLabs/CostSpec.ma".
 
 (* Check that the RTLabs pc → cost label map is injective for a given RTLabs
@@ -68 +68 @@
       [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3)
         [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct
-        | * #_ #PR'' @H1 /3/
+        | * #_ #PR'' @H1 % /2/
         ]
       | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/
@@ -78 +78 @@
           [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct
             @lookup_add_hit
-          | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
+          | * #NE #PR'' lapply (H1 ?) [% /2/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
           ]
         | #Lcl' cases (lookup_add_cases ??????? Lcl')
@@ -90 +90 @@
         [ assumption
         | >(lookup_present_eq ????? L ?) assumption
-        | #E destruct /2/
+        | #E destruct @(absurd … PR' FR)
         ]
       ]
@@ -100 +100 @@
   ]
 | cases r
-  [ //
+  [ whd in ⊢ (% → %); //
   | #m whd in ⊢ (% → %); #H
     #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2