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

Definition empty : ∀ {s}, [knownNat s ⇒ t s] := fun s ⇒ function.constant false.
Definition full : ∀ {s}, [knownNat s ⇒ t s] := fun s ⇒ function.constant true.

Definition inhabited {s} : [isSucc s ⇒ t s → bool] := fun u ⇒ function.fold (M := s) orb u.

Module big.

  Section Cxt.
    Context {idx s : Type}.
    Definition union : [knownNat s, isSucc idx ⇒ function.t (t s) idx → t idx → t s ] :=
      fun F iset ⇒
        function.fold (M:=idx) (@subset.union s) (function.zipWith (fun b S ⇒ if b then S else (empty (s:=s))) iset F).

    Definition intersection : [knownNat s, isSucc idx ⇒ function.t (t s) idx → t idx → t s ] :=
      fun F iset ⇒ function.fold (M:=idx) (@subset.intersection s) (function.zipWith (fun b S ⇒ if b then S else full) iset F).

  End Cxt.

End big.

Require Import regexp.concrete.universe.
Require regexp.concrete.subset.
Require regexp.synthesis.clash.axioms.

Section Syn.
  Context {s : universe.sort}.
  Definition syn (u : concrete.subset.t s) : t ⟨ s ⟩ := function.syn u.

  Lemma empty_spec : empty = syn concrete.subset.empty.
    by rewrite /empty axioms.constant_spec.
  Qed.

  Lemma intersection_spec (A B : concrete.subset.t s) : intersection (syn A) (syn B) = syn (concrete.subset.intersection A B).
    by rewrite /intersection axioms.zipWith_spec.
  Qed.

  Lemma union_spec (A B : concrete.subset.t s) : union (syn A) (syn B) = syn (concrete.subset.union A B).
    by rewrite /union axioms.zipWith_spec.
  Qed.

  Lemma inhabited_spec (A : concrete.subset.t s ) : inhabited (syn A) = concrete.subset.inhabited A.
    by rewrite /inhabited axioms.fold_spec.
  Qed.

End Syn.

Section BigSyn.
  Context {s idx : sort}.
  Context (f : concrete.function.t (concrete.subset.t s) idx).

  Lemma bigunion_spec (A : concrete.subset.t idx)
    : big.union (function.map (subset.syn) (function.syn f))(subset.syn A) = subset.syn (concrete.subset.big.union f A).
    rewrite /big.union /concrete.subset.big.union
             axioms.map_spec axioms.zipWith_spec axioms.fold_spec.
    rewrite -(concrete.function.fold_map syn concrete.subset.union union).
    set F := fun (b : bool) (S : _) ⇒ if b then _ else _.
    set G := fun (b : bool) (S : _) ⇒ if b then _ else _.
    - rewrite (concrete.function.zipWith_mapR G F syn).
      + done.
      + rewrite /G /F ⇒ a b.
        case: a; by rewrite ?empty_spec.
    - move ⇒ a b; by rewrite union_spec.
  Qed.

End BigSyn.