Changeset 1044


Ignore:
Timestamp:
Jun 27, 2011, 2:17:25 PM (8 years ago)
Author:
boender
Message:
  • more fold/forall stuff
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1038 r1044  
    9191qed.
    9292
     93lemma forall_node:
     94  ∀A.∀n.∀l,r.∀P:BitVector (S n) → A → Prop.
     95  forall A n l (λx.λa.P (false:::x) a) → forall A n r (λx.λa.P (true:::x) a) →
     96  forall A (S n) (Node ? n l r) P.
     97 #A #n #l #r #P #Hl #Hr
     98 normalize @(fold_eq … True)
     99 [ #_ @Hr
     100 | #x #t' #X #Y #HXY #HP %1 [ @(proj1 … HP) | @HXY @(proj2 … HP) ]
     101 | @Hl
     102 ]
     103qed.
     104
    93105let rec lookup_opt (A: Type[0]) (n: nat)
    94106                (b: BitVector n) (t: BitVectorTrie A n) on t
     
    122134qed.
    123135
     136lemma lookup_forall:
     137 ∀A:Type[0].∀n.∀t:BitVectorTrie A n.∀P:BitVector n → A → Prop. 
     138 (∀a:A.∀b:BitVector n.lookup_opt A n b t = Some ? a → P b a) → forall A n t P.
     139 #A #n #t elim t
     140 [ #x #P #HP normalize %1 [ @HP normalize @refl | // ]
     141 | #h #l #r #Hl #Hr #P #HP @forall_node
     142   [ @Hl #a #b #Hlookup @HP normalize @Hlookup
     143   | @Hr #a #b #Hlookup @HP normalize @Hlookup
     144   ]
     145 | #n #P #HP normalize //
     146 ]   
     147qed.
     148 
    124149let rec lookup (A: Type[0]) (n: nat)
    125150                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
Note: See TracChangeset for help on using the changeset viewer.