include "infrastructure.ma".

inductive expr (E: Type[0]) : Type[0] ≝
   Num : nat -> expr E
 | Plus : E -> E -> expr E
 | Mul : E -> 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 Q_holds_for_tag:
 ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝
 λE,Q,t.
  match t with
    [ num  ⇒ ∀n.   Q (Num … n)
    | plus ⇒ ∀x,y. Q (Plus … x y)
    | mul  ⇒ ∀x,y. Q (Mul … x y)
    ].

theorem Q_holds_for_tag_spec:
 ∀E:Type[0]. ∀Q: expr E → Prop.
  ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x.
#E #Q * normalize //
qed.