(*
include "infrastructure.ma".
axiom tag: DeqSet.
axiom expr: Type[0] → Type[0].
axiom tag_of_expr: ∀E:Type[0]. expr E → tag.
axiom Q_holds_for_tag: ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop.
axiom 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.
*)

include "test.ma".

definition is_in : ∀E: Type[0]. list tag -> expr E -> bool ≝
 λE,l,e. memb … (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 ? ?.

definition Q_of_Q':
 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. expr E → Prop ≝
 λE,l,Q,e.
  match memb … (tag_of_expr … e) l return λx. memb … (tag_of_expr … e) l = x → Prop with
  [ true ⇒ λH. Q e
  | false ⇒ λH. False
  ] (refl …).
whd in match (is_in ???); >H //
qed.

lemma Q_of_Q_ok':
 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀x:l E.
  Q_of_Q' E l Q x→Q x.
 #E #l #Q #x normalize
 @(dep_bool_match_elim (tag_of_expr E x ∈ l)) [2: #_ *]
 cases x #y #prf' #prf'' #H @H
qed.
  
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,p.
  Q_holds_for_tag E (Q_of_Q' … l Q') t.

theorem Q_holds_for_tag_spec':
 ∀E:Type[0]. ∀l: list tag. ∀Q: l E → Prop. ∀t:tag.
  ∀p:memb … t l. Q_holds_for_tag' … Q … p →
   ∀x: [t] E. Q x.
[2: cases x #y #H @(memb_to_sublist_to_memb … H) whd in match (sublist ???);
    cases (memb ???) in p; //
| #E #l #Q #t #p whd in match Q_holds_for_tag'; normalize nodelta #H #x
  cut (t = tag_of_expr … x)
  [ cases x -x #x #EQ whd in EQ; inversion (is_in E [t] x) in EQ;
    normalize nodelta
    [2: #_ #abs cases abs] whd in ⊢ (??%? → ? → ?);
    inversion (tag_of_expr E x == t) [2: #_ normalize #abs destruct]
    #EQ #_ #_ <(\P EQ) %
  | #EQ2 lapply H >EQ2 in ⊢ (% → ?); #K lapply(Q_holds_for_tag_spec … K)
    cut (tag_of_expr E x ∈ l) // #K1 #K2 @(Q_of_Q_ok' E l Q x)
    cases x in K2; // ]]
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 … l fixed_l → Prop ≝
 match l return λl. sublist … 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
     Q_holds_for_tag' … fixed_l Q hd (sublist_hd_tl_to_memb … hd tl fixed_l H) →
      tail_call ].
/2/ qed.

lemma sub_expr_elim0:
 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
  ∀l',H.
   (∀y:l E. ¬ is_in … l' y → Q y) →
    sub_expr_elim_type E l x Q l' H.
 #E #l #x #Q #l' elim l' /2/
 #hd #tl #IH (*cases hd*) #H #INV whd #P0 @IH #y
 whd in match (is_in ???) in INV:%;
 lapply (Q_holds_for_tag_spec' … P0) #K1 #K2
 inversion (tag_of_expr … y == hd) #K3
 [ lapply (K1 y)
   [ whd in match (is_in ???); >K3 %
   | cases y in K3; // ]
 | @INV whd in match (is_in ???); >K3 // ]
qed.

theorem sub_expr_elim:
 ∀E:Type[0]. ∀l: list tag. ∀x: l E. ∀Q: l E → Prop.
  sub_expr_elim_type E l x Q l ?.
[2://
| #E #l #x #Q @sub_expr_elim0 * #y #H #NH
  cases (?: False) cases (is_in E l y) in H NH; //
qed.