Changeset 992 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 17, 2011, 6:05:05 PM (8 years ago)

Author:

mulligan

Message:

a few more axioms closed

File:

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

src/ASM/AssemblyProof.ma

@@ -78 +78 @@
 qed.
 
-axiom vector_associative_append:
-  ∀A: Type[0].
-  ∀n, m, o:  nat.
-  ∀v: Vector A n.
-  ∀q: Vector A m.
-  ∀r: Vector A o.
-    ((v @@ q) @@ r)
-    ≃
-    (v @@ (q @@ r)).
-        
+lemma super_rewrite2:
+ ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
+  ∀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 //
+qed.
+
 lemma vector_cons_append:
   ∀A: Type[0].
@@ -103 +100 @@
 qed.
 
-lemma super_rewrite2:
- ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
-  ∀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 //
+lemma vector_cons_append2:
+  ∀A: Type[0].
+  ∀n, m: nat.
+  ∀v: Vector A n.
+  ∀q: Vector A m.
+  ∀hd: A.
+    hd:::(v@@q) = (hd:::v)@@q.
+  #A #n #m #v #q
+  elim v
+  [ #hd %
+  | #n' #hd' #tl' #ih #hd' <ih %
+  ]
+qed.
+
+lemma jmeq_cons_vector_monotone:
+  ∀A: Type[0].
+  ∀m, n: nat.
+  ∀v: Vector A m.
+  ∀q: Vector A n.
+  ∀prf: m = n.
+  ∀hd: A.
+    v ≃ q → hd:::v ≃ hd:::q.
+  #A #m #n #v #q #prf #hd #E
+  @(super_rewrite2 A … E)
+  [ assumption | @jmrefl ]
+qed.
+
+lemma vector_associative_append:
+  ∀A: Type[0].
+  ∀n, m, o:  nat.
+  ∀v: Vector A n.
+  ∀q: Vector A m.
+  ∀r: Vector A o.
+    ((v @@ q) @@ r)
+    ≃
+    (v @@ (q @@ r)).
+  #A #n #m #o #v #q #r
+  elim v
+  [ %
+  | #n' #hd #tl #ih
+    <(vector_cons_append2 A … hd)
+    @jmeq_cons_vector_monotone
+    //
+  ]
 qed.