Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
(** If [B] is a (bounded) lattice, then so is [A -> B], pointwise. This relies on functional extensionality. *)Sectioncontents.Context `{Funext}.Context {AB : Type}.Context `{BJoin : Join B}.Context `{BMeet : Meet B}.Context `{BBottom : Bottom B}.Context `{BTop : Top B}.Global Instancebot_fun : Bottom (A -> B)
:= fun_ => ⊥.Global Instancetop_fun : Top (A -> B)
:= fun_ => ⊤.Global Instancejoin_fun : Join (A -> B) :=
fun (fg : A -> B) (a : A) => (f a) ⊔ (g a).Global Instancemeet_fun : Meet (A -> B) :=
fun (fg : 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 Ltacreduce_fun := compute; intros; apply path_forall; intro.
H: Funext A, B: Type BJoin: Join B BMeet: Meet B BBottom: Bottom B BTop: Top B IsLattice0: 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)
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
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
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
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.
H: Funext A, B: Type BJoin: Join B BMeet: Meet B BBottom: Bottom B BTop: Top B IsBoundedJoinSemiLattice0: 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)
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.
H: Funext A, B: Type BJoin: Join B BMeet: Meet B BBottom: Bottom B BTop: Top B IsBoundedMeetSemiLattice0: 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)
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.
H: Funext A, B: Type BJoin: Join B BMeet: Meet B BBottom: Bottom B BTop: Top B IsBoundedLattice0: 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