Changeset 1939 for src/ASM/AssemblyProof.ma

Timestamp:

May 14, 2012, 10:37:08 AM (8 years ago)

Author:

mulligan

Message:

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

File:

• src/ASM/AssemblyProof.ma (modified) (11 diffs)

src/ASM/AssemblyProof.ma

@@ -107 +107 @@
   ∀P: ∀m. Vector A m → Prop.
     n = m → v1 ≃ v2 → P n v1 → P m v2.
-  #A #n #m #v1 #v2 #P #EQ
-  <EQ in v2; #V #JMEQ
-  >JMEQ //
+  #A #n #m #v1 #v2 #P #eq #jmeq
+  destruct #assm assumption
 qed.
 
@@ -119 +118 @@
     e ::: v = [[ e ]] @@ v.
   #A #n #e #v
-  elim v
-  [1:
-    normalize %
-  |2:
-    #NN #AA #VV #IH
-    normalize
-    %
-  ]
+  cases v try %
+  #n' #hd #tl %
 qed.
 
@@ -137 +130 @@
     hd:::(v@@q) = (hd:::v)@@q.
   #A #n #m #v #q
-  elim v
-  [1:
-    #hd %
-  |2:
-    #n' #hd' #tl' #ih #hd'
-    <ih %
-  ]
+  elim v try (#hd %)
+  #n' #hd' #tl' #ih #hd'
+  <ih %
 qed.
 
@@ -185 +174 @@
     mem A eq ? (p@@(a:::r)) a = true.
   #A #m #o #eq #reflex #p #a
-  elim p
-  [1:
-    normalize
-    >reflex
-    #H %
-  |2:
-    #m' #hd #tl #inductive_hypothesis
-    normalize
-    cases (eq ??) normalize nodelta
-    [1:
-      #_ %
-    |2:
-      @inductive_hypothesis
-    ]
-  ]
+  elim p try (normalize >reflex #H %)
+  #m' #hd #tl #inductive_hypothesis
+  normalize
+  cases (eq ??) normalize nodelta
+  try (#irrelevant %)
+  @inductive_hypothesis
 qed.
 
@@ -212 +192 @@
     mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
   #A #m #o #eq #reflex #p #a
-  elim p
-  [1:
-    #r #assm assumption
-  |2:
-    #m' #hd #tl #inductive_hypothesis #r #assm
-    normalize
-    cases (eq ??) try %
-    @inductive_hypothesis assumption
-  ]
+  elim p try (#r #assm assumption)
+  #m' #hd #tl #inductive_hypothesis #r #assm
+  normalize
+  cases (eq ??) try %
+  @inductive_hypothesis assumption
 qed.
 
@@ -234 +210 @@
     bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
   #A #o #n #eq #reflex #h #v
-  elim v
+  elim v try (normalize #m #irrelevant @I)
+  #m' #hd #tl #inductive_hypothesis #m #q
+  change with (bool_to_Prop (andb ??))
+  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
   [1:
-    normalize #m #_ @I
+    @mem_monotonic_wrt_append try assumption
+    @mem_monotonic_wrt_append try assumption
+    normalize >reflex %
   |2:
-    #m' #hd #tl #inductive_hypothesis #m #q
-    change with (bool_to_Prop (andb ??))
-    cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
-    [1:
-      @mem_monotonic_wrt_append try assumption
-      @mem_monotonic_wrt_append try assumption
-      normalize >reflex %
-    |2:
-      #assm >assm
-      >vector_cons_append
-      change with (bool_to_Prop (subvector_with ??????))
-      @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
-      try @associative_plus
-      @inductive_hypothesis
-    ]
+    #assm >assm
+    >vector_cons_append
+    change with (bool_to_Prop (subvector_with ??????))
+    @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
+    try @associative_plus
+    @inductive_hypothesis
   ]
 qed.
@@ -803 +775 @@
     eq_sum A B leq req s s = true.
   #A #B #leq #req #s #leq_refl #req_refl
-  cases s
-  whd in ⊢ (? → ??%?);
-  assumption
+  cases s assumption
 qed.
 
@@ -828 +798 @@
   try @eq_addressing_mode_refl
   [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
-    whd in ⊢ (??%?);
-    try %
+    whd in ⊢ (??%?); try %
     >eq_addressing_mode_refl
     >eq_addressing_mode_refl %
@@ -852 +821 @@
     |3:
       #arg1_left normalize nodelta
-      >(eq_sum_refl …) [1: %
-      |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
+      >(eq_sum_refl …)
+      [1:
+        %
+      |2,3:
+        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
+      ]
     |4:
       #arg1_left normalize nodelta
@@ -1291 +1264 @@
 *)
 
-lemma split_elim:
+definition split_elim:
   ∀A: Type[0].
   ∀l, m: nat.
@@ -1298 +1271 @@
     (∀vl: Vector A l.
      ∀vm: Vector A m.
-      v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
-  cases daemon (* XXX: problem with dependent types *)
-qed.
+      v = vl@@vm → P 〈vl,vm〉) → P (split A l m v) ≝
+  λa: Type[0].
+  λl, m: nat.
+  λv: Vector a (l + m).
+  λP.
+  match v return λn: nat. λv: Vector a (n + m).
+    (∀vl: Vector a ?.
+     ∀vm: Vector a m.
+      v = vl@@vm → P 〈vl,vm〉) → P (split a ? m v) with
+  [ VEmpty ⇒ ?
+  | VCons v' hd tl ⇒ ?
+  ] ?.
 
 (* XXX: this looks almost certainly wrong *)