regexp.abstract.utils

Require Import regexp.prelude.

Section Cxt.
  Context {St0 St1 : finType}.
  Definition State : finType := (St0 + St1)%type.

  Lemma imset_inl (st : St0)(S : {set St0}) : ((inl st : State) \in inl @: S) = (st \in S).
  Proof using Type.
    by rewrite (mem_imset _ _ inl_inj).
  Qed.

  Lemma imset_inr (st : St1)(S : {set St1}) : ((inr st : State) \in inr @: S) = (st \in S).
  Proof.
    by rewrite (mem_imset _ _ inr_inj).
  Qed.

  Lemma imset_inl_inr (st : St0)(S : {set St1}) : (inl st : State) \in inr @: S = false.
    apply/imsetP ⇒ h. case: h ⇒ x h1 h2; inversion h2.
  Qed.

  Lemma imset_inr_inl (st : St1)(S : {set St0}) : inr st \in inl @: S = false.
  Proof using Type.
    apply/imsetP ⇒ h; case: h ⇒ x h1 h2; inversion h2.
  Qed.

End Cxt.

Lemma set_unit : [set: unit] = [set tt].
  rewrite -setP ⇒ i; case i; rewrite in_set1 in_setT //=.
Qed.

Lemma snocE {A} (xs : seq A) : xs = [::] ∨ (∃ ys y, xs = ys ++ [::y]) .
  elim: xs ⇒ [|z zs IH].
  - by left.
  - case: IH ⇒ hyp; right.
    + ∃ [::]; ∃ z; by rewrite hyp.
    + case: hyp ⇒ ys [y] h.
      ∃ (z :: ys); ∃ y; by rewrite h.
Qed.

Definition inhabited {A : finType}(U : {set A}) : bool := [∃ z, z \in U].

Definition inhabitedP {A : finType}(U : {set A}) : reflect (∃ z , z \in U) (inhabited U) := existsP.

Lemma lemb : ∀ b : bool, b ∨ b = false.
  by case; intuition.
Qed.

Lemma inhabitedIP {A : finType}(U V : {set A}) : reflect (∃ z, z \in U ∧ z \in V) (inhabited (U :&: V)).
  apply/(iffP idP).
  - by case /inhabitedP ⇒ z /setIP h; ∃ z.
  - by case ⇒ z h; apply /inhabitedP; ∃ z; apply /setIP.
Qed.