Changeset 2406 for Papers/polymorphicvariants2012
 Timestamp:
 Oct 18, 2012, 6:35:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/test.ma
r2405 r2406 68 68 qed. 69 69 70 lemma 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 79 qed. 80 81 lemma 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 ???) // 89 qed. 90 91 lemma sublist_refl: ∀S:DeqSet. ∀l: list S. sublist S l l. 92 #S #l elim l [//] #hd #tl #IH normalize >(\b ?) // 93 qed. 94 70 95 let rec sub_expr_elim_type 71 96 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E) … … 84 109 /2/ qed. 85 110 111 lemma 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/ 118 qed. 86 119 120 theorem 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; // 126 qed. 87 127 88 128 (**************************************)
Note: See TracChangeset
for help on using the changeset viewer.