Changeset 2403


Ignore:
Timestamp:
Oct 18, 2012, 3:57:33 PM (7 years ago)
Author:
sacerdot
Message:

More work, example almost finished up to recursive type.

File:
1 edited

Legend:

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

    r2402 r2403  
    44 λb. match b with [ true ⇒ True | false ⇒ False ].
    55
     6coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     7
    68inductive expr (E: Type[0]) : Type[0] ≝
    79   Num : nat -> expr E
    8  | Plus : expr E -> expr E -> expr E
    9  | Mul : expr E -> expr E -> expr E.
     10 | Plus : E -> E -> expr E
     11 | Mul : E -> E -> expr E.
    1012
    1113inductive tag : Type[0] := num : tag | plus : tag | mul : tag.
     
    3840{
    3941  se_el :> expr E;
    40   se_el_in: bool_to_Prop (is_in … l se_el)
     42  se_el_in: is_in … l se_el
    4143}.
    4244
     
    4648coercion mk_sub_expr :
    4749 ∀l:list tag.∀E.∀e:expr E.
    48   ∀p:bool_to_Prop (is_in ? l e).sub_expr l E
    49  ≝ mk_sub_expr on e:expr E to sub_expr ? ?.
     50  ∀p:is_in ? l e.sub_expr l E
     51 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.
    5052
    5153(**************************************)
    5254
    53 definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.
     55definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝
     56 λE,f,e.
     57  match e return λe. is_in … [plus] e → nat with
     58  [ Plus x y ⇒ λH. f x + f y
     59  | _ ⇒ λH:False. ?
     60  ] (se_el_in ?? e).
     61elim H qed.
     62
     63definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝
     64 λE,f,e.
     65  match e return λe. is_in … [mul] e → nat with
     66  [ Mul x y ⇒ λH. f x + f y
     67  | _ ⇒ λH:False. ?
     68  ] (se_el_in ?? e).
     69elim H qed.
     70
     71definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝
     72 λE,f,e.
     73  match e return λe. is_in … [plus;mul] e → nat with
     74  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
     75  | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
     76  | _ ⇒ λH:False. ?
     77  ] (se_el_in ?? e).
     78[2,3: % | elim H]
     79qed.
Note: See TracChangeset for help on using the changeset viewer.