Changeset 851 for src

Timestamp:

May 27, 2011, 12:40:19 PM (10 years ago)

Author:

mulligan

Message:

strong foldl added

File:

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

src/ASM/AssemblyProof.ma

@@ -2 +2 @@
 include "ASM/Interpret.ma".
 
+axiom append_cons_commute:
+  ∀A: Type[0].
+  ∀l, r: list A.
+  ∀h: A.
+    l @ h::r = l @ [h] @ r.
+
+(*
+axiom append_associative:
+  ∀A: Type[0].
+  ∀l, c, r: list A.
+    (l @ c) @ r = l 
+*)
+
+let rec foldl_strong
+  (A: Type[0]) (P: list A → Prop) (l: list A)
+  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
+  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
+    l = prefix @ suffix → P(prefix @ suffix) ≝
+  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
+  [ nil ⇒ λprf. ?
+  | cons hd tl ⇒ λprf. ?
+  ].
+  [ > (append_nil ?)
+    @ acc
+  | applyS (foldl_strong A P l H (prefix @ [hd]) tl ? ?)
+    [ @ (H prefix hd tl prf acc)
+    | applyS prf
+    ]
+  ]
+qed.
+  
+    (* > append_cons_commute
+    @ 
+
 (* RUSSEL **)
+
+axiom addr11_elim:
+  ∀P: Word11 → Prop.
+    (∀b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11: bool.
+      P [[ b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11]])→
+        ∀w: Word11. P w.
+
+(* using modified version of matita with hacked ng_refiner/nCicMetaSubst.ml *)
+lemma test:
+  ∀i: instruction.
+  ∃pc.
+  let assembled ≝ assembly1 i in
+  let code_memory ≝ load_code_memory assembled in
+  let fetched ≝ fetch code_memory pc in
+  let 〈instr_pc, ticks〉 ≝ fetched in
+    \fst instr_pc = i.
+  # INSTR
+  %
+  [ @ (zero 16)
+  | cases INSTR
+    [ #ADDR11 cases ADDR11 #ADDRX cases ADDRX
+       [18: #A #P
+        @ (addr11_elim … A)
+        ***********
+        [ normalize
+cases B1
+        normalize; whd;
+      
+    
+      whd
+      normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
+      letin xxx ≝ (subaddressing_modeel O [[addr11]] ADDR11)
+      normalize in xxx;
+      normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
+    ]
+  ].
 
 include "basics/jmeq.ma".
@@ -552 +622 @@
   ].
 
-lemma test:
-  ∀i: instruction.
-  ∃pc.
-  let assembled ≝ assembly1 i in
-  let code_memory ≝ load_code_memory assembled in
-  let fetched ≝ fetch code_memory pc in
-  let 〈instr_pc, ticks〉 ≝ fetched in
-    \fst instr_pc = i.
-  # INSTR
-  %
-  [ @ (zero 16)
-  | cases INSTR
-  ].
-
-lemma test:
+(* prove later *)
+axiom test:
   ∀pc: Word.
   ∀code_memory: BitVectorTrie Byte 16.
@@ -575 +632 @@
         let 〈instr, pc〉 ≝ instr_pc in
           instr = i.
-  # PC # CODE_MEMORY # INSTRUCTION
-  whd
-  whd in ⊢ (? → match % with [ _ ⇒ ? ])
-  cases (next CODE_MEMORY PC)
-  whd
-  # PC1 # V1
-
-
-  cases (fetch CODE_MEMORY PC)
-  # INSTR_PC
-  # TICKS
-  cases (INSTRUCTION)
-  [ # ADDR11
-    # ENCODING_CHECK
-    whd in ENCODING_CHECK;
-    normalize
-    cases (INSTR_PC)
-    # INSTR
-    # PC
-    normalize
-    
-    
-  # ENCODING
-  normalize
-  [ cases INSTR_PC
-    # NEW_INSTRUCTION
-    # PC
-    normalize
-    normalize in ENCODING;
-  | # ASSEMBLED
-    whd
  
 lemma main_thm: