Changeset 2405 for Papers/polymorphic-variants-2012
- Timestamp:
- Oct 18, 2012, 5:29:44 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/test.ma
r2404 r2405 50 50 ∀p:is_in ? l e.sub_expr l E 51 51 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?. 52 53 let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝ 54 match l1 with 55 [ nil ⇒ true 56 | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ]. 57 58 lemma sublist_hd_tl_to_memb: 59 ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. 60 sublist S (hd::tl) l2 → memb S hd l2. 61 #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // 62 qed. 63 64 lemma sublist_hd_tl_to_sublist: 65 ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2. 66 sublist S (hd::tl) l2 → sublist S tl l2. 67 #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H 68 qed. 69 70 let rec sub_expr_elim_type 71 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E) 72 (Q: fixed_l E → Prop) 73 (l: list tag) 74 on l : sublist Tag l fixed_l → Prop ≝ 75 match l return λl. sublist Tag l fixed_l → Prop with 76 [ nil ⇒ λH. Q orig 77 | cons hd tl ⇒ λH. 78 let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in 79 match hd return λt. memb Tag t fixed_l → Prop with 80 [ num ⇒ λH. (∀n. Q (Num … n)) → tail_call 81 | plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call 82 | mul ⇒ λH. (∀x,y. Q (Mul … x y)) → tail_call 83 ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)]. 84 /2/ qed. 85 86 52 87 53 88 (**************************************)
Note: See TracChangeset
for help on using the changeset viewer.