 Timestamp:
 Jun 27, 2011, 2:17:25 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1038 r1044 91 91 qed. 92 92 93 lemma 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 ] 103 qed. 104 93 105 let rec lookup_opt (A: Type[0]) (n: nat) 94 106 (b: BitVector n) (t: BitVectorTrie A n) on t … … 122 134 qed. 123 135 136 lemma 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 ] 147 qed. 148 124 149 let rec lookup (A: Type[0]) (n: nat) 125 150 (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
Note: See TracChangeset
for help on using the changeset viewer.