Require ImportRequire Import
  HoTT.Classes.interfaces.abstract_algebra.

(** If [B] is a (bounded) lattice, then so is [A -> B], pointwise.
    This relies on functional extensionality. *)
Section contents.
  Context `{Funext}.

  Context {A B : Type}.
  Context `{BJoin : Join B}.
  Context `{BMeet : Meet B}.
  Context `{BBottom : Bottom B}.
  Context `{BTop : Top B}.

  #[export] Instance bot_fun : Bottom (A -> B)
    := fun _ => ⊥.

  #[export] Instance top_fun : Top (A -> B)
    := fun _ => ⊤.

  #[export] Instance join_fun : Join (A -> B) :=
    fun (f g : A -> B) (a : A) => (f a) ⊔ (g a).

  #[export] Instance meet_fun : Meet (A -> B) :=
    fun (f g : A -> B) (a : A) => (f a) ⊓ (g a).

  (** Try to solve some of the lattice obligations automatically *)
  Create HintDb lattice_hints.
  #[local]
  Hint Resolve
       associativity
       absorption
       commutativity | 1 : lattice_hints.
  Local Ltac reduce_fun := compute; intros; apply path_forall; intro.

  #[export] Instance lattice_fun `{!IsLattice B} : IsLattice (A -> B).
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
IsLattice (A -> B)
  Proof.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
IsLattice (A -> B)
    repeat split; try apply _; reduce_fun.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y, z: A -> B
x0: A
BJoin (x x0) (BJoin (y x0) (z x0)) = BJoin (BJoin (x x0) (y x0)) (z x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BJoin (x x0) (y x0) = BJoin (y x0) (x x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x: A -> B
x0: A
BJoin (x x0) (x x0) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y, z: A -> B
x0: A
BMeet (x x0) (BMeet (y x0) (z x0)) = BMeet (BMeet (x x0) (y x0)) (z x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BMeet (x x0) (y x0) = BMeet (y x0) (x x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x: A -> B
x0: A
BMeet (x x0) (x x0) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BJoin (x x0) (BMeet (x x0) (y x0)) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BMeet (x x0) (BJoin (x x0) (y x0)) = x x0
    1,4: apply associativity.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BJoin (x x0) (y x0) = BJoin (y x0) (x x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x: A -> B
x0: A
BJoin (x x0) (x x0) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BMeet (x x0) (y x0) = BMeet (y x0) (x x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x: A -> B
x0: A
BMeet (x x0) (x x0) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BJoin (x x0) (BMeet (x x0) (y x0)) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BMeet (x x0) (BJoin (x x0) (y x0)) = x x0
    1,3: apply commutativity.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x: A -> B
x0: A
BJoin (x x0) (x x0) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x: A -> B
x0: A
BMeet (x x0) (x x0) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BJoin (x x0) (BMeet (x x0) (y x0)) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BMeet (x x0) (BJoin (x x0) (y x0)) = x x0
    1,2: apply binary_idempotent.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BJoin (x x0) (BMeet (x x0) (y x0)) = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsLattice0: IsLattice B
x, y: A -> B
x0: A
BMeet (x x0) (BJoin (x x0) (y x0)) = x x0
    1,2: apply absorption.
  Defined.

  Instance boundedjoinsemilattice_fun
   `{!IsBoundedJoinSemiLattice B} :
    IsBoundedJoinSemiLattice (A -> B).
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
IsBoundedJoinSemiLattice (A -> B)
  Proof.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
IsBoundedJoinSemiLattice (A -> B)
    repeat split; try apply _; reduce_fun.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x, y, z: A -> B
x0: A
BJoin (x x0) (BJoin (y x0) (z x0)) = BJoin (BJoin (x x0) (y x0)) (z x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
y: A -> B
x: A
BJoin BBottom (y x) = y x
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x: A -> B
x0: A
BJoin (x x0) BBottom = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x, y: A -> B
x0: A
BJoin (x x0) (y x0) = BJoin (y x0) (x x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x: A -> B
x0: A
BJoin (x x0) (x x0) = x x0
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x, y, z: A -> B
x0: A
BJoin (x x0) (BJoin (y x0) (z x0)) = BJoin (BJoin (x x0) (y x0)) (z x0) apply associativity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
y: A -> B
x: A
BJoin BBottom (y x) = y x apply left_identity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x: A -> B
x0: A
BJoin (x x0) BBottom = x x0 apply right_identity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x, y: A -> B
x0: A
BJoin (x x0) (y x0) = BJoin (y x0) (x x0) apply commutativity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice B
x: A -> B
x0: A
BJoin (x x0) (x x0) = x x0 apply binary_idempotent.
  Defined.

  Instance boundedmeetsemilattice_fun
   `{!IsBoundedMeetSemiLattice B} :
    IsBoundedMeetSemiLattice (A -> B).
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
IsBoundedMeetSemiLattice (A -> B)
  Proof.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
IsBoundedMeetSemiLattice (A -> B)
    repeat split; try apply _; reduce_fun.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x, y, z: A -> B
x0: A
BMeet (x x0) (BMeet (y x0) (z x0)) = BMeet (BMeet (x x0) (y x0)) (z x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
y: A -> B
x: A
BMeet BTop (y x) = y x
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x: A -> B
x0: A
BMeet (x x0) BTop = x x0
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x, y: A -> B
x0: A
BMeet (x x0) (y x0) = BMeet (y x0) (x x0)
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x: A -> B
x0: A
BMeet (x x0) (x x0) = x x0
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x, y, z: A -> B
x0: A
BMeet (x x0) (BMeet (y x0) (z x0)) = BMeet (BMeet (x x0) (y x0)) (z x0) apply associativity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
y: A -> B
x: A
BMeet BTop (y x) = y x apply left_identity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x: A -> B
x0: A
BMeet (x x0) BTop = x x0 apply right_identity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x, y: A -> B
x0: A
BMeet (x x0) (y x0) = BMeet (y x0) (x x0) apply commutativity.
    *
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedMeetSemiLattice0: IsBoundedMeetSemiLattice B
x: A -> B
x0: A
BMeet (x x0) (x x0) = x x0 apply binary_idempotent.
  Defined.

  #[export] Instance boundedlattice_fun
   `{!IsBoundedLattice B} : IsBoundedLattice (A -> B).
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedLattice0: IsBoundedLattice B
IsBoundedLattice (A -> B)
  Proof.
H: Funext
A, B: Type
BJoin: Join B
BMeet: Meet B
BBottom: Bottom B
BTop: Top B
IsBoundedLattice0: IsBoundedLattice B
IsBoundedLattice (A -> B)
    repeat split; try apply _; reduce_fun; apply absorption.
  Defined.
End contents.

#[export]
  Hint Resolve
       associativity
       absorption
       commutativity | 1 : lattice_hints.