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

include "basics/lists/listb.ma".

definition bool_to_Prop : bool → Prop ≝
 λ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 : 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 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: 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:is_in ? l e.sub_expr l E
 ≝ mk_sub_expr on e:expr ? to sub_expr ? ?.

let rec sublist (S:DeqSet) (l1:list S) (l2:list S) on l1 : bool ≝
 match l1 with
 [ nil ⇒ true
 | cons hd tl ⇒ memb S hd l2 ∧ sublist S tl l2 ].
 
lemma sublist_hd_tl_to_memb:
 ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2.
  sublist S (hd::tl) l2 → memb S hd l2.
 #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize //
qed.

lemma sublist_hd_tl_to_sublist:
 ∀S:DeqSet. ∀hd:S. ∀tl:list S. ∀l2.
  sublist S (hd::tl) l2 → sublist S tl l2.
 #S #hd #tl #l2 normalize cases (hd ∈ l2) normalize // #H cases H
qed.

let rec sub_expr_elim_type
 (E:Type[0]) (fixed_l: list tag) (orig: fixed_l E)
 (Q: fixed_l E → Prop)
 (l: list tag)
 on l : sublist Tag l fixed_l → Prop ≝
 match l return λl. sublist Tag l fixed_l → Prop with
 [ nil ⇒ λH. Q orig
 | cons hd tl ⇒ λH.
    let tail_call ≝ sub_expr_elim_type E fixed_l orig Q tl ? in
    match hd return λt. memb Tag t fixed_l → Prop with
    [ num  ⇒ λH. (∀n.   Q (Num … n))    → tail_call
    | plus ⇒ λH. (∀x,y. Q (Plus … x y)) → tail_call
    | mul  ⇒ λH. (∀x,y. Q (Mul … x y))  → tail_call
    ] (sublist_hd_tl_to_memb Tag hd tl fixed_l H)].
/2/ qed.



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

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.

definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝
 λE,f,e.
  match e return λe. is_in … [plus;mul;num] 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)
  | Num n ⇒ λH. n
  ] (se_el_in ?? e).
% qed.

(*CSC: not accepted :-(
inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. 
*)

inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr.

coercion K.

let rec eval_final_expr e on e : nat ≝
 match e with
 [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e'].
cases e' try #x try #y %
qed.

example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6.
% qed.