From Tealeaves Require Export
  Classes.Functor
  Functors.Early.Subset.

From Coq Require Import
  Relations.Relation_Definitions
  Classes.Morphisms.

Import Monoid.Notations.
Import Functor.Notations.
Import Subset.Notations.

#[local] Generalizable Variables F T A.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.

(** * Container-Like Functors *)
(**********************************************************************)

(** ** Operation <<tosubset>> and <<x ∈ ->>*)
(**********************************************************************)
Class ToSubset (F: Type -> Type) :=
  tosubset: F ⇒ subset.

#[global] Arguments tosubset {F}%function_scope
  {ToSubset} {A}%type_scope.

Definition element_of `{ToSubset F} {A: Type}:
  A -> F A -> Prop := fun a t => tosubset t a.

Lemma element_of_tosubset `{ToSubset F} {A: Type}:
  forall (a:A), element_of a = evalAt a ∘ tosubset.
F: Type -> Type
H: ToSubset F
A: Type
forall a : A, element_of a = evalAt a ∘ tosubset
Proof.
F: Type -> Type
H: ToSubset F
A: Type
forall a : A, element_of a = evalAt a ∘ tosubset
  reflexivity.
Qed.
#[local] Notation "x ∈ t" :=
  (element_of x t) (at level 50): tealeaves_scope.

(** ** Typeclass *)
(**********************************************************************)
Class ContainerFunctor
  (F: Type -> Type)
  `{Map F} `{ToSubset F} :=
  { cont_natural :> Natural (@tosubset F _);
    cont_functor :> Functor F;
    cont_pointwise: forall (A B: Type) (t: F A) (f g: A -> B),
      (forall a, a ∈ t -> f a = g a) -> map F f t = map F g t;
  }.

(** ** Homomorphisms of Container-Like Functors *)
(**********************************************************************)
Class ContainerTransformation
  {F G: Type -> Type}
  `{Map F} `{ToSubset F}
  `{Map G} `{ToSubset G}
  (η: F ⇒ G) :=
  { cont_trans_natural: Natural η;
    cont_trans_commute:
    forall A, tosubset (F := F) = tosubset (F := G) ∘ η A;
  }.

(** * Container Instance for <<subset>> *)
(**********************************************************************)
Section Container_subset.

  Instance ToSubset_set: ToSubset subset :=
    fun (A: Type) (s: subset A) => s.

  Instance Natural_elements_set: Natural (@tosubset subset _).
Natural (@tosubset subset ToSubset_set)
  Proof.
Natural (@tosubset subset ToSubset_set)
    constructor; try typeclasses eauto.
forall (A B : Type) (f : A -> B),
map subset f ∘ tosubset = tosubset ∘ map subset f
    intros.
A, B: Type
f: A -> B
map subset f ∘ tosubset = tosubset ∘ map subset f ext S b.
A, B: Type
f: A -> B
S: A -> Prop
b: B
(map subset f ∘ tosubset) S b =
(tosubset ∘ map subset f) S b reflexivity.
  Qed.

  Lemma subset_pointwise:
    forall (A B: Type) (t: A -> Prop) (f g: A -> B),
      (forall a: A, a ∈ t -> f a = g a) ->
      map subset f t = map subset g t.
forall (A B : Type) (t : A -> Prop) (f g : A -> B),
(forall a : A, a ∈ t -> f a = g a) ->
map subset f t = map subset g t
  Proof.
forall (A B : Type) (t : A -> Prop) (f g : A -> B),
(forall a : A, a ∈ t -> f a = g a) ->
map subset f t = map subset g t
    intros.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
map subset f t = map subset g t ext b.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
map subset f t b = map subset g t b cbv.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ f a = b) =
(exists a : A, t a /\ g a = b) propext.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ f a = b) ->
exists a : A, t a /\ g a = b
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ g a = b) ->
exists a : A, t a /\ f a = b
    intros.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
