Changeset 871


Ignore:
Timestamp:
May 31, 2011, 6:05:18 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r870 r871  
    351351  ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool.
    352352
     353(*
    353354definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
    354355  λP.
     
    427428  | @ (instruction_elim INSTR)
    428429  ].
    429  
     430*)
     431 
    430432(* This establishes the correspondence between pseudo program counters and
    431433   program counters. It is at the heart of the proof. *)
     
    550552   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
    551553    → False.
     554
     555lemma BitVectorTrie_O:
     556 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
     557 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     558  [ #w #_ %1 %[@w] %
     559  | #n #l #r #abs @⊥ //
     560  | #n #EQ %2 >EQ %]
     561qed.
     562
     563lemma BitVectorTrie_Sn:
     564 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
     565 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     566  [ #m #abs @⊥ //
     567  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
     568  | #m #EQ %2 // ]
     569qed.
     570
     571lemma lookup_prepare_trie_for_insertion_hit:
     572 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
     573  lookup … b (prepare_trie_for_insertion … b v) a = v.
     574 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     575qed.
     576 
     577lemma lookup_insert_hit:
     578 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     579  lookup … b (insert … b v t) a = v.
     580 #A #a #v #n #b elim b -b -n //
     581 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
     582  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
     583  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     584qed.
     585
     586lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     587 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     588 #n #hd #tl #abs @⊥ //
     589qed.
     590
     591lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
     592 ∃hd.∃tl.v ≃ VCons bool n hd tl.
     593 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     594 [ #abs @⊥ //
     595 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     596qed.
     597
     598lemma lookup_prepare_trie_for_insertion_miss:
     599 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
     600  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
     601 #A #a #v #n #c elim c
     602  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     603  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     604    cases hd cases hd' normalize
     605    [2,3: #_ cases tl' //
     606    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
     607qed.
     608 
     609lemma lookup_insert_miss:
     610 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     611  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
     612 #A #a #v #n #c elim c -c -n
     613  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     614  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     615    #t cases(BitVectorTrie_Sn … t)
     616    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     617     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     618    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     619     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     620     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
     621qed.
    552622
    553623definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.