include "infrastructure.ma".

inductive tag : Type[0] := a : tag | b : tag | c : tag.

definition tags : list tag ≝ [a;b;c].

definition type_of_tag : ∀T:Type[0]. tag → Type[0] ≝
 λT,t. match t with [ a ⇒ T | b ⇒ nat | c ⇒ bool ].

record test (T:Type[0]) : Type[0] ≝
 { A_:option (type_of_tag T a); B_: option (type_of_tag T b); C_: option (type_of_tag T c) }.

definition mk_test ≝ mk_test.

definition proj_of_tag: ∀t:tag. ∀T:Type[0]. test T → option (type_of_tag T t) ≝
 λt. match t with [ a ⇒ A_ | b ⇒ B_ | c ⇒ C_ ].

definition eq_tag : tag → tag → bool ≝
 λt1,t2.
  match t1 with
  [ a ⇒ match t2 with [a => true | _ => false]
  | b ⇒ match t2 with [b => true | _ => false]
  | c ⇒ match t2 with [c => true | _ => false]].

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

record sub_test (l: list tag) (T: Type[0]) : Type[0] ≝
{
  st_el :> test T;
  st_el_in: for_each ? (λt. defined … (proj_of_tag t … st_el)) l
}.

coercion sub_test : ∀l:list tag. Type[0] → Type[0]
 ≝ sub_test 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 proj:
 ∀t:tag. ∀l:list tag. memb Tag t l → ∀T:Type[0]. l T → type_of_tag T t
≝
 λt,l,H,T,r.
  match proj_of_tag t … r return λr. defined ? r → type_of_tag T t with
  [ None ⇒ λH:False.?
  | Some v ⇒ λH:True.v] ?.
[2: cases H
| lapply (st_el_in …r) inversion (for_each ???) [2: #_ #abs cases abs]
  #K #_ lapply (for_each_to_memb_to_true ???? H K) #X >X %]
qed.

definition A: ∀l:list tag. memb Tag a l → ∀T:Type[0]. l T → T ≝ proj a.
definition B: ∀l:list tag. memb Tag b l → ∀T:Type[0]. l T → nat ≝ proj b.
definition C: ∀l:list tag. memb Tag c l → ∀T:Type[0]. l T → bool ≝ proj c.

let rec type_of_build_test0 (tags: list tag) (l:list tag) (T:Type[0]) on tags: Type[0] ≝
 match tags with
 [ nil ⇒ l T
 | cons hd tl ⇒
    if memb Tag hd l then
     (type_of_tag T hd → type_of_build_test0 tl l T)
    else
     type_of_build_test0 tl l T ].

definition type_of_build_test: list tag → Type[0] → Type[0] ≝
 type_of_build_test0 tags.

let rec type_of_mk_test0 (tags: list tag) (T:Type[0]) on tags: Type[0] ≝
 match tags with
 [ nil ⇒ test T
 | cons hd tl ⇒ option (type_of_tag T hd) → type_of_mk_test0 tl T].

let rec mk_test0_ok (tags: list tag) (l:list tag) (T:Type[0]) on tags :
 type_of_mk_test0 tags T → Prop ≝
 match tags return λtags.type_of_mk_test0 tags T → Prop with
 [ nil ⇒ λr:test T. bool_to_Prop (for_each ? (λt. defined … (proj_of_tag t … r)) l)
 | cons hd tl ⇒ λr:option (type_of_tag T hd) → type_of_mk_test0 tl T.
    if memb Tag hd l then
     ∀x:type_of_tag T hd. mk_test0_ok tl l T (r (Some … x))
    else
     mk_test0_ok tl l T (r (None …))
 ].

let rec build_test0 (tags: list tag) (l:list tag) (T:Type[0]) on tags :
 ∀mk_record:type_of_mk_test0 tags T.
  mk_test0_ok tags l T mk_record → type_of_build_test0 tags l T
≝
 match tags
  return λtags.
   ∀mk_record:type_of_mk_test0 tags T.
    mk_test0_ok tags l T mk_record → type_of_build_test0 tags l T
 with
 [ nil ⇒ λr,r_ok.?
 | cons hd tl ⇒ λmk_record,mk_record_ok.
    match memb Tag hd l return λb. b=memb Tag hd l → if b then ? else ? with
    [ true ⇒ λH.λv. build_test0 tl l T (mk_record (Some ? v)) ?
    | false ⇒ λH.build_test0 tl l T (mk_record (None …)) ?] (refl … (memb Tag hd l))].
[ %{r} @r_ok
|2,3: whd in mk_record_ok; <H in mk_record_ok; // ]
qed.

 (*CSC: This needs to be proved every time :-( *)
axiom mk_test_ok: ∀l: list tag. ∀T:Type[0]. mk_test0_ok tags l T (mk_test T).

definition build_test: ∀l:list tag. ∀T:Type[0]. type_of_build_test l T ≝
 λl,T. build_test0 tags l T (mk_test …) ?.
// qed.

example xxx: [a; c] True ≝ build_test [a;c] … I true.
example xxx_c: C … xxx = true. // qed.
(*CSC: here we need a lemma! *)
example xxx_sub: [a;b] True → [a] True.
 #x %{x} cases x #y whd in ⊢ (% → %); whd in match (for_each ???);
 cases (for_each ???) [#X @X | #X cases X]
qed.