Changeset 2303 for src/common/PositiveMap.ma
 Timestamp:
 Aug 24, 2012, 5:41:18 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/PositiveMap.ma
r2104 r2303 1 1 include "basics/types.ma". 2 2 include "utilities/binary/positive.ma". 3 include "ASM/Util.ma". (* bool_to_Prop *) 3 4 4 5 inductive positive_map (A:Type[0]) : Type[0] ≝ … … 292 293 *: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi // 293 294 ] qed. 295 296 (* Testing all of the entries with a boolean predicate, where the predicate 297 is given a proof that the entry is in the map. *) 298 299 let rec pm_all_aux (A:Type[0]) (m,t:positive_map A) (pre:Pos → Pos) on t : (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool ≝ 300 match t return λt. (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool with 301 [ pm_leaf ⇒ λ_.λ_. true 302  pm_node a l r ⇒ λH,f. 303 pm_all_aux A m l (λx. pre (p0 x)) ? f ∧ 304 ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true  Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧ 305 pm_all_aux A m r (λx. pre (p1 x)) ? f 306 ]. 307 [ >H % 308  #p >H % 309  #p >H % 310 ] qed. 311 312 definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝ 313 λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f. 314 315 (* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can 316 use the function graph to show that it's fine. *) 317 318 inductive pm_all_pred_graph : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. bool → Prop ≝ 319  pmallpg : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. pm_all_pred_graph A m p a L f (f p a L). 320 321 lemma pm_all_pred_irr : ∀A,m,p,a,L,L'. 322 ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. 323 f p a L = f p a L'. 324 #A #m #p #a #L #L' #f 325 cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ] 326 cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H  1,4: skip] 327 * // 328 qed. 329 330 lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L. 331 pm_all_aux A m t pre H f → 332 lookup_opt A one t = Some A a → 333 f (pre one) a L. 334 #A #m * 335 [ #pre #H #f #a #L #H #L' normalize in L'; destruct 336  * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct 337  #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct 338 cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX') 339 #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr 340 ] 341 ] qed. 342 343 lemma pm_all_aux_ok : ∀A,m,t,pre,H,f. 344 bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H). 345 #A #m #t #pre #H #f % 346 [ #H' #p generalize in match pre in H H' ⊢ %; pre generalize in match t; elim p 347 [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux // 348  #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct 349  #x #l #r #pre #H #H' #a #L @(IH r) 350 [ #x >H %  cases (andb_Prop_true … H') #_ // ] 351 ] 352  #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct 353  #x #l #r #pre #H #H' #a #L @(IH l) 354 [ #x >H %  cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ] 355 ] 356 ] 357  #H' generalize in match pre in H H' ⊢ %; pre elim t 358 [ // 359  * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop 360 [ 1,3: @andb_Prop 361 [ 1,3: @IHl // 362  @(H' one x) 363  % 364 ] 365  2,4: @IHr // 366 ] 367 ] 368 ] qed. 369 370 lemma pm_all_ok : ∀A,m,f. 371 bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H). 372 #A #m #f @pm_all_aux_ok 373 qed. 374
Note: See TracChangeset
for help on using the changeset viewer.