Definition t (s : sort) := (s ~> bool)%con.
Definition union {s} : t s → t s → t s := function.zipWith orb.
Definition intersection {s} : t s → t s → t s := function.zipWith andb.
Definition disjoint_union {s1 s2} : t s1 → t s2 → t (s1 ∐ s2) := function.concat.

Definition empty {s} : t s := function.constant false.
Definition full {s} : t s := function.constant true.

Definition inhabited {s} : t s → bool := function.fold orb.


Definition injl {s1 s2} (u : t s1) : t (s1 ∐ s2) := u ⊎ ∅.
Definition injr {s1 s2} (u : t s2) : t (s1 ∐ s2) := ∅ ⊎ u.

Fixpoint singleton {s} : typeOf s → t s :=
  match s with
  | 𝟙 ⇒ fun _ ⇒ full
  | s1 ∐ s2 ⇒ fun u ⇒ match u with
                    | inl uL ⇒ injl (singleton uL)
                    | inr uR ⇒ injr (singleton uR)
                    end
  end.

Lemma union_empty_r {s}(a : t s) : a ∪ ∅ = a.
  apply function.extensionality ⇒ i.
  by rewrite /union zip_pointwise /empty constantE orbF.
Qed.

Lemma union_empty_l {s}(a : t s) : ∅ ∪ a = a.
  apply function.extensionality ⇒ i.
  by rewrite /union zip_pointwise /empty constantE orFb.
Qed.

Definition denote {s} (a : t s) : {set universe.denote s} := finset (function.denote a).


Lemma denoteE {s}(a : t s) : ∀ i, i \in denote a = a i.
  move ⇒ i; by rewrite /denote /function.denote in_set ffunE.
Qed.

Lemma disjULE {s1 s2}{a : t s1}{b : t s2} x : x \in denote a = (inl x \in denote (a ⊎ b)).
  apply/idP/idP.
  - by rewrite denoteE ⇒ h; rewrite (denoteE (a ⊎ b)) /disjoint_union //=.
  - by rewrite (denoteE (a ⊎ b)) //= -denoteE.
Qed.

Lemma disjURE {s1 s2}{a : t s1}{b : t s2} x : x \in denote b = (inr x \in denote (a ⊎ b)).
  apply/idP/idP.
  - by rewrite denoteE ⇒ h; rewrite (denoteE (a ⊎ b)) /disjoint_union //=.
  - by rewrite (denoteE (a ⊎ b)) //= -denoteE.
Qed.

Lemma union_spec {s}(a b : t s) : denote (a ∪ b) = denote a :|: denote b.
  apply/setP ⇒ x; by rewrite in_setU ?denoteE /union zip_pointwise.
Qed.


Lemma intersection_spec {s}(a b : t s) : denote (a ∩ b) = denote a :&: denote b.
  apply/setP ⇒ x; by rewrite in_setI ?denoteE /intersection zip_pointwise.
Qed.

Lemma empty_spec {s} : denote (@empty s) = set0.
  apply/setP ⇒ x; by rewrite /empty ?denoteE constantE in_set0.
Qed.

Lemma full_spec {s} : denote (@full s) = setT.
  apply/setP ⇒ x; by rewrite /empty ?denoteE constantE in_setT.
Qed.

Lemma inl_inj {A B : Type} : (injective (inl : A → A + B)).
  move ⇒ x y Hyp; by inversion Hyp.
Qed.

Lemma inr_inj {A B : Type} : (injective (inr : B → A + B)).
  move ⇒ x y Hyp; by inversion Hyp.
Qed.

Lemma injlinv_spec {s1 s2} (a : t s1) : inl @^-1: denote (injl (s2:=s2) a) = denote a.
  apply/setP ⇒ x; by rewrite ?denoteE ?in_set function.denoteE //=.
Qed.

Lemma injl_spec {s1 s2}(a : t s1) : denote (injl (s2:=s2) a) = inl @: denote a.
  rewrite /injl /disjoint_union -setP ⇒ x; case x ⇒ u.
  - rewrite (mem_imset _ _ (inl_inj)) ?in_set ?function.denoteE //=.
  - rewrite ?in_set ?function.denoteE /empty //= ?function.constantE //=.
    apply/idP/imsetP.
    + done.
    + case ⇒ y h1 h2; inversion h2.
Qed.

Lemma setUnit : [set: unit] = [set tt].
  apply/setP; by case; rewrite ?in_set in_set1 //=.
Qed.

Lemma injrinv_spec {s1 s2} (a : t s2) : inr @^-1: denote (injr (s1:=s1) a) = denote a.
  apply/setP ⇒ x; by rewrite ?denoteE ?in_set function.denoteE //=.
Qed.

Lemma injr_spec {s1 s2}(a : t s2) : denote (injr (s1:=s1) a) = inr @: denote a.
  rewrite /injr /disjoint_union -setP ⇒ x; case x ⇒ u.
  - rewrite ?in_set ?function.denoteE /empty //= ?function.constantE //=.
    apply/idP/imsetP.
    + done.
    + case ⇒ y h1 h2; inversion h2.
  - rewrite (mem_imset _ _ (inr_inj)) ?in_set ?function.denoteE //=.
Qed.

