Changeset 2405 for Papers/polymorphic-variants-2012

Ignore:
Timestamp:
Oct 18, 2012, 5:29:44 PM (8 years ago)
Message:

Type of elimination principle generated + more lemmas.

File:
1 edited

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

 r2404 ∀p:is_in ? l e.sub_expr l E ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝ match l1 with [ nil ⇒ true | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ]. lemma sublist_hd_tl_to_memb: ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. sublist S (hd::tl) l2 → memb S hd l2. #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // qed. lemma sublist_hd_tl_to_sublist: ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. sublist S (hd::tl) l2 → sublist S tl l2. #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H qed. let rec sub_expr_elim_type (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E) (Q: fixed_l E → Prop) (l: list tag) on l : sublist Tag l fixed_l → Prop ≝ match l return λl. sublist Tag l fixed_l → Prop with [ nil ⇒ λH. Q orig | cons hd tl ⇒ λH. let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in match hd return λt. memb Tag t fixed_l → Prop with [ num  ⇒ λH. (∀n.   Q (Num … n))    → tail_call | plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call | mul  ⇒ λH. (∀x,y. Q (Mul … x y))  → tail_call ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)]. /2/ qed. (**************************************)
Note: See TracChangeset for help on using the changeset viewer.