Changeset 1006


Ignore:
Timestamp:
Jun 20, 2011, 5:51:51 PM (8 years ago)
Author:
boender
Message:
  • added fold + lemmas on fold
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r990 r1006  
    99| Stub: ∀n: nat. BitVectorTrie A n.
    1010
    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.
     11let 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
     21qed.
     22
     23(* these two can probably be generalized w/r/t the second type and
     24 * some sort of equality relationship *)
     25lemma 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
     42qed.
     43 
     44lemma 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 ]
     60qed.
     61 
     62(* definition forall
     63 ≝
     64  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λ_.λa.λacc.(P a) ∧ acc) t True. *)
     65
     66definition 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 ]
     82qed.
     83 
     84lemma 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 ]
     95qed. *)
     96
     97lemma 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 ]
     109qed.
     110 
     111lemma 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 ]
     122qed.
    18123
    19124let rec lookup_opt (A: Type[0]) (n: nat)
     
    25130  | Stub _ ⇒ λ_.None ?
    26131  ]) b.
     132 
     133lemma 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
     153qed.
    27154
    28155let rec lookup (A: Type[0]) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.