Changeset 2403 for Papers/polymorphic-variants-2012

Timestamp:

Oct 18, 2012, 3:57:33 PM (9 years ago)

Author:

sacerdot

Message:

More work, example almost finished up to recursive type.

File:

• Papers/polymorphic-variants-2012/test.ma (modified) (3 diffs)

Papers/polymorphic-variants-2012/test.ma

@@ -4 +4 @@
  λb. match b with [ true ⇒ True | false ⇒ False ].
 
+coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
+
 inductive expr (E: Type[0]) : Type[0] ≝
    Num : nat -> expr E
- | Plus : expr E -> expr E -> expr E
- | Mul : expr E -> expr E -> expr E.
+ | Plus : E -> E -> expr E
+ | Mul : E -> E -> expr E.
 
 inductive tag : Type[0] := num : tag | plus : tag | mul : tag.
@@ -38 +40 @@
 {
   se_el :> expr E;
-  se_el_in: bool_to_Prop (is_in … l se_el)
+  se_el_in: is_in … l se_el
 }.
 
@@ -46 +48 @@
 coercion mk_sub_expr :
  ∀l:list tag.∀E.∀e:expr E.
-  ∀p:bool_to_Prop (is_in ? l e).sub_expr l E
- ≝ mk_sub_expr on e:expr E to sub_expr ? ?.
+  ∀p:is_in ? l e.sub_expr l E
+ ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.
 
 (**************************************)
 
-definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.
+definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝
+ λE,f,e.
+  match e return λe. is_in … [plus] e → nat with
+  [ Plus x y ⇒ λH. f x + f y
+  | _ ⇒ λH:False. ?
+  ] (se_el_in ?? e).
+elim H qed.
+
+definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝
+ λE,f,e.
+  match e return λe. is_in … [mul] e → nat with
+  [ Mul x y ⇒ λH. f x + f y
+  | _ ⇒ λH:False. ?
+  ] (se_el_in ?? e).
+elim H qed.
+
+definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝
+ λE,f,e.
+  match e return λe. is_in … [plus;mul] e → nat with
+  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y)
+  | Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y)
+  | _ ⇒ λH:False. ?
+  ] (se_el_in ?? e).
+[2,3: % | elim H]
+qed.