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

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]. ∀l: list tag. ∀Q: ∀x: l E → Prop. ∀t:tag. memb … t l → Prop ≝
 λE,l,Q,t. ?.
  match t return λt. memb … t l → Prop with
    [ num  ⇒ λH. (∀n.   Q (Num … n))
    | plus ⇒ λH. (∀x,y. Q (Plus … x y))
    | mul  ⇒ λH. (∀x,y. Q (Mul … x y))
    ].


definition Q_holds_for_tag:
 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag. memb … t l → Prop ≝
 λE,l,Q,t. ?.
  match t return λt. memb … t l → Prop with
    [ num  ⇒ λH. (∀n.   Q (Num … n))
    | plus ⇒ λH. (∀x,y. Q (Plus … x y))
    | mul  ⇒ λH. (∀x,y. Q (Mul … x y))
    ].

axiom Q_holds_for_tag_spec:
 ∀E:Type[0]. ∀fixed_l: list tag. ∀Q: fixed_l E → Prop. ∀t:tag.
  ∀p:memb … t fixed_l. Q_holds_for_tag … Q … p →
   ∀x: [t] E. Q x.
*)