source: src/ASM/BitVectorTrie.ma @ 1044

Last change on this file since 1044 was 1044, checked in by boender, 8 years ago
  • more fold/forall stuff
File size: 16.7 KB
Line 
1include "basics/types.ma".
2
3include "utilities/option.ma".
4include "ASM/BitVector.ma".
5
6inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
7  Leaf: A → BitVectorTrie A O
8| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
9| Stub: ∀n: nat. BitVectorTrie A n.
10
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 
62definition forall
63 ≝
64  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
65 
66lemma forall_nodel:
67  ∀A:Type[0].
68  ∀n:nat.
69  ∀l,r.
70  ∀P:BitVector (S n) → A → Prop.
71  forall A (S n) (Node ? n l r) P → forall A n l (λx.λa.P (false:::x) a).
72 #A #n #l #r #P #Hl
73 whd @(fold_eq A n ? ? (fold A ? n (λk.λa.λacc.P (true:::k) a∧acc) r True) True)
74 [ //
75 | #n #t' #X #Y #HXY #HX %1
76   [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ]
77 | whd in Hl @Hl ]
78qed.
79 
80lemma forall_noder:
81  ∀A:Type[0].
82  ∀n:nat.
83  ∀l,r.
84  ∀P:BitVector (S n) → A → Prop.
85  forall A (S n) (Node ? n l r) P → forall A n r (λx.λa.P (true:::x) a).
86 #A #n #l #r #P #Hr
87 whd @(fold_init A n (λk.λa.λacc.P (false:::k) a∧acc) l) 
88 [ #n #t' #P #HP @(proj2 ? ? HP)
89 | @Hr
90 ]
91qed.
92
93lemma 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 ]
103qed.
104
105let rec lookup_opt (A: Type[0]) (n: nat)
106                (b: BitVector n) (t: BitVectorTrie A n) on t
107       : option A ≝
108 (match t return λx.λ_. BitVector x → option A with
109  [ Leaf l ⇒ λ_.Some ? l
110  | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l)
111  | Stub _ ⇒ λ_.None ?
112  ]) b.
113 
114lemma forall_lookup:
115 ∀A.
116  ∀n.
117  ∀t:BitVectorTrie A n.
118  ∀P:BitVector n → A → Prop.
119  forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a.
120 #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?)
121 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf)
122 | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b)
123   #hd #bla elim bla -bla #tl #Htl >Htl in Hb; #Hb cases hd in Hb;
124   [ #Hb normalize in Hb; @(Hr (λx.λa.f (true:::x) a) (refl ? h))
125     [ @(forall_noder A h l r f Hf)
126     | @Hb
127     ]
128   | #Hb normalize in Hb; @(Hl (λx.λa.f (false:::x) a) (refl ? h))
129     [ @(forall_nodel A h l r f Hf)
130     | @Hb
131     ]
132   ]
133 | #n #f #_ #Hf #a #b #Hb normalize in Hb; destruct
134qed.
135
136lemma 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 ]   
147qed.
148 
149let rec lookup (A: Type[0]) (n: nat)
150                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
151       : A ≝
152  (match b return λx.λ_. x = n → A with
153    [ VEmpty ⇒
154      (match t return λx.λ_. O = x → A with
155        [ Leaf l ⇒ λ_.l
156        | Node h l r ⇒ λK.⊥
157        | Stub s ⇒ λ_.a
158        ])
159    | VCons o hd tl ⇒
160      match t return λx.λ_. (S o) = x → A with
161        [ Leaf l ⇒ λK.⊥
162        | Node h l r ⇒
163           match hd with
164             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
165             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
166             ]
167        | Stub s ⇒ λ_. a]
168    ]) (refl ? n).
169  [1,2:
170    destruct
171  |*:
172    @ injective_S
173    //
174  ]
175qed.
176
177let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
178   match b with
179    [ VEmpty ⇒ Leaf A a
180    | VCons o hd tl ⇒
181      match hd with
182        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
183        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
184        ]
185    ].
186
187let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
188  (match b with
189    [ VEmpty ⇒ λ_. Leaf A a
190    | VCons o hd tl ⇒ λt.
191          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
192            [ Leaf l ⇒ λprf.⊥
193            | Node p l r ⇒ λprf.
194               match hd with
195                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
196                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
197                ]
198            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
199            ] (refl ? (S o))
200    ]).
201  [ destruct
202  |*:
203    @ injective_S
204    //
205  ]
206qed.
207 
208let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
209  (match b with
210    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
211                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
212                   | Stub _ ⇒ λ_. None ?
213                   | Node _ _ _ ⇒ λprf. ⊥
214                   ] (refl ? O)
215    | VCons o hd tl ⇒ λt.
216          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
217            [ Leaf l ⇒ λprf.⊥
218            | Node p l r ⇒ λprf.
219               match hd with
220                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
221                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
222                ]
223            | Stub p ⇒ λprf. None ?
224            ] (refl ? (S o))
225    ]).
226  [ 1,2: destruct
227  |*:
228    @ injective_S @sym_eq @prf
229  ]
230qed.
231
232let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝
233  match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with
234  [ Stub _ ⇒ λc. c
235  | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ]
236  | Node p l r ⇒
237    λc.
238    (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with
239    [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉))
240    | Stub _ ⇒ λprf. Node ? p l r
241    | Leaf _ ⇒ λabsd. ?
242    ] (refl ? (S p)))
243  ].
244  [1:
245      destruct(absd)
246  |2,3:
247      @ injective_S
248        assumption
249  ]
250qed.
251
252lemma BitVectorTrie_O:
253 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
254 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
255  [ #w #_ %1 %[@w] %
256  | #n #l #r #abs @⊥ destruct(abs)
257  | #n #EQ %2 >EQ %]
258qed.
259
260lemma BitVectorTrie_Sn:
261 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
262 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
263  [ #m #abs @⊥ destruct(abs)
264  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
265  | #m #EQ %2 // ]
266qed.
267
268lemma lookup_prepare_trie_for_insertion_hit:
269 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
270  lookup … b (prepare_trie_for_insertion … b v) a = v.
271 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
272qed.
273 
274lemma lookup_insert_hit:
275 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
276  lookup … b (insert … b v t) a = v.
277 #A #a #v #n #b elim b -b -n //
278 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
279  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
280  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
281qed.
282
283lemma lookup_prepare_trie_for_insertion_miss:
284 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
285  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
286 #A #a #v #n #c elim c
287  [ #b >(BitVector_O … b) normalize #abs @⊥ //
288  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
289    cases hd cases hd' normalize
290    [2,3: #_ cases tl' //
291    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
292qed.
293 
294lemma lookup_insert_miss:
295 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
296  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
297 #A #a #v #n #c elim c -c -n
298  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
299  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
300    #t cases(BitVectorTrie_Sn … t)
301    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
302     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
303    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
304     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
305     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
306qed.
307
308lemma lookup_stub:
309 ∀A.∀n.∀b.∀a.
310 lookup A n b (Stub A ?) a = a.
311 #A #n #b #a cases n in b ⊢ (??(??%%%?)?)
312 [ #b >(BitVector_O b) normalize @refl
313 | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
314   [ normalize @refl
315   | normalize @refl
316   ]
317 ]   
318qed.   
319
320lemma lookup_opt_lookup:
321  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
322  lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a.
323 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
324 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl
325 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X; -X; #tl #Hb
326   >Hb >Hb in H; cases hd
327   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
328   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
329   ]
330 | #n #B #_ #H #x normalize in H; destruct
331 ]
332qed.
333
334lemma lookup_opt_prepare_trie_for_insertion_hit:
335 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
336  lookup_opt … b (prepare_trie_for_insertion … b v) = Some A v.
337 #A #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
338qed.
339
340lemma lookup_opt_insert_hit:
341 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
342  lookup_opt … b (insert … b v t) = Some A v.
343 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?)
344 [ #x #b >(BitVector_O b) normalize @refl
345 | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
346   [ normalize @Hr
347   | normalize @Hl
348   ]
349 | #n' #b cases n' in b ⊢ ?
350   [ #b >(BitVector_O b) normalize @refl
351   | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd
352     normalize @lookup_opt_prepare_trie_for_insertion_hit
353   ]
354 ]
355qed.
356   
357lemma forall_insert_inv1:
358  ∀A.∀n.∀b.∀a.∀t.∀P.
359  forall A n (insert A n b a t) P → P b a.
360 #A #n #b #a #t #P #H @(forall_lookup ? ? (insert A n b a t))
361 [ @H
362 | >(lookup_opt_insert_hit A ? n b) @(refl ? (Some A a))
363 ]
364qed.
365
366lemma forall_insert_inv2a:
367  ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P.
368  lookup_opt A n b t = (None A)  → forall A n (insert A n b a t) P → forall A n t P.
369 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%)
370 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct
371 | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H
372   [ normalize in H; normalize
373     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … H)
374     [ #Hfold @(Hr tl (refl ? h) ? Hlookup Hfold)
375     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ?HP)) ]
376     ]
377   | normalize in H; normalize     
378     @(fold_eq … True)
379     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
380       [ #z #t' #X #HX @(proj2 ? ? HX)
381       | @H ]
382     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
383     | @(Hl tl (refl ? h) ? Hlookup) normalize
384       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
385       [ //
386       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
387       | @H
388       ]
389     ]
390   ]
391 | #n #b #_ #P #Hlookup #Hf normalize // ]
392qed. 
393
394lemma forall_insert_inv2b:
395  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop).
396  (∀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.
397 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?)
398 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ]
399 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf
400   [ normalize in Hf; normalize
401     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … Hf)
402     [ #Hfold @(Hr tl (refl ? h) ? HP Hfold)
403     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
404     ]
405   | normalize in H; normalize     
406     @(fold_eq … True)
407     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
408       [ #z #t' #X #HX @(proj2 ? ? HX)
409       | @Hf ]
410     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
411     | @(Hl tl (refl ? h) ? HP) normalize
412       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
413       [ //
414       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
415       | @Hf
416       ]
417     ]
418   ]
419 | #n #b #_ #P #Hlookup #Hf normalize // ]
420qed.
421
422lemma forall_prepare_tree_for_insertion:
423 ∀A:Type[0].∀h:nat.∀b:BitVector h.∀a:A.∀P.
424 P b a →
425 forall A h (prepare_trie_for_insertion A h b a) P.
426 #A #h #b elim b
427 [ #a #P #HP normalize %1 [ @HP | // ]
428 | #h #x #tl #Ha #a #P cases x #HP normalize @Ha @HP
429 ]
430qed.
431
432lemma forall_insert:
433  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P.
434  forall A n t P → P b a → forall A n (insert A n b a t) P.
435 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%)
436 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/
437 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #Hf #HP
438   [ normalize in Hf; normalize
439     @(fold_eq A … (fold A … (λx.λa0.λacc.P (true:::x) a0∧acc) r True) … Hf)
440     [ #Hp @(Hr tl (refl ? h) ? Hp HP)
441     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
442     ]
443   | normalize in Hf; normalize
444     @(fold_eq … True)
445     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0∧acc) l)
446       [ #z #t' #X #HX @(proj2 ? ? HX)
447       | @Hf ]
448     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
449     | @(Hl tl (refl ? h) ? ? HP)
450       normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
451       [ //
452       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
453       | @Hf
454       ]
455     ]
456   ]
457 | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%)
458   [ #b #P #Hf #HP normalize %1 [ @HP | // ]
459   | #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP)
460   ]
461 ]
462qed.   
Note: See TracBrowser for help on using the repository browser.