Changeset 2405 for Papers/polymorphic-variants-2012

Timestamp:

Oct 18, 2012, 5:29:44 PM (7 years ago)

Author:

sacerdot

Message:

Type of elimination principle generated + more lemmas.

File:

• Papers/polymorphic-variants-2012/test.ma (modified) (1 diff)

Papers/polymorphic-variants-2012/test.ma

@@ -50 +50 @@
   ∀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.
+
+
 
 (**************************************)