Changeset 2405


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

Type of elimination principle generated + more lemmas.

File:
1 edited

Legend:

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

    r2404 r2405  
    5050  ∀p:is_in ? l e.sub_expr l E
    5151 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.
     52
     53let 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 
     58lemma 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 //
     62qed.
     63
     64lemma 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
     68qed.
     69
     70let 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
    5287
    5388(**************************************)
Note: See TracChangeset for help on using the changeset viewer.