source: Papers/polymorphic-variants-2012/test.ma @ 2402

include "basics/lists/listb.ma".

definition bool_to_Prop : bool → Prop ≝
 λb. match b with [ true ⇒ True | false ⇒ False ].

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.

inductive tag : Type[0] := num : tag | plus : tag | mul : tag.

definition eq_tag : tag -> tag -> bool :=
 λt1,t2.
  match t1 with
  [ num => match t2 with [num => true | _ => false]
  | plus => match t2 with [plus => true | _ => false]
  | mul => match t2 with [mul => true | _ => false]].

definition Tag : DeqSet ≝ mk_DeqSet tag eq_tag ?.
 ** normalize /2/ % #abs destruct
qed.

definition tag_of_expr : ∀E:Type[0]. expr E -> tag :=
 λE,e.
   match e with
   [ Num _ => num
   | Plus _ _ => plus
   | Mul _ _ => mul ].

(*definition is_a : ∀E: Type[0]. tag -> expr E -> Prop ≝
 λE,t,e. eq_tag t (tag_of_expr \ldots e).*)

definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
 λE,l,e. memb Tag (tag_of_expr ? e) l. 

record sub_expr (l: list tag) (E: Type[0]) : Type[0] ≝
{
  se_el :> expr E;
  se_el_in: bool_to_Prop (is_in … l se_el)
}.

coercion sub_expr : ∀l:list tag. Type[0] → Type[0]
 ≝ sub_expr on _l: list tag to Type[0] → Type[0].

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 ? ?.

(**************************************)

definition additive_expr : Type[0] → Type[0] ≝ λE. [plus] E.