Lemma singleton_spec {s} : ∀ (a : typeOf s), denote (singleton a) = set1 a.
  move ⇒ a; apply/setP ⇒ x; rewrite ?denoteE ?in_set.
  induction s.
  - rewrite //=; case x; rewrite ?in_set1 //=.
  - destruct a; destruct x; rewrite //= ?IHs1 ?IHs2 ?in_set1 /empty //= ?constantE ?in_set1 //=.
Qed.

Lemma disUUU {s1 s2}(a1 a2 : t s1)(b1 b2 : t s2) : (a1 ∪ a2) ⊎ (b1 ∪ b2) = (a1 ⊎ b1) ∪ (a2 ⊎ b2).
  rewrite /disjoint_union /union; apply function.extensionality; case ⇒ x; rewrite //=.
Qed.

Lemma injDU {s1 s2}(a : t s1)(b : t s2) : a ⊎ b = injl a ∪ injr b.
  by rewrite /injl /injr -/disjoint_union -disUUU union_empty_l union_empty_r.
Qed.

Lemma inhabitedP {s} (A : t s) : reflect (∃ x, x \in denote A) (inhabited A).
  rewrite /inhabited.
  induction A.
  - case: a.
    + by apply ReflectT; ∃ tt; rewrite denoteE //=.
    + apply ReflectF; case ⇒ x; rewrite denoteE constantE //=.
  - rewrite /fold -/fold; apply /(iffP idP).
    + case/orP.
      × by case/IHA1 ⇒ x1 h1; ∃ (inl x1); rewrite -disjULE.
      × by case/IHA2 ⇒ x2 h2; ∃ (inr x2); rewrite -disjURE.
    + case ⇒ x; case: x ⇒ a; rewrite -?disjULE -?disjURE ⇒ h; apply/orP.
      × by left; apply/IHA1; ∃ a.
      × by right; apply/IHA2; ∃ a.
Qed.

Lemma inhabited_spec {s} (A : t s) : inhabited A = abstract.utils.inhabited (denote A).
  by apply /inhabitedP/existsP.
Qed.

Module big.

  Section Cxt.
    Context {idx s : sort}(F : idx ~> t s).

    Definition union (iset : t idx) : t s :=
      function.fold (@subset.union s) (function.zipWith (fun b S ⇒ if b then S else ∅) iset F).

    Definition intersection (iset : t idx)
      := function.fold (@subset.intersection s) (function.zipWith (fun b S ⇒ if b then S else full) iset F).

  End Cxt.

  Lemma bigcup_sum {idx1 idx2 s}(F1 : idx1 ~> t s) (F2 : idx2 ~> t s)(iset1 : t idx1) (iset2 : t idx2) :
    \bigcup_(i in denote (iset1 ++ iset2)) denote ((F1 ++ F2) i) =
      \bigcup_(i in denote iset1) denote (F1 i) :|: \bigcup_(i in denote iset2) denote (F2 i).
    apply /setP ⇒ x; rewrite in_setU; apply/bigcupP/orP.
    - case ⇒ i; case i ⇒ idx; rewrite -?disjULE -?disjURE //= ⇒ h1 h2.
      + by left; apply /bigcupP ; ∃ idx.
      + by right; apply /bigcupP; ∃ idx.
    - case; case /bigcupP ⇒ i h1 h2.
      + by ∃ (inl i); rewrite -?disjULE //=.
      + by ∃ (inr i); rewrite -?disjURE //=.
  Qed.

  Lemma bigcap_sum {idx1 idx2 s}(F1 : idx1 ~> t s) (F2 : idx2 ~> t s)(iset1 : t idx1) (iset2 : t idx2) :
    \bigcap_(i in denote (iset1 ++ iset2)) denote ((F1 ++ F2) i) =
      \bigcap_(i in denote iset1) denote (F1 i) :&: \bigcap_(i in denote iset2) denote (F2 i).
    apply/setP ⇒ x; rewrite in_setI. apply/bigcapP/andP.
    - move ⇒ h. apply conj; apply /bigcapP ⇒ i.
      + by rewrite (disjULE(b:=iset2)); apply (h (inl i)).
      + by rewrite (disjURE(a:=iset1)); apply (h (inr i)).
    - case; move/bigcapP ⇒ h1; move /bigcapP ⇒ h2 i; case i ⇒ idx; rewrite -?disjULE -?disjURE ⇒ h.
      + rewrite (disjULE (b:=iset2)) //= -?disjULE; intuition.
      + rewrite (disjURE (a:=iset2)) //= -?disjURE; intuition.
  Qed.

  Lemma union_spec {idx s}(F : idx ~> t s)(iset : t idx) :
    denote (big.union F iset) = \bigcup_ (i in denote iset) denote (F i).
    induction idx; dependent destruction iset; dependent destruction F.
    - case: b.
      × by rewrite full_spec setUnit big_set1E setU0.
      × by rewrite ?empty_spec big_set0.
    - by rewrite bigcup_sum -IHidx1 -IHidx2 -subset.union_spec.
  Qed.

  Lemma intersection_spec {idx s}(F : idx ~> t s)(iset : t idx) :
    denote (big.intersection F iset) = \bigcap_ (i in denote iset) denote (F i).
    induction idx; dependent destruction iset; dependent destruction F.
    - case: b.
      × by rewrite full_spec setUnit big_set1E setIT.
      × by rewrite empty_spec big_set0 full_spec.
    - by rewrite bigcap_sum -IHidx1 -IHidx2 -subset.intersection_spec.
  Qed.

End big.