Changeset 853 for src

Timestamp:

May 27, 2011, 1:58:21 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -2 +2 @@
 include "ASM/Interpret.ma".
 
+(*
 axiom append_cons_commute:
   ∀A: Type[0].
@@ -7 +8 @@
   ∀h: A.
     l @ h::r = l @ [h] @ r.
-
+*)
 (*
 axiom append_associative:
@@ -16 +17 @@
 
 let rec foldl_strong_internal
-  (A: Type[0]) (P: list A → Prop) (l: list A)
+  (A: Type[0]) (P: list A → Type[0]) (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:
@@ -35 +36 @@
 definition foldl_strong ≝
   λA: Type[0].
-  λP: list A → Prop.
+  λP: list A → Type[0].
   λl: list A.
   λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
-  λsuffix: list A.
   λacc: P [ ].
-    foldl_strong_internal A P l H [ ] suffix acc.
-
-definition bit_elim: ∀P: bool → bool. bool ≝
-  λP.
-    P true ∧ P false.
-
-definition bitvector_elim: ∀P: ∀n. BitVector n → bool. ∀n: nat. bool ≝
-  λP.
-  λn.
-    P n.
-  
-    
-  
-    (* > append_cons_commute
-    @ 
+    foldl_strong_internal A P l H [ ] l acc (refl …).
 
 (* 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".
+
+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.
@@ -167 +128 @@
 qed.
 
-(*
 definition build_maps' ≝
   λpseudo_program.
   let 〈preamble,instr_list〉 ≝ pseudo_program in
   let result ≝
-   foldl
-    ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))
+   foldl_strong
     (option Identifier × pseudo_instruction)
-    (λt,i.
+    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
+      let pre' ≝ 〈preamble,pre〉 in
+      let 〈labels,pc_costs〉 ≝ res in
+      let 〈ignore,costs〉 ≝ pc_costs in
+       ∀pc. (nat_of_bitvector … pc) < length … pre →
+        lookup ?? pc labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre pc)))
+    instr_list
+    (λprefix,i,tl,prf,t.
       let 〈labels, pc_costs〉 ≝ t in
       let 〈program_counter, costs〉 ≝ pc_costs in
@@ -193 +159 @@
          | Some construct ⇒ 〈labels, construct〉
          ]
-    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
+    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
   in
    let 〈labels, pc_costs〉 ≝ result in
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
-
+ [
+ |
+ | whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
+qed.
+
+(*
 (*
 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
@@ -289 +260 @@
  ∀A:Type[0].∀l,l1,l2:list A.
   is_prefix … l l1 → is_prefix … l (l1@l2).
-
-record Propify (A:Type[0]) : Prop ≝ { in_propify: A }.
+axiom prefix_reflexive: ∀A,l. is_prefix A l l.
+axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
+
+record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
 
 definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
@@ -339 +312 @@
  ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
 
+axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
+axiom pprefix_of_append:
+ ∀A:Type[0].∀l,l1,l2.
+  is_pprefix A l l1 → is_pprefix A l (l1@l2).
+axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
+axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
+
+
+axiom foldll':
+ ∀A:Type[0].∀l: list A.
+  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
+  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
+   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
+ #A #l #B
+ generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
+ 
+ 
+  #H #acc
+ @foldll
+  [
+  |
+  ]
+ 
+ ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
+
+
+(*
+record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
+ { subset_wit:> A;
+   subset_proof: P subset_wit
+ }.
+*)
+
 definition build_maps' ≝
   λpseudo_program.
   let 〈preamble,instr_list〉 ≝ pseudo_program in
   let result ≝
-   foldl
-    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
-          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
-           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
-    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
-          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
-           is_prefix ? instr_list_prefix' instr_list →
-           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
-    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
-          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
-           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
-     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
-          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
-           is_prefix ? instr_list_prefix' instr_list →
-           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
+   foldll
+    (option Identifier × pseudo_instruction)
+    (λprefix.
+      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
+       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
+    (λprefix,t,i.
       let 〈labels, pc_costs〉 ≝ t in
       let 〈program_counter, costs〉 ≝ pc_costs in
@@ -375 +372 @@
          | Some construct ⇒ 〈labels, construct〉
          ]
-    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
+    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
   in
    let 〈labels, pc_costs〉 ≝ result in
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
+ [
+ | @⊥ 
+ | normalize % // 
+ ]
+qed.
 
 definition build_maps' ≝