Changeset 851


Ignore:
Timestamp:
May 27, 2011, 12:40:19 PM (8 years ago)
Author:
mulligan
Message:

strong foldl added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r850 r851  
    22include "ASM/Interpret.ma".
    33
     4axiom append_cons_commute:
     5  ∀A: Type[0].
     6  ∀l, r: list A.
     7  ∀h: A.
     8    l @ h::r = l @ [h] @ r.
     9
     10(*
     11axiom append_associative:
     12  ∀A: Type[0].
     13  ∀l, c, r: list A.
     14    (l @ c) @ r = l
     15*)
     16
     17let rec foldl_strong
     18  (A: Type[0]) (P: list A → Prop) (l: list A)
     19  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
     20  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
     21    l = prefix @ suffix → P(prefix @ suffix) ≝
     22  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
     23  [ nil ⇒ λprf. ?
     24  | cons hd tl ⇒ λprf. ?
     25  ].
     26  [ > (append_nil ?)
     27    @ acc
     28  | applyS (foldl_strong A P l H (prefix @ [hd]) tl ? ?)
     29    [ @ (H prefix hd tl prf acc)
     30    | applyS prf
     31    ]
     32  ]
     33qed.
     34 
     35    (* > append_cons_commute
     36    @
     37
    438(* RUSSEL **)
     39
     40axiom addr11_elim:
     41  ∀P: Word11 → Prop.
     42    (∀b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11: bool.
     43      P [[ b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11]])→
     44        ∀w: Word11. P w.
     45
     46(* using modified version of matita with hacked ng_refiner/nCicMetaSubst.ml *)
     47lemma test:
     48  ∀i: instruction.
     49  ∃pc.
     50  let assembled ≝ assembly1 i in
     51  let code_memory ≝ load_code_memory assembled in
     52  let fetched ≝ fetch code_memory pc in
     53  let 〈instr_pc, ticks〉 ≝ fetched in
     54    \fst instr_pc = i.
     55  # INSTR
     56  %
     57  [ @ (zero 16)
     58  | cases INSTR
     59    [ #ADDR11 cases ADDR11 #ADDRX cases ADDRX
     60       [18: #A #P
     61        @ (addr11_elim … A)
     62        ***********
     63        [ normalize
     64cases B1
     65        normalize; whd;
     66     
     67   
     68      whd
     69      normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
     70      letin xxx ≝ (subaddressing_modeel O [[addr11]] ADDR11)
     71      normalize in xxx;
     72      normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
     73    ]
     74  ].
    575
    676include "basics/jmeq.ma".
     
    552622  ].
    553623
    554 lemma test:
    555   ∀i: instruction.
    556   ∃pc.
    557   let assembled ≝ assembly1 i in
    558   let code_memory ≝ load_code_memory assembled in
    559   let fetched ≝ fetch code_memory pc in
    560   let 〈instr_pc, ticks〉 ≝ fetched in
    561     \fst instr_pc = i.
    562   # INSTR
    563   %
    564   [ @ (zero 16)
    565   | cases INSTR
    566   ].
    567 
    568 lemma test:
     624(* prove later *)
     625axiom test:
    569626  ∀pc: Word.
    570627  ∀code_memory: BitVectorTrie Byte 16.
     
    575632        let 〈instr, pc〉 ≝ instr_pc in
    576633          instr = i.
    577   # PC # CODE_MEMORY # INSTRUCTION
    578   whd
    579   whd in ⊢ (? → match % with [ _ ⇒ ? ])
    580   cases (next CODE_MEMORY PC)
    581   whd
    582   # PC1 # V1
    583 
    584 
    585   cases (fetch CODE_MEMORY PC)
    586   # INSTR_PC
    587   # TICKS
    588   cases (INSTRUCTION)
    589   [ # ADDR11
    590     # ENCODING_CHECK
    591     whd in ENCODING_CHECK;
    592     normalize
    593     cases (INSTR_PC)
    594     # INSTR
    595     # PC
    596     normalize
    597    
    598    
    599   # ENCODING
    600   normalize
    601   [ cases INSTR_PC
    602     # NEW_INSTRUCTION
    603     # PC
    604     normalize
    605     normalize in ENCODING;
    606   | # ASSEMBLED
    607     whd
    608634 
    609635lemma main_thm:
Note: See TracChangeset for help on using the changeset viewer.