H0: exists a : A, t a /\ f a = b
exists a : A, t a /\ g a = b
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ g a = b) ->
exists a : A, t a /\ f a = b preprocess.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
exists a : A, t a /\ g a = f x
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ g a = b) ->
exists a : A, t a /\ f a = b setoid_rewrite H.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
exists a : A, t a /\ g a = g x
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
a: A
x ∈ t
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ g a = b) ->
exists a : A, t a /\ f a = b firstorder.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
a: A
x ∈ t
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ g a = b) ->
exists a : A, t a /\ f a = b auto.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
(exists a : A, t a /\ g a = b) ->
exists a : A, t a /\ f a = b
    intros.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
b: B
H0: exists a : A, t a /\ g a = b
exists a : A, t a /\ f a = b preprocess.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
exists a : A, t a /\ f a = g x setoid_rewrite <- H.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
exists a : A, t a /\ f a = f x
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
a: A
x ∈ t firstorder.
A, B: Type
t: A -> Prop
f, g: A -> B
H: forall a : A, a ∈ t -> f a = g a
x: A
H0: t x
a: A
x ∈ t auto.
  Qed.

  Instance ContainerFunctor_subset: ContainerFunctor subset :=
    {| cont_pointwise := subset_pointwise;
    |}.

End Container_subset.

(** * Basic Properties of Containers *)
(**********************************************************************)
Section setlike_functor_theory.

  Context
    (F: Type -> Type)
    `{ContainerFunctor F}
    {A B: Type}.

  Implicit Types (t: F A) (b: B) (a: A) (f g: A -> B).

  (** ** Interaction between (∈) and <<map>> *)
  (********************************************************************)

  (** Naturality relates elements before and after a map. *)
  Theorem in_map_iff: forall t f b,
      b ∈ map F f t <-> exists a: A, a ∈ t /\ f a = b.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t f b,
b ∈ map F f t <-> (exists a, a ∈ t /\ f a = b)
  Proof.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t f b,
b ∈ map F f t <-> (exists a, a ∈ t /\ f a = b)
    introv.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
b: B
b ∈ map F f t <-> (exists a, a ∈ t /\ f a = b) compose near t on left.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
b: B
(element_of b ∘ map F f) t <->
(exists a, a ∈ t /\ f a = b)
    rewrite element_of_tosubset.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
b: B
(evalAt b ∘ tosubset ∘ map F f) t <->
(exists a, a ∈ t /\ f a = b)
    reassociate -> on left.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
b: B
(evalAt b ∘ (tosubset ∘ map F f)) t <->
(exists a, a ∈ t /\ f a = b)
    unfold element_of.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
b: B
(evalAt b ∘ (tosubset ∘ map F f)) t <->
(exists a, tosubset t a /\ f a = b)
    rewrite <- (natural (G:=(-> Prop))).
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
b: B
(evalAt b ∘ (map subset f ∘ tosubset)) t <->
(exists a, tosubset t a /\ f a = b)
    reflexivity.
  Qed.

  (** This next property says that applying <<f>> (or on the
      right-hand side, appling <<map f>>) is monotone with respect to
      the <<∈>> relation. *)
  Corollary in_map_mono: forall t f a,
      a ∈ t -> f a ∈ map F f t.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t f a, a ∈ t -> f a ∈ map F f t
  Proof.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t f a, a ∈ t -> f a ∈ map F f t
    introv.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
a: A
a ∈ t -> f a ∈ map F f t rewrite in_map_iff.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> B
a: A
a ∈ t -> exists a0, a0 ∈ t /\ f a0 = f a now exists a.
  Qed.

  (** ** Respectfulness Conditions *)
  (********************************************************************)
  (** Renaming to keep consistent name scheme *)
  Corollary map_respectful: forall t (f g: A -> B),
      (forall a, a ∈ t -> f a = g a) -> map F f t = map F g t.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t f g,
(forall a, a ∈ t -> f a = g a) ->
map F f t = map F g t
  Proof.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t f g,
(forall a, a ∈ t -> f a = g a) ->
map F f t = map F g t
    apply (cont_pointwise (F := F)).
  Qed.

  Corollary map_respectful_id: forall t (f: A -> A),
      (forall a, a ∈ t -> f a = a) -> map F f t = t.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t (f : A -> A),
(forall a, a ∈ t -> f a = a) -> map F f t = t
  Proof.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
forall t (f : A -> A),
(forall a, a ∈ t -> f a = a) -> map F f t = t
    intros.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> A
H2: forall a, a ∈ t -> f a = a
map F f t = t replace t with (map F id t) at 2
      by now rewrite (fun_map_id (F := F)).
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f: A -> A
H2: forall a, a ∈ t -> f a = a
map F f t = map F id t
    now apply (cont_pointwise (F := F)).
  Qed.

End setlike_functor_theory.

(** ** Properness Conditions *)
(**********************************************************************)
Definition pointwise_equal_on
  (F: Type -> Type) {A B} `{ToSubset F}:
  F A -> relation (A -> B) :=
  fun t f g => (forall a: A, a ∈ t -> f a = g a).

