Subset.v

From Tealeaves Require Export
  Misc.Prop
  Classes.Functor
  Classes.Monoid.

From Tealeaves Require Import
  Classes.Categorical.ApplicativeCommutativeIdempotent
  Classes.Kleisli.Monad
  Tactics.Debug.

Import Kleisli.Monad.Notations.

#[local] Generalizable Variables A B.

(** * Subsets *)
(**********************************************************************)
#[local] Notation "( -> B )" := (fun A => A -> B) (at level 50).
#[local] Notation "'subset'" := ((-> Prop)).

(** ** Operations *)
(**********************************************************************)
Definition subset_one {A}: A -> subset A := eq.

Definition subset_empty {A}: subset A :=
  const False.

Definition subset_add {A}: subset A -> subset A -> subset A :=
  fun x y p => x p \/ y p.

(** ** Notations and Tactics *)
(**********************************************************************)
Module Notations.
  Notation "∅" := subset_empty: tealeaves_scope.
  Notation "{{ x }}" := (subset_one x): tealeaves_scope.
  Infix "∪" :=
    subset_add (at level 61, left associativity): tealeaves_scope.
  Notation "( -> B )" :=
    (fun A => A -> B) (at level 50): tealeaves_scope.
  Notation "'subset'" := ((-> Prop)): tealeaves_scope.
End Notations.

Import Notations.

Tactic Notation "simpl_subset" :=
  (autorewrite with tea_set).
Tactic Notation "simpl_subset" "in" hyp(H) :=
  (autorewrite with tea_set in H).
Tactic Notation "simpl_subset" "in" "*" :=
  (autorewrite with tea_set in *).

Ltac unfold_subset :=
  unfold subset_empty; unfold subset_add; unfold const.

Ltac solve_basic_subset :=
  unfold transparent tcs; unfold_subset; unfold compose; try setext;
  first [tauto | firstorder (subst; (solve auto + eauto)) ].

