Changeset 1044 for src/ASM/BitVectorTrie.ma

Timestamp:

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

Author:

boender

Message:

• more fold/forall stuff

File:

• src/ASM/BitVectorTrie.ma (modified) (2 diffs)

src/ASM/BitVectorTrie.ma

@@ -91 +91 @@
 qed.
 
+lemma forall_node:
+  ∀A.∀n.∀l,r.∀P:BitVector (S n) → A → Prop.
+  forall A n l (λx.λa.P (false:::x) a) → forall A n r (λx.λa.P (true:::x) a) →
+  forall A (S n) (Node ? n l r) P.
+ #A #n #l #r #P #Hl #Hr
+ normalize @(fold_eq … True)
+ [ #_ @Hr
+ | #x #t' #X #Y #HXY #HP %1 [ @(proj1 … HP) | @HXY @(proj2 … HP) ]
+ | @Hl
+ ]
+qed.
+
 let rec lookup_opt (A: Type[0]) (n: nat)
                 (b: BitVector n) (t: BitVectorTrie A n) on t
@@ -122 +134 @@
 qed.
 
+lemma lookup_forall:
+ ∀A:Type[0].∀n.∀t:BitVectorTrie A n.∀P:BitVector n → A → Prop.  
+ (∀a:A.∀b:BitVector n.lookup_opt A n b t = Some ? a → P b a) → forall A n t P.
+ #A #n #t elim t
+ [ #x #P #HP normalize %1 [ @HP normalize @refl | // ]
+ | #h #l #r #Hl #Hr #P #HP @forall_node
+   [ @Hl #a #b #Hlookup @HP normalize @Hlookup
+   | @Hr #a #b #Hlookup @HP normalize @Hlookup
+   ]
+ | #n #P #HP normalize //
+ ]   
+qed.
+ 
 let rec lookup (A: Type[0]) (n: nat)
                 (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b