Ignore:
Timestamp:
Dec 2, 2012, 4:40:41 PM (7 years ago)
Author:
sacerdot
Message:

All .ma files committed: some of them are just in-progress.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Papers/polymorphic-variants-2012/test.ma

    r2406 r2514  
    1 include "basics/lists/listb.ma".
    2 
    3 definition bool_to_Prop : bool → Prop ≝
    4  λb. match b with [ true ⇒ True | false ⇒ False ].
    5 
    6 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     1include "infrastructure.ma".
    72
    83inductive expr (E: Type[0]) : Type[0] ≝
    … …  
    116 | Mul : E -> E -> expr E.
    127
    13 inductive tag : Type[0] := num : tag | plus : tag | mul : tag.
     8inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_.
    149
    15 definition eq_tag : tag -> tag -> bool :=
     10definition eq_tag : tag_ -> tag_ -> bool :=
    1611 λt1,t2.
    1712  match t1 with
    … …  
    2015  | mul => match t2 with [mul => true | _ => false]].
    2116
    22 definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
     17definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?.
    2318 ** normalize /2/ % #abs destruct
    2419qed.
    … …  
    3126   | Mul _ _ => mul ].
    3227
    33 (*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝
    34  λE,t,e. eq_tag t (tag_of_expr \ldots e).*)
     28(*
     29definition Q_holds_for_tag:
     30 ∀E:Type[0]. ∀l: list tag. ∀Q: ∀x: l E → Prop. ∀t:tag. memb … t l → Prop ≝
     31 λE,l,Q,t. ?.
     32  match t return λt. memb … t l → Prop with
     33    [ num  ⇒ λH. (∀n.   Q (Num … n))
     34    | plus ⇒ λH. (∀x,y. Q (Plus … x y))
     35    | mul  ⇒ λH. (∀x,y. Q (Mul … x y))
     36    ].
    3537
    36 definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
    37  λE,l,e. memb Tag (tag_of_expr ? e) l.
    3838
    39 record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝
    40 {
    41   se_el :> expr E;
    42   se_el_in: is_in … l se_el
    43 }.
     39definition Q_holds_for_tag:
     40 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝
     41 λE,l,Q,t. ?.
     42  match t return λt. memb … t l → Prop with
     43    [ num  ⇒ λH. (∀n.   Q (Num … n))
     44    | plus ⇒ λH. (∀x,y. Q (Plus … x y))
     45    | mul  ⇒ λH. (∀x,y. Q (Mul … x y))
     46    ].
    4447
    45 coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
    46  ≝ sub_expr on _l: list tag to Type[0] → Type[0].
    47 
    48 coercion mk_sub_expr :
    49  ∀l:list tag.∀E.∀e:expr E.
    50   ∀p:is_in ? l e.sub_expr l E
    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 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 
    95 let rec sub_expr_elim_type
    96  (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E)
    97  (Q: fixed_l E → Prop)
    98  (l: list tag)
    99  on l : sublist Tag l fixed_l → Prop ≝
    100  match l return λl. sublist Tag l fixed_l → Prop with
    101  [ nil ⇒ λH. Q orig
    102  | cons hd tl ⇒ λH.
    103     let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in
    104     match hd return λt. memb Tag t fixed_l → Prop with
    105     [ num  ⇒ λH. (∀n.   Q (Num … n))    → tail_call
    106     | plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call
    107     | mul  ⇒ λH. (∀x,y. Q (Mul … x y))  → tail_call
    108     ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)].
    109 /2/ qed.
    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.
    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.
    127 
    128 (**************************************)
    129 
    130 definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝
    131  λE,f,e.
    132   match e return λe. is_in … [plus] e → nat with
    133   [ Plus x y ⇒ λH. f x + f y
    134   | _ ⇒ λH:False. ?
    135   ] (se_el_in ?? e).
    136 elim H qed.
    137 
    138 definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝
    139  λE,f,e.
    140   match e return λe. is_in … [mul] e → nat with
    141   [ Mul x y ⇒ λH. f x * f y
    142   | _ ⇒ λH:False. ?
    143   ] (se_el_in ?? e).
    144 elim H qed.
    145 
    146 definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝
    147  λE,f,e.
    148   match e return λe. is_in … [plus;mul] e → nat with
    149   [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
    150   | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
    151   | _ ⇒ λH:False. ?
    152   ] (se_el_in ?? e).
    153 [2,3: % | elim H]
    154 qed.
    155 
    156 definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝
    157  λE,f,e.
    158   match e return λe. is_in … [plus;mul;num] e → nat with
    159   [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
    160   | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
    161   | Num n ⇒ λH. n
    162   ] (se_el_in ?? e).
    163 % qed.
    164 
    165 (*CSC: not accepted :-(
    166 inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const.
     48axiom Q_holds_for_tag_spec:
     49 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag.
     50  ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p →
     51   ∀x: [t] E. Q x.
    16752*)
    168 
    169 inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.
    170 
    171 coercion K.
    172 
    173 let rec eval_final_expr e on e : nat ≝
    174  match e with
    175  [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e'].
    176 cases e' try #x try #y %
    177 qed.
    178 
    179 example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
    180 % qed.
Note: See TracChangeset for help on using the changeset viewer.