(** * The <<subset>> Monoid *)
(**********************************************************************)
Section subset_monoid.

  Context
    {A: Type}.

  Implicit Types (s t: subset A) (a: A).

  Definition subset_add_nil_l: forall s, s ∪ ∅ = s :=
    ltac:(solve_basic_subset).
  Definition subset_add_nil_r: forall s, ∅ ∪ s = s :=
    ltac:(solve_basic_subset).
  Definition subset_add_assoc: forall s t u, s ∪ t ∪ u = s ∪ (t ∪ u) :=
    ltac:(solve_basic_subset).
  Definition subset_add_comm: forall s t, s ∪ t = t ∪ s :=
    ltac:(solve_basic_subset).

  Definition subset_in_empty: forall a, ∅ a = False
    := ltac:(solve_basic_subset).
  Definition subset_in_add: forall s t a, (s ∪ t) a = (s a \/ t a)
    := ltac:(solve_basic_subset).

  Definition subset_in_one: forall a a', {{a}} a' = (a = a')
    := ltac:(solve_basic_subset).

End subset_monoid.

#[export] Hint Rewrite @subset_add_nil_l @subset_add_nil_r
     @subset_add_assoc @subset_in_empty @subset_in_add @subset_in_one: tea_set.

#[export] Instance Monoid_op_subset {A}:
  Monoid_op (subset A) := @subset_add A.

#[export] Instance Monoid_unit_subset {A}:
  Monoid_unit (subset A) := subset_empty.

#[export, program] Instance Monoid_subset {A}:
  @Monoid (subset A) (@Monoid_op_subset A) (@Monoid_unit_subset A).

Solve Obligations with
  (intros; unfold transparent tcs; solve_basic_subset).

#[export] Instance CommutativeMonoidOp_subset: forall (A: Type),
    CommutativeMonoidOp (M := subset A) Monoid_op_subset.forall A : Type, CommutativeMonoidOp Monoid_op_subset
Proof.forall A : Type, CommutativeMonoidOp Monoid_op_subset
  intros; constructor; solve_basic_subset.
Qed.

(** ** Simplification Support *)
(**********************************************************************)
Lemma monoid_subset_unit_rw {A}:
  monoid_unit (subset A) (Monoid_unit := Monoid_unit_subset) = ∅.A: Type
monoid_unit (subset%tea A) = ∅
Proof.A: Type
monoid_unit (subset%tea A) = ∅
  reflexivity.
Qed.

Lemma monoid_subset_rw:
  forall {A} (l1 l2: subset A),
    monoid_op (Monoid_op := Monoid_op_subset) l1 l2 = l1 ∪ l2.forall (A : Type) (l1 l2 : subset%tea A),
monoid_op l1 l2 = l1 ∪ l2
Proof.forall (A : Type) (l1 l2 : subset%tea A),
monoid_op l1 l2 = l1 ∪ l2
  reflexivity.
Qed.

Ltac simplify_monoid_subset :=
  ltac_trace "simplify_monoid_subset";
  match goal with
  | |- context[monoid_op (Monoid_op := Monoid_op_subset) ?S1 ?S2] =>
      rewrite monoid_subset_rw
  | |- context[monoid_unit _ (Monoid_unit := Monoid_unit_subset)] =>
      rewrite monoid_subset_unit_rw
  end.

(** ** Querying for an Element is a Monoid Homomorphism *)
(**********************************************************************)
#[export] Instance Monmor_el {A: Type} (a: A):
  @Monoid_Morphism (subset A) Prop
    (@Monoid_op_subset A) (@Monoid_unit_subset A)
    (Monoid_op_or) (Monoid_unit_false)
    (evalAt a).A: Type
a: A
Monoid_Morphism (subset%tea A) Prop (evalAt a)
Proof.A: Type
a: A
Monoid_Morphism (subset%tea A) Prop (evalAt a)
  constructor.A: Type
a: A
Monoid (A -> Prop)
A: Type
a: A
Monoid Prop
A: Type
a: A
evalAt a (monoid_unit (A -> Prop)) = monoid_unit Prop
A: Type
a: A
forall a1 a2 : A -> Prop,
evalAt a (monoid_op a1 a2) =
monoid_op (evalAt a a1) (evalAt a a2)
  -A: Type
a: A
Monoid (A -> Prop) typeclasses eauto.
  -A: Type
a: A
Monoid Prop typeclasses eauto.
  -A: Type
a: A
evalAt a (monoid_unit (A -> Prop)) = monoid_unit Prop reflexivity.
  -A: Type
a: A
forall a1 a2 : A -> Prop,
evalAt a (monoid_op a1 a2) =
monoid_op (evalAt a a1) (evalAt a a2) reflexivity.
Qed.

(** * Functor Instance *)
(**********************************************************************)

(** ** The Map Operation *)
(**********************************************************************)
#[export] Instance Map_subset: Map subset :=
  fun A B f s b => exists (a: A), s a /\ f a = b.

(** ** Rewriting Laws *)
(**********************************************************************)
Definition map_set_nil `{f: A -> B}:
  map f ∅ = ∅ := ltac:(solve_basic_subset).

Lemma map_set_one `{f: A -> B} {a: A}:
  map f {{ a }} = {{ f a }}.A, B: Type
f: A -> B
a: A
map f {{a}} = {{f a}}
Proof.A, B: Type
f: A -> B
a: A
map f {{a}} = {{f a}}
  ext b.A, B: Type
f: A -> B
a: A
b: B
map f {{a}} b = {{f a}} b propext.A, B: Type
f: A -> B
a: A
b: B
map f {{a}} b -> {{f a}} b
A, B: Type
f: A -> B
a: A
b: B
{{f a}} b -> map f {{a}} b
  -A, B: Type
f: A -> B
a: A
b: B
map f {{a}} b -> {{f a}} b intros [a' [Hin Heq]].A, B: Type
f: A -> B
a: A
b: B
a': A
Hin: {{a}} a'
Heq: f a' = b
{{f a}} b
    cbv in Hin; subst.A, B: Type
f: A -> B
a': A
{{f a'}} (f a')
    solve_basic_subset.
  -A, B: Type
f: A -> B
a: A
b: B
{{f a}} b -> map f {{a}} b cbv.A, B: Type
f: A -> B
a: A
b: B
f a = b -> exists a0 : A, a = a0 /\ f a0 = b intro; subst.A, B: Type
f: A -> B
a: A
exists a0 : A, a = a0 /\ f a0 = f a
    eauto.
Qed.

Definition map_set_add `{f: A -> B} {x y}:
  map f (x ∪ y) = map f x ∪ map f y
  := ltac:(solve_basic_subset).

#[export] Hint Rewrite
  @map_set_nil  @map_set_one  @map_set_add
: tea_set.

(** ** Functor Laws *)
(**********************************************************************)
Lemma map_id_subset: forall (A: Type), map id = id (A := subset A).forall A : Type, map id = id
Proof.forall A : Type, map id = id
  intros.A: Type
map id = id ext s a.A: Type
s: A -> Prop
a: A
map id s a = id s a
  cbv.A: Type
s: A -> Prop
a: A
(exists a0 : A, s a0 /\ a0 = a) = s a propext.A: Type
s: A -> Prop
a: A
(exists a0 : A, s a0 /\ a0 = a) -> s a
A: Type
s: A -> Prop
a: A
s a -> exists a0 : A, s a0 /\ a0 = a
  -A: Type
s: A -> Prop
a: A
(exists a0 : A, s a0 /\ a0 = a) -> s a intros [a' [Hin Heq]].A: Type
s: A -> Prop
a, a': A
Hin: s a'
Heq: a' = a
s a now subst.
  -A: Type
s: A -> Prop
a: A
s a -> exists a0 : A, s a0 /\ a0 = a intros H.A: Type
s: A -> Prop
a: A
H: s a
exists a0 : A, s a0 /\ a0 = a eauto.
Qed.

Lemma map_map_subset: forall (A B C: Type) (f: A -> B) (g: B -> C),
    map g ∘ map f = map (F := subset) (g ∘ f).forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
Proof.forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  intros.A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) ext s c.A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
(map g ∘ map f) s c = map (g ∘ f) s c
  unfold compose.A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
map g (map f s) c = map (g ○ f) s c cbv.A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
(exists a : B,
   (exists a0 : A, s a0 /\ f a0 = a) /\ g a = c) =
(exists a : A, s a /\ g (f a) = c)
  propext.A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
(exists a : B,
   (exists a0 : A, s a0 /\ f a0 = a) /\ g a = c) ->
exists a : A, s a /\ g (f a) = c
A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
(exists a : A, s a /\ g (f a) = c) ->
exists a : B,
  (exists a0 : A, s a0 /\ f a0 = a) /\ g a = c
  -A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
(exists a : B,
   (exists a0 : A, s a0 /\ f a0 = a) /\ g a = c) ->
exists a : A, s a /\ g (f a) = c intros [b [[a [Hina Heqa]] Heq]].A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
b: B
a: A
Hina: s a
Heqa: f a = b
Heq: g b = c
exists a : A, s a /\ g (f a) = c
    exists a.A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
b: B
a: A
Hina: s a
Heqa: f a = b
Heq: g b = c
s a /\ g (f a) = c rewrite Heqa.A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
b: B
a: A
Hina: s a
Heqa: f a = b
Heq: g b = c
s a /\ g b = c eauto.
  -A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
(exists a : A, s a /\ g (f a) = c) ->
exists a : B,
  (exists a0 : A, s a0 /\ f a0 = a) /\ g a = c intros [a [Hin Heq]].A, B, C: Type
f: A -> B
g: B -> C
s: A -> Prop
c: C
a: A
Hin: s a
Heq: g (f a) = c
exists a : B,
  (exists a0 : A, s a0 /\ f a0 = a) /\ g a = c eauto.
Qed.

#[export] Instance Functor_subset: Functor subset :=
  {| fun_map_id := map_id_subset;
     fun_map_map := map_map_subset;
  |}.

(** ** Mapping is a Monoid Homomorphism *)
(**********************************************************************)
#[export] Instance Monoid_Morphism_subset_map:
  forall (A B: Type) (f: A -> B),
    Monoid_Morphism (subset A) (subset B) (map f).forall (A B : Type) (f : A -> B),
Monoid_Morphism (subset%tea A) (subset%tea B) (map f)
Proof.forall (A B : Type) (f : A -> B),
Monoid_Morphism (subset%tea A) (subset%tea B) (map f)
  intros.A, B: Type
f: A -> B
Monoid_Morphism (subset%tea A) (subset%tea B) (map f)
  constructor.A, B: Type
f: A -> B
Monoid (A -> Prop)
A, B: Type
f: A -> B
Monoid (B -> Prop)
A, B: Type
f: A -> B
map f (monoid_unit (A -> Prop)) =
monoid_unit (B -> Prop)
A, B: Type
f: A -> B
forall a1 a2 : A -> Prop,
map f (monoid_op a1 a2) =
monoid_op (map f a1) (map f a2)
  -A, B: Type
f: A -> B
Monoid (A -> Prop) typeclasses eauto.
  -A, B: Type
f: A -> B
Monoid (B -> Prop) typeclasses eauto.
  -A, B: Type
f: A -> B
map f (monoid_unit (A -> Prop)) =
monoid_unit (B -> Prop) ext b.A, B: Type
f: A -> B
b: B
map f (monoid_unit (A -> Prop)) b =
monoid_unit (B -> Prop) b apply propositional_extensionality.A, B: Type
f: A -> B
b: B
map f (monoid_unit (A -> Prop)) b <->
monoid_unit (B -> Prop) b
    firstorder.
  -A, B: Type
f: A -> B
forall a1 a2 : A -> Prop,
map f (monoid_op a1 a2) =
monoid_op (map f a1) (map f a2) intros.A, B: Type
f: A -> B
a1, a2: A -> Prop
map f (monoid_op a1 a2) =
monoid_op (map f a1) (map f a2) ext b.A, B: Type
f: A -> B
a1, a2: A -> Prop
b: B
map f (monoid_op a1 a2) b =
monoid_op (map f a1) (map f a2) b apply propositional_extensionality.A, B: Type
f: A -> B
a1, a2: A -> Prop
b: B
map f (monoid_op a1 a2) b <->
monoid_op (map f a1) (map f a2) b
    firstorder.
Qed.

(** * Monad Instance (Categorical) *)
(**********************************************************************)
#[export] Instance Return_subset: Return subset := fun A a b => a = b.

#[local] Notation "{{ x }}" := (@ret subset _ _ x).

#[local] Instance Join_subset: Monad.Join subset := fun A P a => exists (Q: subset A), P Q /\ Q a.

(** ** Monad Laws *)
(**********************************************************************)
#[export] Instance Natural_Return_subset: Natural (@ret subset _).Natural (@ret subset%tea Return_subset)
Proof.Natural (@ret subset%tea Return_subset)
  constructor.Functor (fun A : Type => A)
Functor subset%tea
forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f
  -Functor (fun A : Type => A) typeclasses eauto.
  -Functor subset%tea typeclasses eauto.
  -forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f intros.A, B: Type
f: A -> B
map f ∘ ret = ret ∘ map f ext a.A, B: Type
f: A -> B
a: A
(map f ∘ ret) a = (ret ∘ map f) a ext b.A, B: Type
f: A -> B
a: A
b: B
(map f ∘ ret) a b = (ret ∘ map f) a b
    unfold_ops @Map_I @Map_subset @Return_subset.A, B: Type
f: A -> B
a: A
b: B
((fun (s : A -> Prop) (b : B) =>
  exists a : A, s a /\ f a = b)
 ∘ (fun a b : A => a = b)) a b =
((fun a b : B => a = b) ∘ f) a b
    unfold compose.A, B: Type
f: A -> B
a: A
b: B
(exists a0 : A, a = a0 /\ f a0 = b) = (f a = b)
    propext.A, B: Type
f: A -> B
a: A
b: B
(exists a0 : A, a = a0 /\ f a0 = b) -> f a = b
A, B: Type
f: A -> B
a: A
b: B
f a = b -> exists a0 : A, a = a0 /\ f a0 = b
    firstorder (now subst).A, B: Type
f: A -> B
a: A
b: B
f a = b -> exists a0 : A, a = a0 /\ f a0 = b
    firstorder (now subst).
Qed.

Lemma natural_join_subset:
  forall (A B : Type) (f : A -> B), map f ∘ Monad.join = Monad.join ∘ map f.forall (A B : Type) (f : A -> B),
map f ∘ Monad.join = Monad.join ∘ map f
Proof.forall (A B : Type) (f : A -> B),
map f ∘ Monad.join = Monad.join ∘ map f
  intros.A, B: Type
f: A -> B
map f ∘ Monad.join = Monad.join ∘ map f
  unfold compose.A, B: Type
f: A -> B
map f ○ Monad.join = Monad.join ○ map f
  unfold_ops @Map_compose @Map_subset @Join_subset.A, B: Type
f: A -> B
(fun (a : (A -> Prop) -> Prop) (b : B) =>
 exists a0 : A,
   (exists Q : A -> Prop, a Q /\ Q a0) /\ f a0 = b) =
(fun (a : (A -> Prop) -> Prop) (a0 : B) =>
 exists Q : B -> Prop,
   (exists a1 : A -> Prop,
      a a1 /\
      (fun b : B => exists a2 : A, a1 a2 /\ f a2 = b) =
      Q) /\ Q a0)
  ext P b.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
(exists a : A,
   (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b) =
(exists Q : B -> Prop,
   (exists a : A -> Prop,
      P a /\
      (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
      Q) /\ Q b) propext.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
(exists a : A,
   (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b) ->
exists Q : B -> Prop,
  (exists a : A -> Prop,
     P a /\
     (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
     Q) /\ Q b
A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
(exists Q : B -> Prop,
   (exists a : A -> Prop,
      P a /\
      (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
      Q) /\ Q b) ->
exists a : A,
  (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b
  +A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
(exists a : A,
   (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b) ->
exists Q : B -> Prop,
  (exists a : A -> Prop,
     P a /\
     (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
     Q) /\ Q b intros [a [[Q [PQ Qa]] Heq]].A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
Heq: f a = b
exists Q : B -> Prop,
  (exists a : A -> Prop,
     P a /\
     (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
     Q) /\ Q b
    subst.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
exists Q : B -> Prop,
  (exists a : A -> Prop,
     P a /\
     (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
     Q) /\ Q (f a)
    exists (map f Q).A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
(exists a : A -> Prop,
   P a /\
   (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
   map f Q) /\ map f Q (f a)
    unfold_ops @Map_subset.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
(exists a : A -> Prop,
   P a /\
   (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
   (fun b : B => exists a0 : A, Q a0 /\ f a0 = b)) /\
(exists a0 : A, Q a0 /\ f a0 = f a)
    split.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
exists a : A -> Prop,
  P a /\
  (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
  (fun b : B => exists a0 : A, Q a0 /\ f a0 = b)
A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
exists a0 : A, Q a0 /\ f a0 = f a
    *A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
exists a : A -> Prop,
  P a /\
  (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
  (fun b : B => exists a0 : A, Q a0 /\ f a0 = b) exists Q.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
P Q /\
(fun b : B => exists a : A, Q a /\ f a = b) =
(fun b : B => exists a : A, Q a /\ f a = b) split.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
P Q
A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
(fun b : B => exists a : A, Q a /\ f a = b) =
(fun b : B => exists a : A, Q a /\ f a = b)
      {A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
P Q assumption. }A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
(fun b : B => exists a : A, Q a /\ f a = b) =
(fun b : B => exists a : A, Q a /\ f a = b)
      {A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
(fun b : B => exists a : A, Q a /\ f a = b) =
(fun b : B => exists a : A, Q a /\ f a = b) setext; firstorder. }
    *A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
a: A
Q: A -> Prop
PQ: P Q
Qa: Q a
exists a0 : A, Q a0 /\ f a0 = f a firstorder.
  +A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
(exists Q : B -> Prop,
   (exists a : A -> Prop,
      P a /\
      (fun b : B => exists a0 : A, a a0 /\ f a0 = b) =
      Q) /\ Q b) ->
exists a : A,
  (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b intros [Qb [[Qa [PQa rest]] Qbb]].A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
Qb: B -> Prop
Qa: A -> Prop
PQa: P Qa
rest: (fun b : B => exists a : A, Qa a /\ f a = b) =
Qb
Qbb: Qb b
exists a : A,
  (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b
    subst.A, B: Type
f: A -> B
P: (A -> Prop) -> Prop
b: B
Qa: A -> Prop
PQa: P Qa
Qbb: exists a : A, Qa a /\ f a = b
exists a : A,
  (exists Q : A -> Prop, P Q /\ Q a) /\ f a = b
    firstorder.
Qed.

#[export] Instance Natural_Join_subset: Natural (@Monad.join subset _).Natural (@Monad.join subset%tea Join_subset)
Proof.Natural (@Monad.join subset%tea Join_subset)
  constructor.Functor (subset%tea ∘ subset%tea)
Functor subset%tea
forall (A B : Type) (f : A -> B),
map f ∘ Monad.join = Monad.join ∘ map f
  -Functor (subset%tea ∘ subset%tea) typeclasses eauto.
  -Functor subset%tea typeclasses eauto.
  -forall (A B : Type) (f : A -> B),
map f ∘ Monad.join = Monad.join ∘ map f apply natural_join_subset.
Qed.

Lemma join_ret_subset:
  forall A: Type, Monad.join (T := subset) ∘ (ret (T := subset)) = (@id (subset A)).forall A : Type, Monad.join ∘ ret = id
Proof.forall A : Type, Monad.join ∘ ret = id
  intros.A: Type
Monad.join ∘ ret = id ext P.A: Type
P: A -> Prop
(Monad.join ∘ ret) P = id P unfold id.A: Type
P: A -> Prop
(Monad.join ∘ ret) P = P
  unfold compose.A: Type
P: A -> Prop
Monad.join {{P}} = P
  unfold_ops @Join_subset.A: Type
P: A -> Prop
(fun a : A => exists Q : A -> Prop, {{P}} Q /\ Q a) =
P
  ext a.A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop, {{P}} Q /\ Q a) = P a
  propext.A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop, {{P}} Q /\ Q a) -> P a
A: Type
P: A -> Prop
a: A
P a -> exists Q : A -> Prop, {{P}} Q /\ Q a
  -A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop, {{P}} Q /\ Q a) -> P a simpl_subset.A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop, {{P}} Q /\ Q a) -> P a
    intros [Q [Qin Qa]].A: Type
P: A -> Prop
a: A
Q: A -> Prop
Qin: {{P}} Q
Qa: Q a
P a
    simpl_subset in Qin.A: Type
P: A -> Prop
a: A
Q: A -> Prop
Qin: P = Q
Qa: Q a
P a
    now subst.
  -A: Type
P: A -> Prop
a: A
P a -> exists Q : A -> Prop, {{P}} Q /\ Q a intros.A: Type
P: A -> Prop
a: A
H: P a
exists Q : A -> Prop, {{P}} Q /\ Q a exists P.A: Type
P: A -> Prop
a: A
H: P a
{{P}} P /\ P a now simpl_subset.
Qed.

Corollary join_one_subset: forall (A: Type) (P: A -> Prop),
    Monad.join {{P}} = P.forall (A : Type) (P : A -> Prop),
Monad.join {{P}} = P
Proof.forall (A : Type) (P : A -> Prop),
Monad.join {{P}} = P
  intros.A: Type
P: A -> Prop
Monad.join {{P}} = P
  change ((Monad.join ∘ ret (T := subset)) P = P).A: Type
P: A -> Prop
(Monad.join ∘ ret) P = P
  rewrite join_ret_subset.A: Type
P: A -> Prop
id P = P
  reflexivity.
Qed.

Lemma join_map_ret_subset:
  forall A : Type, Monad.join (T := subset) (A := A) ∘
                map (ret (A := A) (T := subset)) = id.forall A : Type, Monad.join ∘ map ret = id
Proof.forall A : Type, Monad.join ∘ map ret = id
  intros.A: Type
Monad.join ∘ map ret = id
  unfold id, compose.A: Type
Monad.join ○ map ret = (fun x : A -> Prop => x)
  ext P a.A: Type
P: A -> Prop
a: A
Monad.join (map ret P) a = P a
  unfold_ops @Join_subset @Map_compose @Map_subset.A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop,
   (exists a : A, P a /\ {{a}} = Q) /\ Q a) = P a
  propext.A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop,
   (exists a : A, P a /\ {{a}} = Q) /\ Q a) -> P a
A: Type
P: A -> Prop
a: A
P a ->
exists Q : A -> Prop,
  (exists a : A, P a /\ {{a}} = Q) /\ Q a
  -A: Type
P: A -> Prop
a: A
(exists Q : A -> Prop,
   (exists a : A, P a /\ {{a}} = Q) /\ Q a) -> P a intros [P' [[a' [Pa' rest]] Ha']].A: Type
P: A -> Prop
a: A
P': A -> Prop
a': A
Pa': P a'
rest: {{a'}} = P'
Ha': P' a
P a
    subst.A: Type
P: A -> Prop
a, a': A
Pa': P a'
Ha': {{a'}} a
P a
    simpl_subset in Ha'.A: Type
P: A -> Prop
a, a': A
Pa': P a'
Ha': a' = a
P a now subst.
  -A: Type
P: A -> Prop
a: A
P a ->
exists Q : A -> Prop,
  (exists a : A, P a /\ {{a}} = Q) /\ Q a intros.A: Type
P: A -> Prop
a: A
H: P a
exists Q : A -> Prop,
  (exists a : A, P a /\ {{a}} = Q) /\ Q a exists {{a}}.A: Type
P: A -> Prop
a: A
H: P a
(exists a0 : A, P a0 /\ {{a0}} = {{a}}) /\ {{a}} a
    simpl_subset.A: Type
P: A -> Prop
a: A
H: P a
(exists a0 : A, P a0 /\ {{a0}} = {{a}}) /\ a = a
    split; eauto.
Qed.

Lemma join_join_subset:
  forall A : Type,
    Monad.join (T := subset) (A := A) ∘
      Monad.join (T := subset) (A := subset A)
    = Monad.join (T := subset) (A := A) ∘ map (Monad.join (T := subset)).forall A : Type,
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join
Proof.forall A : Type,
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join
  intros.A: Type
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join
  unfold id, compose.A: Type
Monad.join ○ Monad.join = Monad.join ○ map Monad.join
  ext P a.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Monad.join (Monad.join P) a =
Monad.join (map Monad.join P) a
  propext.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Monad.join (Monad.join P) a ->
Monad.join (map Monad.join P) a
A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Monad.join (map Monad.join P) a ->
Monad.join (Monad.join P) a
  -A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Monad.join (Monad.join P) a ->
Monad.join (map Monad.join P) a intros [Q [[R [PR RQ]] Qa]].A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
Monad.join (map Monad.join P) a
    unfold_ops @Map_subset.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
Monad.join
  (fun b : A -> Prop =>
   exists a : (A -> Prop) -> Prop,
     P a /\ Monad.join a = b) a
    unfold Monad.join at 1.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
Join_subset A
  (fun b : A -> Prop =>
   exists a : (A -> Prop) -> Prop,
     P a /\ Monad.join a = b) a
    unfold Join_subset at 1.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
exists Q : A -> Prop,
  (exists a : (A -> Prop) -> Prop,
     P a /\ Monad.join a = Q) /\ Q a
    exists (Monad.join R); split; auto.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
exists a : (A -> Prop) -> Prop,
  P a /\ Monad.join a = Monad.join R
A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
Monad.join R a
    exists R; auto.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: A -> Prop
R: (A -> Prop) -> Prop
PR: P R
RQ: R Q
Qa: Q a
Monad.join R a exists Q; auto.
  -A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Monad.join (map Monad.join P) a ->
Monad.join (Monad.join P) a intros [R [[Q [PQ Rspec]] Ra]].A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
R: A -> Prop
Q: (A -> Prop) -> Prop
PQ: P Q
Rspec: Monad.join Q = R
Ra: R a
Monad.join (Monad.join P) a
    subst.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: (A -> Prop) -> Prop
PQ: P Q
Ra: Monad.join Q a
Monad.join (Monad.join P) a
    destruct Ra as [X [QX Xa]].A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: (A -> Prop) -> Prop
PQ: P Q
X: A -> Prop
QX: Q X
Xa: X a
Monad.join (Monad.join P) a
    exists X; split; auto.A: Type
P: ((A -> Prop) -> Prop) -> Prop
a: A
Q: (A -> Prop) -> Prop
PQ: P Q
X: A -> Prop
QX: Q X
Xa: X a
Monad.join P X
    exists Q; auto.
Qed.

#[local] Instance Categorical_Monad_subset: Categorical.Monad.Monad subset.Categorical.Monad.Monad subset%tea
Proof.Categorical.Monad.Monad subset%tea
  constructor.Functor subset%tea
Natural (@ret subset%tea Return_subset)
Natural (@Monad.join subset%tea Join_subset)
forall A : Type, Monad.join ∘ ret = id
forall A : Type, Monad.join ∘ map ret = id
forall A : Type,
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join
  -Functor subset%tea typeclasses eauto.
  -Natural (@ret subset%tea Return_subset) typeclasses eauto.
  -Natural (@Monad.join subset%tea Join_subset) typeclasses eauto.
  -forall A : Type, Monad.join ∘ ret = id apply join_ret_subset.
  -forall A : Type, Monad.join ∘ map ret = id apply join_map_ret_subset.
  -forall A : Type,
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join apply join_join_subset.
Qed.

(** * Monad Instance (Kleisli) *)
(**********************************************************************)
#[export] Instance Bind_subset: Bind subset subset := fun A B f s_a =>
(fun b => exists (a: A), s_a a /\ f a b).

#[export] Instance Compat_Map_Bind_subset:
  `{Compat_Map_Bind (Map_U := Map_subset) subset subset} :=
  ltac:(reflexivity).

(** ** Rewriting Laws *)
(**********************************************************************)
Definition set_in_ret: forall A (a b: A),
    (ret a) b = (a = b) := ltac:(reflexivity).

#[export] Hint Rewrite @set_in_ret: tea_set.

Lemma bind_set_nil `{f: A -> subset B}:
  bind f ∅ = ∅.A, B: Type
f: A -> subset%tea B
bind f ∅ = ∅
Proof.A, B: Type
f: A -> subset%tea B
bind f ∅ = ∅
  solve_basic_subset.
Qed.

Lemma bind_set_one `{f: A -> subset B} {a: A}:
  bind f {{ a }} = f a.A, B: Type
f: A -> subset%tea B
a: A
bind f {{a}} = f a
Proof.A, B: Type
f: A -> subset%tea B
a: A
bind f {{a}} = f a
  solve_basic_subset.
Qed.

Lemma bind_set_add `{f: A -> subset B} {x y}:
  bind f (x ∪ y) = bind f x ∪ bind f y.A, B: Type
f: A -> subset%tea B
x, y: A -> Prop
bind f (x ∪ y) = bind f x ∪ bind f y
Proof.A, B: Type
f: A -> subset%tea B
x, y: A -> Prop
bind f (x ∪ y) = bind f x ∪ bind f y
  solve_basic_subset.
Qed.

#[export] Hint Rewrite
  @bind_set_nil  @bind_set_one  @bind_set_add
: tea_set.

(** ** Monad Laws *)
(**********************************************************************)
Lemma set_bind0: forall (A B: Type) (f: A -> subset B),
    bind f ∘ ret = f.forall (A B : Type) (f : A -> subset%tea B),
bind f ∘ ret = f
Proof.forall (A B : Type) (f : A -> subset%tea B),
bind f ∘ ret = f
  intros.A, B: Type
f: A -> subset%tea B
bind f ∘ ret = f ext a.A, B: Type
f: A -> subset%tea B
a: A
(bind f ∘ ret) a = f a unfold compose.A, B: Type
f: A -> subset%tea B
a: A
bind f {{a}} = f a
  now autorewrite with tea_set.
Qed.

Lemma set_bind1: forall A: Type, bind ret = @id (subset A).forall A : Type, bind ret = id
  intros.A: Type
bind ret = id cbv.A: Type
(fun (s_a : A -> Prop) (b : A) =>
 exists a : A, s_a a /\ a = b) =
(fun x : A -> Prop => x) ext s a.A: Type
s: A -> Prop
a: A
(exists a0 : A, s a0 /\ a0 = a) = s a propext.A: Type
s: A -> Prop
a: A
(exists a0 : A, s a0 /\ a0 = a) -> s a
A: Type
s: A -> Prop
a: A
s a -> exists a0 : A, s a0 /\ a0 = a
  -A: Type
s: A -> Prop
a: A
(exists a0 : A, s a0 /\ a0 = a) -> s a intros [a' [h1 h2]].A: Type
s: A -> Prop
a, a': A
h1: s a'
h2: a' = a
s a now subst.
  -A: Type
s: A -> Prop
a: A
s a -> exists a0 : A, s a0 /\ a0 = a intro.A: Type
s: A -> Prop
a: A
H: s a
exists a0 : A, s a0 /\ a0 = a eexists a.A: Type
s: A -> Prop
a: A
H: s a
s a /\ a = a intuition.
Qed.

Lemma set_bind2:
  forall (A B C: Type) (g: B -> subset C) (f: A -> subset B),
    bind g ∘ bind f = bind (g ⋆ f).forall (A B C : Type) (g : B -> subset%tea C)
  (f : A -> subset%tea B),
bind g ∘ bind f = bind (g ⋆ f)
Proof.forall (A B C : Type) (g : B -> subset%tea C)
  (f : A -> subset%tea B),
bind g ∘ bind f = bind (g ⋆ f)
  intros.A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
bind g ∘ bind f = bind (g ⋆ f) ext a.A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
(bind g ∘ bind f) a = bind (g ⋆ f) a unfold compose.A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
bind g (bind f a) = bind (g ⋆ f) a
  cbv.A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
(fun b : C =>
 exists a0 : B,
   (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 b) =
(fun b : C =>
 exists a0 : A,
   a a0 /\ (exists a : B, f a0 a /\ g a b)) ext c.A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
(exists a0 : B,
   (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 c) =
(exists a0 : A,
   a a0 /\ (exists a : B, f a0 a /\ g a c)) propext.A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
(exists a0 : B,
   (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 c) ->
exists a0 : A, a a0 /\ (exists a : B, f a0 a /\ g a c)
A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
(exists a0 : A,
   a a0 /\ (exists a : B, f a0 a /\ g a c)) ->
exists a0 : B,
  (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 c
  -A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
(exists a0 : B,
   (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 c) ->
exists a0 : A, a a0 /\ (exists a : B, f a0 a /\ g a c) intros [b [[a' [ha1 ha2]] hb2]].A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
b: B
a': A
ha1: a a'
ha2: f a' b
hb2: g b c
exists a0 : A, a a0 /\ (exists a : B, f a0 a /\ g a c)
    exists a'; split; [assumption | exists b; split; assumption].
  -A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
(exists a0 : A,
   a a0 /\ (exists a : B, f a0 a /\ g a c)) ->
exists a0 : B,
  (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 c intros [a' [ha1 [b [hb1 hb2]]]].A, B, C: Type
g: B -> subset%tea C
f: A -> subset%tea B
a: A -> Prop
c: C
a': A
ha1: a a'
b: B
hb1: f a' b
hb2: g b c
exists a0 : B,
  (exists a1 : A, a a1 /\ f a1 a0) /\ g a0 c
    exists b; split; [exists a'; split; assumption | assumption].
Qed.

#[export] Instance RightPreModule_subset: RightPreModule subset subset :=
  {| kmod_bind1 := set_bind1;
     kmod_bind2 := set_bind2;
  |}.

#[export] Instance Monad_subset: Monad subset :=
  {| kmon_bind0 := set_bind0;
  |}.

#[export] Instance RightModule_subset: RightModule subset subset :=
  {| kmod_monad := _;
  |}.

(** ** <<bind>> is a Monoid Homomorphism *)
(**********************************************************************)
#[export] Instance Monmor_bind {A B f}:
  Monoid_Morphism (subset A) (subset B) (bind f) :=
  {| monmor_unit := @bind_set_nil A B f;
     monmor_op := @bind_set_add A B f;
  |}.

(** ** <<{{ - }}>> is Injective *)
(**********************************************************************)
Theorem set_ret_injective: forall (A: Type) (a b: A),
    {{ a }} = {{ b }} -> a = b.forall (A : Type) (a b : A), {{a}} = {{b}} -> a = b
Proof.forall (A : Type) (a b : A), {{a}} = {{b}} -> a = b
  intros.A: Type
a, b: A
H: {{a}} = {{b}}
a = b assert (lemma: forall x, {{ a }} x = {{ b }} x).A: Type
a, b: A
H: {{a}} = {{b}}
forall x : A, {{a}} x = {{b}} x
A: Type
a, b: A
H: {{a}} = {{b}}
lemma: forall x : A, {{a}} x = {{b}} x
a = b
  intros.A: Type
a, b: A
H: {{a}} = {{b}}
x: A
{{a}} x = {{b}} x
A: Type
a, b: A
H: {{a}} = {{b}}
lemma: forall x : A, {{a}} x = {{b}} x
a = b now rewrite H.A: Type
a, b: A
H: {{a}} = {{b}}
lemma: forall x : A, {{a}} x = {{b}} x
a = b specialize (lemma a).A: Type
a, b: A
H: {{a}} = {{b}}
lemma: {{a}} a = {{b}} a
a = b
  cbv in lemma.A: Type
a, b: A
H: {{a}} = {{b}}
lemma: (a = a) = (b = a)
a = b symmetry.A: Type
a, b: A
H: {{a}} = {{b}}
lemma: (a = a) = (b = a)
b = a now rewrite <- lemma.
Qed.

(** * Applicative Instance *)
(**********************************************************************)
Section subset_applicative_instance.

  Import Applicative.Notations.

  #[export] Instance Pure_subset: Pure subset := @eq.

  #[export] Instance Mult_subset: Mult subset :=
    fun A B '(sa, sb) '(a, b) => sa a /\ sb b.

  #[export] Instance Applicative_subset: Applicative subset.Applicative subset%tea
  Proof.Applicative subset%tea
    constructor.Functor subset%tea
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : A -> Prop) (y : B -> Prop),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
forall (A B C : Type) (x : A -> Prop) (y : B -> Prop)
  (z : C -> Prop),
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
forall (A : Type) (x : A -> Prop),
map left_unitor (pure tt ⊗ x) = x
forall (A : Type) (x : A -> Prop),
map right_unitor (x ⊗ pure tt) = x
forall (A B : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
    -Functor subset%tea apply Functor_subset.
    -forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x) intros.A, B: Type
f: A -> B
x: A
map f (pure x) = pure (f x) change (pure ?x) with (ret x).A, B: Type
f: A -> B
x: A
map f {{x}} = {{f x}}
      now simpl_subset.
    -forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : A -> Prop) (y : B -> Prop),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y) intros.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y) unfold_ops @Mult_subset.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
(fun '(a, b) => map f x a /\ map g y b) =
map (map_tensor f g) (fun '(a, b) => x a /\ y b)
      ext [c d].A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
(map f x c /\ map g y d) =
map (map_tensor f g) (fun '(a, b) => x a /\ y b)
  (c, d) cbv.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
((exists a : A, x a /\ f a = c) /\
 (exists a : B, y a /\ g a = d)) =
(exists a : A * B,
   (let '(a0, b) := a in x a0 /\ y b) /\
   (let (x, y) := a in (f x, g y)) = (c, d)) propext.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
(exists a : A, x a /\ f a = c) /\
(exists a : B, y a /\ g a = d) ->
exists a : A * B,
  (let '(a0, b) := a in x a0 /\ y b) /\
  (let (x, y) := a in (f x, g y)) = (c, d)
A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
(exists a : A * B,
   (let '(a0, b) := a in x a0 /\ y b) /\
   (let (x, y) := a in (f x, g y)) = (c, d)) ->
(exists a : A, x a /\ f a = c) /\
(exists a : B, y a /\ g a = d)
      +A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
(exists a : A, x a /\ f a = c) /\
(exists a : B, y a /\ g a = d) ->
exists a : A * B,
  (let '(a0, b) := a in x a0 /\ y b) /\
  (let (x, y) := a in (f x, g y)) = (c, d) intros [[a [Ha1 Ha2]] [b [Hb1 Hb2]]].A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
a: A
Ha1: x a
Ha2: f a = c
b: B
Hb1: y b
Hb2: g b = d
exists a : A * B,
  (let '(a0, b) := a in x a0 /\ y b) /\
  (let (x, y) := a in (f x, g y)) = (c, d)
        exists (a, b).A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
a: A
Ha1: x a
Ha2: f a = c
b: B
Hb1: y b
Hb2: g b = d
(x a /\ y b) /\ (f a, g b) = (c, d) subst.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
a: A
Ha1: x a
b: B
Hb1: y b
(x a /\ y b) /\ (f a, g b) = (f a, g b) intuition.
      +A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
(exists a : A * B,
   (let '(a0, b) := a in x a0 /\ y b) /\
   (let (x, y) := a in (f x, g y)) = (c, d)) ->
(exists a : A, x a /\ f a = c) /\
(exists a : B, y a /\ g a = d) intros [[a b] [Hab1 Hab2]].A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
a: A
b: B
Hab1: x a /\ y b
Hab2: (f a, g b) = (c, d)
(exists a : A, x a /\ f a = c) /\
(exists a : B, y a /\ g a = d)
        inversion Hab2.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
c: C
d: D
a: A
b: B
Hab1: x a /\ y b
Hab2: (f a, g b) = (c, d)
H0: f a = c
H1: g b = d
(exists a0 : A, x a0 /\ f a0 = f a) /\
(exists a : B, y a /\ g a = g b) subst.A, B, C, D: Type
f: A -> C
g: B -> D
x: A -> Prop
y: B -> Prop
a: A
b: B
Hab1: x a /\ y b
Hab2: (f a, g b) = (f a, g b)
(exists a0 : A, x a0 /\ f a0 = f a) /\
(exists a : B, y a /\ g a = g b) intuition eauto.
    -forall (A B C : Type) (x : A -> Prop) (y : B -> Prop)
  (z : C -> Prop),
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z) intros.A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z) ext [a [b c]].A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
map associator (x ⊗ y ⊗ z) (a, (b, c)) =
(x ⊗ (y ⊗ z)) (a, (b, c)) cbv.A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
(exists a0 : A * B * C,
   (let
    '(a, b) := a0 in
     (let '(a1, b0) := a in x a1 /\ y b0) /\ z b) /\
   (let (p0, z) := a0 in
    let (x, y) := p0 in (x, (y, z))) = (a, (b, c))) =
(x a /\ y b /\ z c)
      propext.A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
(exists a0 : A * B * C,
   (let
    '(a, b) := a0 in
     (let '(a1, b0) := a in x a1 /\ y b0) /\ z b) /\
   (let (p0, z) := a0 in
    let (x, y) := p0 in (x, (y, z))) = (a, (b, c))) ->
x a /\ y b /\ z c
A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
x a /\ y b /\ z c ->
exists a0 : A * B * C,
  (let
   '(a, b) := a0 in
    (let '(a1, b0) := a in x a1 /\ y b0) /\ z b) /\
  (let (p0, z) := a0 in
   let (x, y) := p0 in (x, (y, z))) = (a, (b, c))
      +A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
(exists a0 : A * B * C,
   (let
    '(a, b) := a0 in
     (let '(a1, b0) := a in x a1 /\ y b0) /\ z b) /\
   (let (p0, z) := a0 in
    let (x, y) := p0 in (x, (y, z))) = (a, (b, c))) ->
x a /\ y b /\ z c intros [[[a' b'] c'] [Ht1 Ht2]].A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
a': A
b': B
c': C
Ht1: (x a' /\ y b') /\ z c'
Ht2: (a', (b', c')) = (a, (b, c))
x a /\ y b /\ z c
        inversion Ht2; subst.A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
Ht2: (a, (b, c)) = (a, (b, c))
Ht1: (x a /\ y b) /\ z c
x a /\ y b /\ z c tauto.
      +A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
x a /\ y b /\ z c ->
exists a0 : A * B * C,
  (let
   '(a, b) := a0 in
    (let '(a1, b0) := a in x a1 /\ y b0) /\ z b) /\
  (let (p0, z) := a0 in
   let (x, y) := p0 in (x, (y, z))) = (a, (b, c)) intros.A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
H: x a /\ y b /\ z c
exists a0 : A * B * C,
  (let
   '(a, b) := a0 in
    (let '(a1, b0) := a in x a1 /\ y b0) /\ z b) /\
  (let (p0, z) := a0 in
   let (x, y) := p0 in (x, (y, z))) = (a, (b, c)) exists (a, b, c).A, B, C: Type
x: A -> Prop
y: B -> Prop
z: C -> Prop
a: A
b: B
c: C
H: x a /\ y b /\ z c
((x a /\ y b) /\ z c) /\ (a, (b, c)) = (a, (b, c)) tauto.
    -forall (A : Type) (x : A -> Prop),
map left_unitor (pure tt ⊗ x) = x intros.A: Type
x: A -> Prop
map left_unitor (pure tt ⊗ x) = x ext a.A: Type
x: A -> Prop
a: A
map left_unitor (pure tt ⊗ x) a = x a cbv.A: Type
x: A -> Prop
a: A
(exists a0 : unit * A,
   (let '(a, b) := a0 in tt = a /\ x b) /\
   (let (_, y) := a0 in y) = a) = x a
      propext.A: Type
x: A -> Prop
a: A
(exists a0 : unit * A,
   (let '(a, b) := a0 in tt = a /\ x b) /\
   (let (_, y) := a0 in y) = a) -> x a
A: Type
x: A -> Prop
a: A
x a ->
exists a0 : unit * A,
  (let '(a, b) := a0 in tt = a /\ x b) /\
  (let (_, y) := a0 in y) = a
      +A: Type
x: A -> Prop
a: A
(exists a0 : unit * A,
   (let '(a, b) := a0 in tt = a /\ x b) /\
   (let (_, y) := a0 in y) = a) -> x a intros [[tt' a'] [H1 H2]].A: Type
x: A -> Prop
a: A
tt': unit
a': A
H1: tt = tt' /\ x a'
H2: a' = a
x a now subst.
      +A: Type
x: A -> Prop
a: A
x a ->
exists a0 : unit * A,
  (let '(a, b) := a0 in tt = a /\ x b) /\
  (let (_, y) := a0 in y) = a intros Xa.A: Type
x: A -> Prop
a: A
Xa: x a
exists a0 : unit * A,
  (let '(a, b) := a0 in tt = a /\ x b) /\
  (let (_, y) := a0 in y) = a exists (tt, a).A: Type
x: A -> Prop
a: A
Xa: x a
(tt = tt /\ x a) /\ a = a tauto.
    -forall (A : Type) (x : A -> Prop),
map right_unitor (x ⊗ pure tt) = x intros.A: Type
x: A -> Prop
map right_unitor (x ⊗ pure tt) = x ext a.A: Type
x: A -> Prop
a: A
map right_unitor (x ⊗ pure tt) a = x a cbv.A: Type
x: A -> Prop
a: A
(exists a0 : A * unit,
   (let '(a, b) := a0 in x a /\ tt = b) /\
   (let (x, _) := a0 in x) = a) = x a
      propext.A: Type
x: A -> Prop
a: A
(exists a0 : A * unit,
   (let '(a, b) := a0 in x a /\ tt = b) /\
   (let (x, _) := a0 in x) = a) -> x a
A: Type
x: A -> Prop
a: A
x a ->
exists a0 : A * unit,
  (let '(a, b) := a0 in x a /\ tt = b) /\
  (let (x, _) := a0 in x) = a
      +A: Type
x: A -> Prop
a: A
(exists a0 : A * unit,
   (let '(a, b) := a0 in x a /\ tt = b) /\
   (let (x, _) := a0 in x) = a) -> x a intros [[a' tt'] [H1 H2]].A: Type
x: A -> Prop
a, a': A
tt': unit
H1: x a' /\ tt = tt'
H2: a' = a
x a now subst.
      +A: Type
x: A -> Prop
a: A
x a ->
exists a0 : A * unit,
  (let '(a, b) := a0 in x a /\ tt = b) /\
  (let (x, _) := a0 in x) = a intros Xa.A: Type
x: A -> Prop
a: A
Xa: x a
exists a0 : A * unit,
  (let '(a, b) := a0 in x a /\ tt = b) /\
  (let (x, _) := a0 in x) = a exists (a, tt).A: Type
x: A -> Prop
a: A
Xa: x a
(x a /\ tt = tt) /\ a = a tauto.
    -forall (A B : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b) intros.A, B: Type
a: A
b: B
pure a ⊗ pure b = pure (a, b) ext [a' b'].A, B: Type
a: A
b: B
a': A
b': B
(pure a ⊗ pure b) (a', b') = pure (a, b) (a', b') cbv.A, B: Type
a: A
b: B
a': A
b': B
(a = a' /\ b = b') = ((a, b) = (a', b')) propext.A, B: Type
a: A
b: B
a': A
b': B
a = a' /\ b = b' -> (a, b) = (a', b')
A, B: Type
a: A
b: B
a': A
b': B
(a, b) = (a', b') -> a = a' /\ b = b'
      +A, B: Type
a: A
b: B
a': A
b': B
a = a' /\ b = b' -> (a, b) = (a', b') intuition.A, B: Type
a: A
b: B
a': A
b': B
H0: a = a'
H1: b = b'
(a, b) = (a', b') now subst.
      +A, B: Type
a: A
b: B
a': A
b': B
(a, b) = (a', b') -> a = a' /\ b = b' intros X; inversion X; now subst.
  Qed.

  Lemma subset_ap_spec:
    forall (A B: Type) (sf: subset (A -> B)) (sa: subset A) (b: B),
      (sf <⋆> sa) b = exists (f: A -> B) (a: A), sa a /\ sf f /\ f a = b.forall (A B : Type) (sf : subset%tea (A -> B))
  (sa : subset%tea A) (b : B),
(sf <⋆> sa) b =
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b)
  Proof.forall (A B : Type) (sf : subset%tea (A -> B))
  (sa : subset%tea A) (b : B),
(sf <⋆> sa) b =
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b)
    intros.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(sf <⋆> sa) b =
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b)
    unfold ap.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
map (fun '(f, a) => f a) (sf ⊗ sa) b =
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b)
    unfold_ops @Map_subset.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(exists a : (A -> B) * A,
   (sf ⊗ sa) a /\ (let '(f, a0) := a in f a0) = b) =
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b)
    unfold_ops @Mult_subset.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(exists a : (A -> B) * A,
   (let '(a0, b) := a in sf a0 /\ sa b) /\
   (let '(f, a0) := a in f a0) = b) =
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b)
    propext.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(exists a : (A -> B) * A,
   (let '(a0, b) := a in sf a0 /\ sa b) /\
   (let '(f, a0) := a in f a0) = b) ->
exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b
A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b) ->
exists a : (A -> B) * A,
  (let '(a0, b) := a in sf a0 /\ sa b) /\
  (let '(f, a0) := a in f a0) = b
    -A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(exists a : (A -> B) * A,
   (let '(a0, b) := a in sf a0 /\ sa b) /\
   (let '(f, a0) := a in f a0) = b) ->
exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b intros [[f a] [[hyp1 hyp2] hyp3]].A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
f: A -> B
a: A
hyp1: sf f
hyp2: sa a
hyp3: f a = b
exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b
      exists f a.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
f: A -> B
a: A
hyp1: sf f
hyp2: sa a
hyp3: f a = b
sa a /\ sf f /\ f a = b auto.
    -A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
(exists (f : A -> B) (a : A), sa a /\ sf f /\ f a = b) ->
exists a : (A -> B) * A,
  (let '(a0, b) := a in sf a0 /\ sa b) /\
  (let '(f, a0) := a in f a0) = b intros [f [a [hyp1 [hyp2 hyp3]]]].A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
b: B
f: A -> B
a: A
hyp1: sa a
hyp2: sf f
hyp3: f a = b
exists a : (A -> B) * A,
  (let '(a0, b) := a in sf a0 /\ sa b) /\
  (let '(f, a0) := a in f a0) = b
      subst.A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
f: A -> B
a: A
hyp1: sa a
hyp2: sf f
exists a0 : (A -> B) * A,
  (let '(a, b) := a0 in sf a /\ sa b) /\
  (let '(f, a) := a0 in f a) = f a exists (f, a).A, B: Type
sf: subset%tea (A -> B)
sa: subset%tea A
f: A -> B
a: A
hyp1: sa a
hyp2: sf f
(sf f /\ sa a) /\ f a = f a tauto.
  Qed.

  (** ** Non-Idempotence of the Applicative *)
  (********************************************************************)
  Lemma fn_nequal_counterexample:
    forall (A B: Type) (f g: A -> B),
      (exists (a: A), (f a <> g a)) -> f <> g.forall (A B : Type) (f g : A -> B),
(exists a : A, f a <> g a) -> f <> g
  Proof.forall (A B : Type) (f g : A -> B),
(exists a : A, f a <> g a) -> f <> g
    intros.A, B: Type
f, g: A -> B
H: exists a : A, f a <> g a
f <> g
    intro contra.A, B: Type
f, g: A -> B
H: exists a : A, f a <> g a
contra: f = g
False
    destruct H as [a Hneq].A, B: Type
f, g: A -> B
a: A
Hneq: f a <> g a
contra: f = g
False
    rewrite contra in Hneq.A, B: Type
f, g: A -> B
a: A
Hneq: g a <> g a
contra: f = g
False
    contradiction.
  Qed.

  Corollary subset_nequal_counterexample:
    forall (A: Type) (a: A) (s1 s2: subset A),
      s1 a -> ~ s2 a ->
      s1 <> s2.forall (A : Type) (a : A) (s1 s2 : subset%tea A),
s1 a -> ~ s2 a -> s1 <> s2
  Proof.forall (A : Type) (a : A) (s1 s2 : subset%tea A),
s1 a -> ~ s2 a -> s1 <> s2
    intros.A: Type
a: A
s1, s2: subset%tea A
H: s1 a
H0: ~ s2 a
s1 <> s2
    apply fn_nequal_counterexample.A: Type
a: A
s1, s2: subset%tea A
H: s1 a
H0: ~ s2 a
exists a : A, s1 a <> s2 a
    exists a.A: Type
a: A
s1, s2: subset%tea A
H: s1 a
H0: ~ s2 a
s1 a <> s2 a intro contra.A: Type
a: A
s1, s2: subset%tea A
H: s1 a
H0: ~ s2 a
contra: s1 a = s2 a
False
    rewrite contra in H.A: Type
a: A
s1, s2: subset%tea A
H: s2 a
H0: ~ s2 a
contra: s1 a = s2 a
False
    contradiction.
  Qed.

  Example not_subset_idem:
    ~ (forall (A: Type) (s: subset A),
          s ⊗ s = map (fun a: A => (a, a)) s).~
(forall (A : Type) (s : subset%tea A),
 s ⊗ s = map (fun a : A => (a, a)) s)
  Proof.~
(forall (A : Type) (s : subset%tea A),
 s ⊗ s = map (fun a : A => (a, a)) s)
    intro contra.contra: forall (A : Type) (s : A -> Prop),
s ⊗ s = map (fun a : A => (a, a)) s
False
    specialize (contra nat ({{1}} ∪ {{2}})).contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
False
    generalize contra.contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}}) -> False
    pose (ctx := subset_nequal_counterexample (nat * nat) (1, 2)).contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : subset%tea (nat * nat),
s1 (1, 2) -> ~ s2 (1, 2) -> s1 <> s2
({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}}) -> False
    unfold not in ctx.contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}}) -> False
    unfold map, Map_subset, mult,Mult_subset.contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
(fun '(a, b) => ({{1}} ∪ {{2}}) a /\ ({{1}} ∪ {{2}}) b) =
(fun b : nat * nat =>
 exists a : nat, ({{1}} ∪ {{2}}) a /\ (a, a) = b) ->
False
    apply ctx.contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
({{1}} ∪ {{2}}) 1 /\ ({{1}} ∪ {{2}}) 2
contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
(exists a : nat, ({{1}} ∪ {{2}}) a /\ (a, a) = (1, 2)) ->
False
    -contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
({{1}} ∪ {{2}}) 1 /\ ({{1}} ∪ {{2}}) 2 simpl_subset.contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
(1 = 1 \/ 2 = 1) /\ (1 = 2 \/ 2 = 2) tauto.
    -contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
(exists a : nat, ({{1}} ∪ {{2}}) a /\ (a, a) = (1, 2)) ->
False intros [a [_ false]].contra: ({{1}} ∪ {{2}}) ⊗ ({{1}} ∪ {{2}}) =
map (fun a : nat => (a, a)) ({{1}} ∪ {{2}})
ctx:= subset_nequal_counterexample (nat * nat) (1, 2): forall s1 s2 : nat * nat -> Prop,
s1 (1, 2) ->
(s2 (1, 2) -> False) -> s1 = s2 -> False
a: nat
false: (a, a) = (1, 2)
False
      now inversion false.
  Qed.

  (** ** The Applicative Functor is Commutative *)
  (********************************************************************)
  Lemma subset_commutative:
    forall (A: Type) (sA: subset A), Center subset%tea A sA.forall (A : Type) (sA : subset%tea A),
Center subset%tea A sA
  Proof.forall (A : Type) (sA : subset%tea A),
Center subset%tea A sA
    intros.A: Type
sA: subset%tea A
Center subset%tea A sA constructor; intros;
     unfold_ops @Mult_subset;
       unfold_ops @Map_subset.A: Type
sA: subset%tea A
B: Type
x: B -> Prop
(fun '(a, b) => x a /\ sA b) =
(fun b : B * A =>
 exists a : A * B,
   (let '(a0, b0) := a in sA a0 /\ x b0) /\
   (let '(x, y) := a in (y, x)) = b)
A: Type
sA: subset%tea A
B: Type
x: B -> Prop
(fun '(a, b) => sA a /\ x b) =
(fun b : A * B =>
 exists a : B * A,
   (let '(a0, b0) := a in x a0 /\ sA b0) /\
   (let '(x, y) := a in (y, x)) = b)
     -A: Type
sA: subset%tea A
B: Type
x: B -> Prop
(fun '(a, b) => x a /\ sA b) =
(fun b : B * A =>
 exists a : A * B,
   (let '(a0, b0) := a in sA a0 /\ x b0) /\
   (let '(x, y) := a in (y, x)) = b) rename x into sB.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
(fun '(a, b) => sB a /\ sA b) =
(fun b : B * A =>
 exists a : A * B,
   (let '(a0, b0) := a in sA a0 /\ sB b0) /\
   (let '(x, y) := a in (y, x)) = b)
       ext [b a].A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
(sB b /\ sA a) =
(exists a0 : A * B,
   (let '(a, b) := a0 in sA a /\ sB b) /\
   (let '(x, y) := a0 in (y, x)) = (b, a))
       propext.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
sB b /\ sA a ->
exists a0 : A * B,
  (let '(a, b) := a0 in sA a /\ sB b) /\
  (let '(x, y) := a0 in (y, x)) = (b, a)
A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
(exists a0 : A * B,
   (let '(a, b) := a0 in sA a /\ sB b) /\
   (let '(x, y) := a0 in (y, x)) = (b, a)) ->
sB b /\ sA a
       +A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
sB b /\ sA a ->
exists a0 : A * B,
  (let '(a, b) := a0 in sA a /\ sB b) /\
  (let '(x, y) := a0 in (y, x)) = (b, a) intros [Ha Hb].A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
Ha: sB b
Hb: sA a
exists a0 : A * B,
  (let '(a, b) := a0 in sA a /\ sB b) /\
  (let '(x, y) := a0 in (y, x)) = (b, a)
         exists (a, b).A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
Ha: sB b
Hb: sA a
(sA a /\ sB b) /\ (b, a) = (b, a) tauto.
       +A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
(exists a0 : A * B,
   (let '(a, b) := a0 in sA a /\ sB b) /\
   (let '(x, y) := a0 in (y, x)) = (b, a)) ->
sB b /\ sA a intros [[a' b'] [H1 H2]].A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a, a': A
b': B
H1: sA a' /\ sB b'
H2: (b', a') = (b, a)
sB b /\ sA a
         inversion H2.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a, a': A
b': B
H1: sA a' /\ sB b'
H2: (b', a') = (b, a)
H0: b' = b
H3: a' = a
sB b /\ sA a subst.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
b: B
a: A
H1: sA a /\ sB b
H2: (b, a) = (b, a)
sB b /\ sA a tauto.
     -A: Type
sA: subset%tea A
B: Type
x: B -> Prop
(fun '(a, b) => sA a /\ x b) =
(fun b : A * B =>
 exists a : B * A,
   (let '(a0, b0) := a in x a0 /\ sA b0) /\
   (let '(x, y) := a in (y, x)) = b) rename x into sB.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
(fun '(a, b) => sA a /\ sB b) =
(fun b : A * B =>
 exists a : B * A,
   (let '(a0, b0) := a in sB a0 /\ sA b0) /\
   (let '(x, y) := a in (y, x)) = b)
       ext [a b].A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
(sA a /\ sB b) =
(exists a0 : B * A,
   (let '(a, b) := a0 in sB a /\ sA b) /\
   (let '(x, y) := a0 in (y, x)) = (a, b))
       propext.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
sA a /\ sB b ->
exists a0 : B * A,
  (let '(a, b) := a0 in sB a /\ sA b) /\
  (let '(x, y) := a0 in (y, x)) = (a, b)
A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
(exists a0 : B * A,
   (let '(a, b) := a0 in sB a /\ sA b) /\
   (let '(x, y) := a0 in (y, x)) = (a, b)) ->
sA a /\ sB b
       +A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
sA a /\ sB b ->
exists a0 : B * A,
  (let '(a, b) := a0 in sB a /\ sA b) /\
  (let '(x, y) := a0 in (y, x)) = (a, b) intros [Ha Hb].A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
Ha: sA a
Hb: sB b
exists a0 : B * A,
  (let '(a, b) := a0 in sB a /\ sA b) /\
  (let '(x, y) := a0 in (y, x)) = (a, b)
         exists (b, a).A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
Ha: sA a
Hb: sB b
(sB b /\ sA a) /\ (a, b) = (a, b) tauto.
       +A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
(exists a0 : B * A,
   (let '(a, b) := a0 in sB a /\ sA b) /\
   (let '(x, y) := a0 in (y, x)) = (a, b)) ->
sA a /\ sB b intros [[b' a'] [H1 H2]].A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b, b': B
a': A
H1: sB b' /\ sA a'
H2: (a', b') = (a, b)
sA a /\ sB b
         inversion H2.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b, b': B
a': A
H1: sB b' /\ sA a'
H2: (a', b') = (a, b)
H0: a' = a
H3: b' = b
sA a /\ sB b subst.A: Type
sA: subset%tea A
B: Type
sB: B -> Prop
a: A
b: B
H1: sB b /\ sA a
H2: (a, b) = (a, b)
sA a /\ sB b tauto.
  Qed.

  #[export] Instance ApplicativeCommutative_subset: ApplicativeCommutative subset.ApplicativeCommutative subset%tea
  Proof.ApplicativeCommutative subset%tea
    constructor.Applicative subset%tea
forall (A : Type) (a : A -> Prop),
Center subset%tea A a
    typeclasses eauto.forall (A : Type) (a : A -> Prop),
Center subset%tea A a
    apply subset_commutative.
  Qed.

End subset_applicative_instance.