Changeset 2406 for Papers


Ignore:
Timestamp:
Oct 18, 2012, 6:35:36 PM (7 years ago)
Author:
sacerdot
Message:

Elimination principle committed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/test.ma

    r2405 r2406  
    6868qed.
    6969
     70lemma sublist_insert_snd_pos:
     71 ∀S:DeqSet. ∀x,y:S. ∀l1,l2:list S.
     72  sublist S l1 (x::l2) → sublist S l1 (x::y::l2).
     73 #S #x #y #l1 elim l1 [//]
     74 #hd #tl #IH #l2 #H
     75 lapply (sublist_hd_tl_to_sublist … H) #K
     76 whd in match (sublist ???); >(?:hd∈x::y::l2 = true) /2/
     77 lapply (sublist_hd_tl_to_memb … H) normalize cases (hd==x) normalize //
     78 cases (hd==y) normalize // cases (hd∈l2) // #H cases H
     79qed.
     80
     81lemma sublist_tl_hd_tl:
     82 ∀S:DeqSet. ∀hd:S. ∀tl:list S. sublist S tl (hd::tl).
     83 #S #hd #tl elim tl try %
     84 #hd' #tl' #IH whd in match (sublist ???);
     85 whd in match (hd' ∈ hd::?::?); cases (hd'==hd)
     86 whd in match (hd' ∈ ?::?); >(\b ?) try % normalize
     87 lapply (sublist_insert_snd_pos … hd' … IH)
     88 cases (sublist ???) //
     89qed.
     90
     91lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l.
     92 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) //
     93qed.
     94
    7095let rec sub_expr_elim_type
    7196 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E)
     
    84109/2/ qed.
    85110
     111lemma sub_expr_elim0:
     112 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
     113  ∀l',H.
     114   (∀y:l E. ¬ is_in … l' y → Q y) →
     115    sub_expr_elim_type E l x Q l' H.
     116 #E #l #x #Q #l' elim l' /2/
     117 #hd #tl #IH cases hd #H #INV whd #P0 @IH ** /2/
     118qed.
    86119
     120theorem sub_expr_elim:
     121 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
     122  sub_expr_elim_type E l x Q l ?.
     123[2://
     124| #E #l #x #Q @sub_expr_elim0 * #y #H #NH
     125  cases (?: False) cases (is_in E l y) in H NH; //
     126qed.
    87127
    88128(**************************************)
Note: See TracChangeset for help on using the changeset viewer.