Changeset 1044 for src/ASM/BitVectorTrie.ma
- Timestamp:
- Jun 27, 2011, 2:17:25 PM (8 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.