Ignore:
Timestamp:
Jun 22, 2011, 4:03:33 PM (8 years ago)
Author:
boender
Message:

various & sundry fold/forall lemmas

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1006 r1034  
    6060qed.
    6161 
    62 (* definition forall
    63  ≝
    64   λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λ_.λa.λacc.(P a) ∧ acc) t True. *)
    65 
    6662definition forall
    6763 ≝
    6864  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
    6965 
    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 
    9766lemma forall_nodel:
    9867  ∀A:Type[0].
     
    211180  ]
    212181qed.
    213 
     182 
    214183let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
    215184  (match b with
     
    311280     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    312281qed.
     282
     283lemma lookup_stub:
     284 ∀A.∀n.∀b.∀a.
     285 lookup A n b (Stub A ?) a = a.
     286 #A #n #b #a cases n in b ⊢ (??(??%%%?)?)
     287 [ #b >(BitVector_O b) normalize @refl
     288 | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
     289   [ normalize @refl
     290   | normalize @refl
     291   ]
     292 ]   
     293qed.   
     294
     295lemma lookup_opt_lookup:
     296  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
     297  lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a.
     298 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
     299 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl
     300 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X; -X; #tl #Hb
     301   >Hb >Hb in H; cases hd
     302   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
     303   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
     304   ]
     305 | #n #B #_ #H #x normalize in H; destruct
     306 ]
     307qed.
     308
     309lemma lookup_opt_prepare_trie_for_insertion_hit:
     310 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
     311  lookup_opt … b (prepare_trie_for_insertion … b v) = Some A v.
     312 #A #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     313qed.
     314
     315lemma lookup_opt_insert_hit:
     316 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     317  lookup_opt … b (insert … b v t) = Some A v.
     318 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?)
     319 [ #x #b >(BitVector_O b) normalize @refl
     320 | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
     321   [ normalize @Hr
     322   | normalize @Hl
     323   ]
     324 | #n' #b cases n' in b ⊢ ?
     325   [ #b >(BitVector_O b) normalize @refl
     326   | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd
     327     normalize @lookup_opt_prepare_trie_for_insertion_hit
     328   ]
     329 ]
     330qed.
     331   
     332lemma forall_insert_inv1:
     333  ∀A.∀n.∀b.∀a.∀t.∀P.
     334  forall A n (insert A n b a t) P → P b a.
     335 #A #n #b #a #t #P #H @(forall_lookup ? ? (insert A n b a t))
     336 [ @H
     337 | >(lookup_opt_insert_hit A ? n b) @(refl ? (Some A a))
     338 ]
     339qed.
     340
     341lemma forall_insert_inv2a:
     342  ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P.
     343  lookup_opt A n b t = (None A)  → forall A n (insert A n b a t) P → forall A n t P.
     344 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%)
     345 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct
     346 | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H
     347   [ normalize in H; normalize
     348     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … H)
     349     [ #Hfold @(Hr tl (refl ? h) ? Hlookup Hfold)
     350     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ?HP)) ]
     351     ]
     352   | normalize in H; normalize     
     353     @(fold_eq … True)
     354     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
     355       [ #z #t' #X #HX @(proj2 ? ? HX)
     356       | @H ]
     357     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
     358     | @(Hl tl (refl ? h) ? Hlookup) normalize
     359       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
     360       [ //
     361       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
     362       | @H
     363       ]
     364     ]
     365   ]
     366 | #n #b #_ #P #Hlookup #Hf normalize // ]
     367qed. 
     368
     369lemma forall_insert_inv2b:
     370  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop).
     371  (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P.
     372 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?)
     373 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ]
     374 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf
     375   [ normalize in Hf; normalize
     376     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … Hf)
     377     [ #Hfold @(Hr tl (refl ? h) ? HP Hfold)
     378     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
     379     ]
     380   | normalize in H; normalize     
     381     @(fold_eq … True)
     382     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
     383       [ #z #t' #X #HX @(proj2 ? ? HX)
     384       | @Hf ]
     385     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
     386     | @(Hl tl (refl ? h) ? HP) normalize
     387       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
     388       [ //
     389       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
     390       | @Hf
     391       ]
     392     ]
     393   ]
     394 | #n #b #_ #P #Hlookup #Hf normalize // ]
     395qed.
     396   
Note: See TracChangeset for help on using the changeset viewer.