Definition respectively_equal_at {A B}:
  A -> A -> relation (A -> B) :=
  fun (a1 a2: A) (f g: A -> B) => f a1 = g a2.

Definition equal_at {A B}: A -> relation (A -> B) :=
  fun (a: A) (f g: A -> B) => f a = g a.

Definition injective_relation {A B}
  (R: relation A) (R': relation B): relation (A -> B) :=
  fun f g => forall a1 a2: A, R' (f a1) (g a2) -> R a1 a2.

Infix "<++" := injective_relation (at level 55).

Definition rigid_relation {A B}
  (R: relation A) (R': relation B): relation (A -> B) :=
  fun f g => forall a1 a2: A, R' (f a1) (g a2) <-> R a1 a2.

Infix "<++>" := rigid_relation (at level 55).

#[export] Instance Proper_Container_Map
  (F: Type -> Type) `{ContainerFunctor F}:
  (forall (A B: Type) (t: F A),
      Proper (pointwise_equal_on F t (B := B) ++> equal_at t) (map F)).
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
forall (A B : Type) (t : F A),
Proper (pointwise_equal_on F t ==> equal_at t) (map F)
Proof.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
forall (A B : Type) (t : F A),
Proper (pointwise_equal_on F t ==> equal_at t) (map F)
  intros.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
Proper (pointwise_equal_on F t ==> equal_at t) (map F)
  unfold Proper.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
(pointwise_equal_on F t ==> equal_at t)%signature
  (map F) (map F)
  intros f g Hpw.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f, g: A -> B
Hpw: pointwise_equal_on F t f g
equal_at t (map F f) (map F g)
  unfold pointwise_equal_on, equal_at in *.
F: Type -> Type
H: Map F
H0: ToSubset F
H1: ContainerFunctor F
A, B: Type
t: F A
f, g: A -> B
Hpw: forall a : A, a ∈ t -> f a = g a
map F f t = map F g t
  now apply cont_pointwise.
Qed.

(** * Quantification over Elements (<<Forall>>, <<Forany>>) *)
(* These are not the best combinators to use, it's typically easier to reason
   when Forall is defined in terms of mapReduce *)
(**********************************************************************)
Section quantification.

  Context `{ContainerFunctor T}.

  Definition Forall_elt `(P: A -> Prop) (t: T A): Prop :=
    forall (a: A), a ∈ t -> P a.

  Definition Forany_elt `(P: A -> Prop) (t :T A): Prop :=
    exists (a: A), a ∈ t /\ P a.

End quantification.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Notation "x ∈ t" :=
    (element_of x t) (at level 50): tealeaves_scope.
End Notations.