Changeset 859 for src

Timestamp:

May 30, 2011, 6:38:58 PM (10 years ago)

Author:

mulligan

Message:

more added

File:

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

src/ASM/AssemblyProof.ma

@@ -59 +59 @@
 qed.
 
+include "basics/jmeq.ma".
+
+notation > "hvbox(a break ≃ b)"
+  non associative with precedence 45
+for @{ 'jmeq ? $a ? $b }.
+
+notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
+  non associative with precedence 45
+for @{ 'jmeq $t $a $u $b }.
+
+interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
+
+lemma eq_to_jmeq:
+  ∀A: Type[0].
+  ∀x, y: A.
+    x = y → x ≃ y.
+  //
+qed.
+
+axiom vector_associativity_of_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)).
+        
+axiom vector_cons_append:
+  ∀A: Type[0].
+  ∀n: nat.
+  ∀a: A.
+  ∀v: Vector A n.
+    a ::: v = [[ a ]] @@ v.
+
+lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
+ #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
+qed.
+
+coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
+
+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 mem_middle_vector:
+  ∀A: Type[0].
+  ∀m, o: nat.
+  ∀eq: A → A → bool.
+  ∀reflex: ∀a. eq a a = true.
+  ∀p: Vector A m.
+  ∀a: A.
+  ∀r: Vector A o.
+    mem A eq ? (p@@(a:::r)) a = true.
+  # A # M # O # EQ # REFLEX # P # A
+  elim P
+  [ normalize
+    > (REFLEX A)
+    normalize
+    # H
+    %
+  | # NN # AA # PP # IH
+    normalize
+    cases (EQ A AA) //
+     @ IH
+  ]
+qed.
+
+lemma mem_monotonic_wrt_append:
+  ∀A: Type[0].
+  ∀m, o: nat.
+  ∀eq: A → A → bool.
+  ∀reflex: ∀a. eq a a = true.
+  ∀p: Vector A m.
+  ∀a: A.
+  ∀r: Vector A o.
+    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
+  # A # M # O # EQ # REFLEX # P # A
+  elim P
+  [ #R #H @H
+  | #NN #AA # PP # IH #R #H
+    normalize
+    cases (EQ A AA)
+    [ normalize %
+    | @ IH @ H
+    ]
+  ]
+qed.
+
+lemma subvector_hd_tl:
+  ∀A: Type[0].
+  ∀o, n: nat.
+  ∀eq: A → A → bool.
+  ∀refl: ∀a. eq a a = true.
+  ∀h: Vector A o.
+  ∀v: Vector A n.
+  ∀m: nat.
+  ∀q: Vector A m.
+    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
+  # A # O # N # EQ # REFLEX # H # V
+  elim V
+  [ normalize
+    # M # V %
+  | # NN # AA # VV # IH # MM # QQ
+    change with (bool_to_Prop (andb ??))
+    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
+    [ 
+    | # HH > HH
+      > (vector_cons_append ? ? AA VV)
+      change with (bool_to_Prop (subvector_with ??????))
+      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
+        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
+        ?
+        (vector_associativity_of_append A ? ? ? QQ [[AA]] VV))
+      [ >associative_plus //
+      | @IH ]
+    ]
+    @(mem_monotonic_wrt_append)
+    [ @ REFLEX
+    | @(mem_monotonic_wrt_append)
+      [ @ REFLEX
+      | normalize
+        > REFLEX
+        normalize
+        %
+      ]
+    ]
+qed.
 (*
 lemma subvector_hd_tl:
@@ -100 +232 @@
     whd in ⊢ (% → ?)
   ]
+  *)
 
 let rec list_addressing_mode_tags_elim
@@ -140 +273 @@
       ]
   ].
+(*
 
 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
  λP.
    P (ADD … ACC_A 
-   P (DA … ACC_A).
+   P (DA … ACC_A).lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
+ #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
+qed.
  %
 qed.
@@ -173 +309 @@
   
 (* RUSSEL **)
-
-include "basics/jmeq.ma".
-
-notation > "hvbox(a break ≃ b)"
-  non associative with precedence 45
-for @{ 'jmeq ? $a ? $b }.
-
-notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
-  non associative with precedence 45
-for @{ 'jmeq $t $a $u $b }.
-
-interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
 
 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.