 Timestamp:
 Jun 20, 2011, 5:51:51 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r990 r1006 9 9  Stub: ∀n: nat. BitVectorTrie A n. 10 10 11 axiom fold: 12 ∀A, B: Type[0]. 13 ∀n: nat. 14 ∀f: BitVector n → A → B → B. 15 ∀t: BitVectorTrie A n. 16 ∀b: B. 17 B. 11 let rec fold (A, B: Type[0]) (n: nat) (f: BitVector n → A → B → B) 12 (t: BitVectorTrie A n) (b: B) on t: B ≝ 13 (match t return λx.λ_.x = n → B with 14 [ Leaf l ⇒ λ_.f (zero ?) l b 15  Node h l r ⇒ λK. 16 fold A B h (λx.f ((VCons ? h false x)⌈(S h) ↦ n⌉)) l 17 (fold A B h (λx.f ((VCons ? h true x)⌈(S h) ↦ n⌉)) r b) 18  Stub _ ⇒ λ_.b 19 ]) (refl ? n). 20 @K 21 qed. 22 23 (* these two can probably be generalized w/r/t the second type and 24 * some sort of equality relationship *) 25 lemma fold_eq: 26 ∀A: Type[0]. 27 ∀n: nat. 28 ∀f. 29 ∀t. 30 ∀P, Q: Prop. 31 (P → Q) → (∀a,t',P,Q.(P → Q) → f a t' P → f a t' Q) → fold A ? n f t P → fold A ? n f t Q. 32 #A #n #f #t #P #Q #H 33 generalize in match (refl ? n) generalize in match H H; generalize in match Q Q; generalize in match P P; 34 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?) 35 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP) 36  #h #l #r #Hl #Hr #f #P #Q #HPQ #_ #Hf #HP normalize normalize in HP; @(Hl ? (fold A Prop h (λx.f (true:::x)) r P) (fold A Prop h (λx.f (true:::x)) r Q) ? (refl ? h) ?) 37 [ @(Hr ? P Q HPQ (refl ? h) ?) 38 #a #t' #X #Y #HXY #Hff @(Hf (true:::a) t' X Y HXY Hff) 39  #a #t' #X #Y #HXY #Hff @(Hf (false:::a) t' X Y HXY Hff) ] 40  #h #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(HPQ HP) ] 41 @HP 42 qed. 43 44 lemma fold_init: 45 ∀A:Type[0]. 46 ∀n:nat. 47 ∀f. 48 ∀t. 49 ∀P: Prop. 50 (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P. 51 #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H H; generalize in match P P; 52 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) t 53 [ #a #f #P #Hf #_ normalize @(Hf [[]]) 54  #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x))) 55 [ #a #t' #X @(Hf (true:::a) t' X)  @(refl ? h)  @(Hl (λx.f (false:::x))) 56 [ #a #t' #X @(Hf (false:::a) t' X)  @(refl ? h)  @HP ] 57 ] 58  #h #f #P #Hf #_ normalize // 59 ] 60 qed. 61 62 (* definition forall 63 ≝ 64 λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λ_.λa.λacc.(P a) ∧ acc) t True. *) 65 66 definition forall 67 ≝ 68 λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True. 69 70 (* lemma forall_nodel: 71 ∀A:Type[0]. 72 ∀n:nat. 73 ∀l,r. 74 ∀P:A → Prop. 75 forall A (S n) (Node ? n l r) P → forall A n l P. 76 #A #n #l #r #P generalize in match (refl ? n) #_ #Hl 77 whd in Hl; whd @(fold_eq A n ? ? (fold A ? n (λx.λa.λacc.P a∧acc) r True) True) 78 [ // 79  #n #t' #X #Y #HXY #HX %1 80 [ @(proj1 ? ? HX)  @HXY @(proj2 ? ? HX) ] 81  @Hl ] 82 qed. 83 84 lemma forall_noder: 85 ∀A:Type[0]. 86 ∀n:nat. 87 ∀l,r. 88 ∀P. 89 forall A (S n) (Node ? n l r) P → forall A n r P. 90 #A #n #l #r #P generalize in match (refl ? n) #_ #Hr 91 whd in Hr; whd @(fold_init A n (λx.λa.λacc.P a∧acc) l) 92 [ #n #t' #P #HP @(proj2 ? ? HP) 93  @Hr 94 ] 95 qed. *) 96 97 lemma forall_nodel: 98 ∀A:Type[0]. 99 ∀n:nat. 100 ∀l,r. 101 ∀P:BitVector (S n) → A → Prop. 102 forall A (S n) (Node ? n l r) P → forall A n l (λx.λa.P (false:::x) a). 103 #A #n #l #r #P #Hl 104 whd @(fold_eq A n ? ? (fold A ? n (λk.λa.λacc.P (true:::k) a∧acc) r True) True) 105 [ // 106  #n #t' #X #Y #HXY #HX %1 107 [ @(proj1 ? ? HX)  @HXY @(proj2 ? ? HX) ] 108  whd in Hl @Hl ] 109 qed. 110 111 lemma forall_noder: 112 ∀A:Type[0]. 113 ∀n:nat. 114 ∀l,r. 115 ∀P:BitVector (S n) → A → Prop. 116 forall A (S n) (Node ? n l r) P → forall A n r (λx.λa.P (true:::x) a). 117 #A #n #l #r #P #Hr 118 whd @(fold_init A n (λk.λa.λacc.P (false:::k) a∧acc) l) 119 [ #n #t' #P #HP @(proj2 ? ? HP) 120  @Hr 121 ] 122 qed. 18 123 19 124 let rec lookup_opt (A: Type[0]) (n: nat) … … 25 130  Stub _ ⇒ λ_.None ? 26 131 ]) b. 132 133 lemma forall_lookup: 134 ∀A. 135 ∀n. 136 ∀t:BitVectorTrie A n. 137 ∀P:BitVector n → A → Prop. 138 forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a. 139 #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?) 140 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf) 141  #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b) 142 #hd #bla elim bla bla #tl #Htl >Htl in Hb; #Hb cases hd in Hb; 143 [ #Hb normalize in Hb; @(Hr (λx.λa.f (true:::x) a) (refl ? h)) 144 [ @(forall_noder A h l r f Hf) 145  @Hb 146 ] 147  #Hb normalize in Hb; @(Hl (λx.λa.f (false:::x) a) (refl ? h)) 148 [ @(forall_nodel A h l r f Hf) 149  @Hb 150 ] 151 ] 152  #n #f #_ #Hf #a #b #Hb normalize in Hb; destruct 153 qed. 27 154 28 155 let rec lookup (A: Type[0]) (n: nat)
Note: See TracChangeset
for help on using the changeset viewer.