Ignore:
Timestamp:
May 27, 2011, 1:58:21 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r852 r853  
    22include "ASM/Interpret.ma".
    33
     4(*
    45axiom append_cons_commute:
    56  ∀A: Type[0].
     
    78  ∀h: A.
    89    l @ h::r = l @ [h] @ r.
    9 
     10*)
    1011(*
    1112axiom append_associative:
     
    1617
    1718let rec foldl_strong_internal
    18   (A: Type[0]) (P: list A → Prop) (l: list A)
     19  (A: Type[0]) (P: list A → Type[0]) (l: list A)
    1920  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
    2021  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
     
    3536definition foldl_strong ≝
    3637  λA: Type[0].
    37   λP: list A → Prop.
     38  λP: list A → Type[0].
    3839  λl: list A.
    3940  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
    40   λsuffix: list A.
    4141  λacc: P [ ].
    42     foldl_strong_internal A P l H [ ] suffix acc.
    43 
    44 definition bit_elim: ∀P: bool → bool. bool ≝
    45   λP.
    46     P true ∧ P false.
    47 
    48 definition bitvector_elim: ∀P: ∀n. BitVector n → bool. ∀n: nat. bool ≝
    49   λP.
    50   λn.
    51     P n.
    52  
    53    
    54  
    55     (* > append_cons_commute
    56     @
     42    foldl_strong_internal A P l H [ ] l acc (refl …).
    5743
    5844(* RUSSEL **)
    5945
    60 axiom addr11_elim:
    61   ∀P: Word11 → Prop.
    62     (∀b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11: bool.
    63       P [[ b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11]])→
    64         ∀w: Word11. P w.
    65 
    66 (* using modified version of matita with hacked ng_refiner/nCicMetaSubst.ml *)
    67 lemma test:
    68   ∀i: instruction.
    69   ∃pc.
    70   let assembled ≝ assembly1 i in
    71   let code_memory ≝ load_code_memory assembled in
    72   let fetched ≝ fetch code_memory pc in
    73   let 〈instr_pc, ticks〉 ≝ fetched in
    74     \fst instr_pc = i.
    75   # INSTR
    76   %
    77   [ @ (zero 16)
    78   | cases INSTR
    79     [ #ADDR11 cases ADDR11 #ADDRX cases ADDRX
    80        [18: #A #P
    81         @ (addr11_elim … A)
    82         ***********
    83         [ normalize
    84 cases B1
    85         normalize; whd;
    86      
    87    
    88       whd
    89       normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
    90       letin xxx ≝ (subaddressing_modeel O [[addr11]] ADDR11)
    91       normalize in xxx;
    92       normalize in ⊢ (match (?(?(%))?) with [ _ ⇒ ? ])
    93     ]
    94   ].
    9546
    9647include "basics/jmeq.ma".
     48
     49notation > "hvbox(a break ≃ b)"
     50  non associative with precedence 45
     51for @{ 'jmeq ? $a ? $b }.
     52
     53notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
     54  non associative with precedence 45
     55for @{ 'jmeq $t $a $u $b }.
     56
     57interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
    9758
    9859definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
     
    167128qed.
    168129
    169 (*
    170130definition build_maps' ≝
    171131  λpseudo_program.
    172132  let 〈preamble,instr_list〉 ≝ pseudo_program in
    173133  let result ≝
    174    foldl
    175     ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))
     134   foldl_strong
    176135    (option Identifier × pseudo_instruction)
    177     (λt,i.
     136    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
     137      let pre' ≝ 〈preamble,pre〉 in
     138      let 〈labels,pc_costs〉 ≝ res in
     139      let 〈ignore,costs〉 ≝ pc_costs in
     140       ∀pc. (nat_of_bitvector … pc) < length … pre →
     141        lookup ?? pc labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre pc)))
     142    instr_list
     143    (λprefix,i,tl,prf,t.
    178144      let 〈labels, pc_costs〉 ≝ t in
    179145      let 〈program_counter, costs〉 ≝ pc_costs in
     
    193159         | Some construct ⇒ 〈labels, construct〉
    194160         ]
    195     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
     161    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
    196162  in
    197163   let 〈labels, pc_costs〉 ≝ result in
    198164   let 〈pc, costs〉 ≝ pc_costs in
    199165    〈labels, costs〉.
    200 
     166 [
     167 |
     168 | whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
     169qed.
     170
     171(*
    201172(*
    202173notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     
    289260 ∀A:Type[0].∀l,l1,l2:list A.
    290261  is_prefix … l l1 → is_prefix … l (l1@l2).
    291 
    292 record Propify (A:Type[0]) : Prop ≝ { in_propify: A }.
     262axiom prefix_reflexive: ∀A,l. is_prefix A l l.
     263axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
     264
     265record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
    293266
    294267definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
     
    339312 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
    340313
     314axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
     315axiom pprefix_of_append:
     316 ∀A:Type[0].∀l,l1,l2.
     317  is_pprefix A l l1 → is_pprefix A l (l1@l2).
     318axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
     319axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
     320
     321
     322axiom foldll':
     323 ∀A:Type[0].∀l: list A.
     324  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
     325  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
     326   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
     327 #A #l #B
     328 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
     329 
     330 
     331  #H #acc
     332 @foldll
     333  [
     334  |
     335  ]
     336 
     337 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
     338
     339
     340(*
     341record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
     342 { subset_wit:> A;
     343   subset_proof: P subset_wit
     344 }.
     345*)
     346
    341347definition build_maps' ≝
    342348  λpseudo_program.
    343349  let 〈preamble,instr_list〉 ≝ pseudo_program in
    344350  let result ≝
    345    foldl
    346     (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    347           ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
    348            tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
    349     (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    350           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    351            is_prefix ? instr_list_prefix' instr_list →
    352            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
    353     (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    354           ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
    355            tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
    356      λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    357           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    358            is_prefix ? instr_list_prefix' instr_list →
    359            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
     351   foldll
     352    (option Identifier × pseudo_instruction)
     353    (λprefix.
     354      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
     355       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
     356    (λprefix,t,i.
    360357      let 〈labels, pc_costs〉 ≝ t in
    361358      let 〈program_counter, costs〉 ≝ pc_costs in
     
    375372         | Some construct ⇒ 〈labels, construct〉
    376373         ]
    377     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
     374    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
    378375  in
    379376   let 〈labels, pc_costs〉 ≝ result in
    380377   let 〈pc, costs〉 ≝ pc_costs in
    381378    〈labels, costs〉.
     379 [
     380 | @⊥
     381 | normalize % //
     382 ]
     383qed.
    382384
    383385definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.