Mathlib.Order.Copy

Module docstring

{"# Tooling to make copies of lattice structures

Sometimes it is useful to make a copy of a lattice structure where one replaces the data parts with provably equal definitions that have better definitional properties. "}

OrderTop.copy definition

 {h : LE α} {h' : LE α} (c : @OrderTop α h') (top : α) (eq_top : top = (by infer_instance : Top α).top)
  (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderTop α h

Full source

/-- A function to create a provable equal copy of a top order
with possibly different definitional equalities. -/
def OrderTop.copy {h : LE α} {h' : LE α} (c : @OrderTop α h')
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderTop α h :=
  @OrderTop.mk α h { top := top } fun _ ↦ by simp [eq_top, le_eq]

Copy of an order with top element

Informal description

Given an order `(α, ≤)` with a top element `⊤` (i.e., an instance of `OrderTop`), a new element `top : α`, and proofs that `top` is equal to the existing top element and that the order relations are equivalent, this function constructs a new `OrderTop` instance with the specified `top` as the greatest element.

OrderBot.copy definition

 {h : LE α} {h' : LE α} (c : @OrderBot α h') (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderBot α h

Full source

/-- A function to create a provable equal copy of a bottom order
with possibly different definitional equalities. -/
def OrderBot.copy {h : LE α} {h' : LE α} (c : @OrderBot α h')
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderBot α h :=
  @OrderBot.mk α h { bot := bot } fun _ ↦ by simp [eq_bot, le_eq]

Copy of an order with bottom element

Informal description

Given an order `(α, ≤)` with a bottom element `⊥` (i.e., an instance of `OrderBot`), a new element `bot : α`, and proofs that `bot` is equal to the existing bottom element and that the order relations are equivalent, this function constructs a new `OrderBot` instance with the specified `bot` as the least element.

BoundedOrder.copy definition

 {h : LE α} {h' : LE α} (c : @BoundedOrder α h') (top : α) (eq_top : top = (by infer_instance : Top α).top) (bot : α)
  (eq_bot : bot = (by infer_instance : Bot α).bot) (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @BoundedOrder α h

Full source

/-- A function to create a provable equal copy of a bounded order
with possibly different definitional equalities. -/
def BoundedOrder.copy {h : LE α} {h' : LE α} (c : @BoundedOrder α h')
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @BoundedOrder α h :=
  @BoundedOrder.mk α h (@OrderTop.mk α h { top := top } (fun _ ↦ by simp [eq_top, le_eq]))
    (@OrderBot.mk α h { bot := bot } (fun _ ↦ by simp [eq_bot, le_eq]))

Copy of a bounded order

Informal description

Given a bounded order `(α, ≤)` with top element `⊤` and bottom element `⊥`, a new top element `top : α`, a new bottom element `bot : α`, proofs that `top` equals the original top element and `bot` equals the original bottom element, and a proof that the order relations are equivalent, this function constructs a new bounded order instance with the specified `top` and `bot` as the greatest and least elements, respectively.

Lattice.copy definition

 (c : Lattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (sup : α → α → α)
  (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) :
  Lattice α

Full source

/-- A function to create a provable equal copy of a lattice
with possibly different definitional equalities. -/
def Lattice.copy (c : Lattice α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) : Lattice α where
  le := le
  sup := sup
  inf := inf
  lt := fun a b ↦ le a b ∧ ¬ le b a
  le_refl := by intros; simp [eq_le]
  le_trans := by intro _ _ _ hab hbc; rw [eq_le] at hab hbc ⊢; exact le_trans hab hbc
  le_antisymm := by intro _ _ hab hba; simp_rw [eq_le] at hab hba; exact le_antisymm hab hba
  le_sup_left := by intros; simp [eq_le, eq_sup]
  le_sup_right := by intros; simp [eq_le, eq_sup]
  sup_le := by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_sup, hac, hbc]
  inf_le_left := by intros; simp [eq_le, eq_inf]
  inf_le_right := by intros; simp [eq_le, eq_inf]
  le_inf := by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_inf, hac, hbc]

Copy of a lattice structure with modified definitions

Informal description

Given a lattice structure on a type $\alpha$, this function creates a new lattice structure with the same operations (join $\sqcup$ and meet $\sqcap$) and order relation $\leq$, but potentially with different definitional properties. The new structure is provably equal to the original one, but may have better computational behavior. Specifically, it takes: - An existing lattice $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) and returns a new lattice structure with these components, while preserving all lattice axioms.

DistribLattice.copy definition

 (c : DistribLattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (sup : α → α → α)
  (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) :
  DistribLattice α

Full source

/-- A function to create a provable equal copy of a distributive lattice
with possibly different definitional equalities. -/
def DistribLattice.copy (c : DistribLattice α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) : DistribLattice α where
  toLattice := Lattice.copy (@DistribLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
  le_sup_inf := by intros; simp [eq_le, eq_sup, eq_inf, le_sup_inf]

Copy of a distributive lattice structure with modified definitions

Informal description

Given a distributive lattice structure on a type $\alpha$, this function creates a new distributive lattice structure with the same operations (join $\sqcup$ and meet $\sqcap$) and order relation $\leq$, but potentially with different definitional properties. The new structure is provably equal to the original one, while maintaining the distributivity property. Specifically, it takes: - An existing distributive lattice $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) and returns a new distributive lattice structure with these components.

GeneralizedHeytingAlgebra.copy definition

 (c : GeneralizedHeytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
  (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) (himp : α → α → α)
  (eq_himp : himp = (by infer_instance : HImp α).himp) : GeneralizedHeytingAlgebra α

Full source

/-- A function to create a provable equal copy of a generalised heyting algebra
with possibly different definitional equalities. -/
def GeneralizedHeytingAlgebra.copy (c : GeneralizedHeytingAlgebra α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (himp : α → α → α) (eq_himp : himp = (by infer_instance : HImp α).himp) :
    GeneralizedHeytingAlgebra α where
  __ := Lattice.copy (@GeneralizedHeytingAlgebra.toLattice α c) le eq_le sup eq_sup inf eq_inf
  __ := OrderTop.copy (@GeneralizedHeytingAlgebra.toOrderTop α c) top eq_top
    (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
  himp := himp
  le_himp_iff _ _ _ := by simp [eq_le, eq_himp, eq_inf]

Copy of a generalized Heyting algebra with modified definitions

Informal description

Given a generalized Heyting algebra structure on a type $\alpha$, this function creates a provably equal copy with potentially different definitional properties. The new structure has: - A new order relation $\leq$ (with proof that it matches the original) - A new top element $\top$ (with proof that it matches the original) - New supremum $\sqcup$ and infimum $\sqcap$ operations (with proofs they match the original) - A new Heyting implication operation $\Rightarrow$ (with proof it matches the original) The resulting structure maintains all generalized Heyting algebra axioms while potentially improving computational behavior.

GeneralizedCoheytingAlgebra.copy definition

 (c : GeneralizedCoheytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (bot : α)
  (eq_bot : bot = (by infer_instance : Bot α).bot) (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
  (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) (sdiff : α → α → α)
  (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) : GeneralizedCoheytingAlgebra α

Full source

/-- A function to create a provable equal copy of a generalised coheyting algebra
with possibly different definitional equalities. -/
def GeneralizedCoheytingAlgebra.copy (c : GeneralizedCoheytingAlgebra α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sdiff : α → α → α) (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) :
    GeneralizedCoheytingAlgebra α where
  __ := Lattice.copy (@GeneralizedCoheytingAlgebra.toLattice α c) le eq_le sup eq_sup inf eq_inf
  __ := OrderBot.copy (@GeneralizedCoheytingAlgebra.toOrderBot α c) bot eq_bot
    (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
  sdiff := sdiff
  sdiff_le_iff := by simp [eq_le, eq_sdiff, eq_sup]

Copy of a generalized co-Heyting algebra with modified definitions

Informal description

Given a generalized co-Heyting algebra structure on a type $\alpha$, this function creates a new generalized co-Heyting algebra structure with the same operations (join $\sqcup$, meet $\sqcap$, difference $\setminus$) and order relation $\leq$, but potentially with different definitional properties. The new structure is provably equal to the original one, while maintaining the adjunction property between $\setminus$ and $\sqcup$. Specifically, it takes: - An existing generalized co-Heyting algebra $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new bottom element $bot$ (with proof $eq\_bot$ that it matches the original $\bot$) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) - A new difference operation $sdiff$ (with proof $eq\_sdiff$ that it matches the original $\setminus$) and returns a new generalized co-Heyting algebra structure with these components.

HeytingAlgebra.copy definition

 (c : HeytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (himp : α → α → α)
  (eq_himp : himp = (by infer_instance : HImp α).himp) (compl : α → α)
  (eq_compl : compl = (by infer_instance : HasCompl α).compl) : HeytingAlgebra α

Full source

/-- A function to create a provable equal copy of a heyting algebra
with possibly different definitional equalities. -/
def HeytingAlgebra.copy (c : HeytingAlgebra α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (himp : α → α → α) (eq_himp : himp = (by infer_instance : HImp α).himp)
    (compl : α → α) (eq_compl : compl = (by infer_instance : HasCompl α).compl) :
    HeytingAlgebra α where
  toGeneralizedHeytingAlgebra := GeneralizedHeytingAlgebra.copy
    (@HeytingAlgebra.toGeneralizedHeytingAlgebra α c) le eq_le top eq_top sup eq_sup inf eq_inf himp
    eq_himp
  __ := OrderBot.copy (@HeytingAlgebra.toOrderBot α c) bot eq_bot
    (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
  compl := compl
  himp_bot := by simp [eq_le, eq_himp, eq_bot, eq_compl]

Copy of a Heyting algebra with modified definitions

Informal description

Given a Heyting algebra structure on a type $\alpha$, this function creates a provably equal copy with potentially different definitional properties. The new structure has: - A new order relation $\leq$ (with proof that it matches the original) - A new top element $\top$ and bottom element $\bot$ (with proofs that they match the original) - New supremum $\sqcup$ and infimum $\sqcap$ operations (with proofs they match the original) - A new Heyting implication operation $\Rightarrow$ (with proof it matches the original) - A new pseudo-complement operation $\neg$ (with proof it matches the original) The resulting structure maintains all Heyting algebra axioms while potentially improving computational behavior.

CoheytingAlgebra.copy definition

 (c : CoheytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (sdiff : α → α → α)
  (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) (hnot : α → α)
  (eq_hnot : hnot = (by infer_instance : HNot α).hnot) : CoheytingAlgebra α

Full source

/-- A function to create a provable equal copy of a coheyting algebra
with possibly different definitional equalities. -/
def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sdiff : α → α → α) (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff)
    (hnot : α → α) (eq_hnot : hnot = (by infer_instance : HNot α).hnot) :
    CoheytingAlgebra α where
  toGeneralizedCoheytingAlgebra := GeneralizedCoheytingAlgebra.copy
    (@CoheytingAlgebra.toGeneralizedCoheytingAlgebra α c) le eq_le bot eq_bot sup eq_sup inf eq_inf
      sdiff eq_sdiff
  __ := OrderTop.copy (@CoheytingAlgebra.toOrderTop α c) top eq_top
    (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
  hnot := hnot
  top_sdiff := by simp [eq_le, eq_sdiff, eq_top, eq_hnot]

Copy of a co-Heyting algebra with modified definitions

Informal description

Given a co-Heyting algebra structure on a type $\alpha$, this function creates a new co-Heyting algebra structure with the same operations (join $\sqcup$, meet $\sqcap$, difference $\setminus$, negation $\neg$) and order relation $\leq$, but potentially with different definitional properties. The new structure is provably equal to the original one, while maintaining the adjunction property between $\setminus$ and $\sqcup$. Specifically, it takes: - An existing co-Heyting algebra $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new top element $top$ (with proof $eq\_top$ that it matches the original $\top$) - A new bottom element $bot$ (with proof $eq\_bot$ that it matches the original $\bot$) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) - A new difference operation $sdiff$ (with proof $eq\_sdiff$ that it matches the original $\setminus$) - A new negation operation $hnot$ (with proof $eq\_hnot$ that it matches the original $\neg$) and returns a new co-Heyting algebra structure with these components.

BiheytingAlgebra.copy definition

 (c : BiheytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (sdiff : α → α → α)
  (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) (hnot : α → α)
  (eq_hnot : hnot = (by infer_instance : HNot α).hnot) (himp : α → α → α)
  (eq_himp : himp = (by infer_instance : HImp α).himp) (compl : α → α)
  (eq_compl : compl = (by infer_instance : HasCompl α).compl) : BiheytingAlgebra α

Full source

/-- A function to create a provable equal copy of a biheyting algebra
with possibly different definitional equalities. -/
def BiheytingAlgebra.copy (c : BiheytingAlgebra α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sdiff : α → α → α) (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff)
    (hnot : α → α) (eq_hnot : hnot = (by infer_instance : HNot α).hnot)
    (himp : α → α → α) (eq_himp : himp = (by infer_instance : HImp α).himp)
    (compl : α → α) (eq_compl : compl = (by infer_instance : HasCompl α).compl) :
    BiheytingAlgebra α where
  toHeytingAlgebra := HeytingAlgebra.copy (@BiheytingAlgebra.toHeytingAlgebra α c) le eq_le top
    eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl
  __ := CoheytingAlgebra.copy (@BiheytingAlgebra.toCoheytingAlgebra α c) le eq_le top eq_top bot
    eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot

Copy of a bi-Heyting algebra with modified definitions

Informal description

Given a bi-Heyting algebra structure on a type $\alpha$, this function creates a provably equal copy with potentially different definitional properties. The new structure has: - A new order relation $\leq$ (with proof that it matches the original) - A new top element $\top$ and bottom element $\bot$ (with proofs that they match the original) - New supremum $\sqcup$ and infimum $\sqcap$ operations (with proofs they match the original) - A new difference operation $\setminus$ (with proof it matches the original) - A new negation operation $\neg$ (with proof it matches the original) - A new Heyting implication operation $\Rightarrow$ (with proof it matches the original) - A new pseudo-complement operation $\neg$ (with proof it matches the original) The resulting structure maintains all bi-Heyting algebra axioms while potentially improving computational behavior.

CompleteLattice.copy definition

 (c : CompleteLattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (sSup : Set α → α)
  (eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
  (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : CompleteLattice α

Full source

/-- A function to create a provable equal copy of a complete lattice
with possibly different definitional equalities. -/
def CompleteLattice.copy (c : CompleteLattice α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup)
    (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) :
    CompleteLattice α where
  toLattice := Lattice.copy (@CompleteLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
  top := top
  bot := bot
  sSup := sSup
  sInf := sInf
  le_sSup := by intro _ _ h; simp [eq_le, eq_sSup, le_sSup _ _ h]
  sSup_le := by intro _ _ h; simpa [eq_le, eq_sSup] using h
  sInf_le := by intro _ _ h; simp [eq_le, eq_sInf, sInf_le _ _ h]
  le_sInf := by intro _ _ h; simpa [eq_le, eq_sInf] using h
  le_top := by intros; simp [eq_le, eq_top]
  bot_le := by intros; simp [eq_le, eq_bot]

Copy of a complete lattice structure with modified definitions

Informal description

Given a complete lattice structure on a type $\alpha$, this function creates a new complete lattice structure with the same operations (join $\sqcup$, meet $\sqcap$, top $\top$, bottom $\bot$, supremum $\bigsqcup$, and infimum $\bigsqcap$) and order relation $\leq$, but potentially with different definitional properties. The new structure is provably equal to the original one, but may have better computational behavior. Specifically, it takes: - An existing complete lattice $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new top element $top$ (with proof $eq\_top$ that it matches the original) - A new bottom element $bot$ (with proof $eq\_bot$ that it matches the original) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) - A new set supremum operation $sSup$ (with proof $eq\_sSup$ that it matches the original) - A new set infimum operation $sInf$ (with proof $eq\_sInf$ that it matches the original) and returns a new complete lattice structure with these components, while preserving all complete lattice axioms.

Frame.copy definition

 (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (himp : α → α → α)
  (eq_himp : himp = (by infer_instance : HImp α).himp) (compl : α → α)
  (eq_compl : compl = (by infer_instance : HasCompl α).compl) (sSup : Set α → α)
  (eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
  (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : Frame α

Full source

/-- A function to create a provable equal copy of a frame with possibly different definitional
equalities. -/
def Frame.copy (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (himp : α → α → α) (eq_himp : himp = (by infer_instance : HImp α).himp)
    (compl : α → α) (eq_compl : compl = (by infer_instance : HasCompl α).compl)
    (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup)
    (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : Frame α where
  toCompleteLattice := CompleteLattice.copy (@Frame.toCompleteLattice α c)
    le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf
  __ := HeytingAlgebra.copy (@Frame.toHeytingAlgebra α c)
    le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl

Copy of a frame with modified definitions

Informal description

Given a frame structure on a type $\alpha$, this function creates a provably equal copy with potentially different definitional properties. The new structure has: - A new order relation $\leq$ (with proof that it matches the original) - A new top element $\top$ and bottom element $\bot$ (with proofs that they match the original) - New supremum $\sqcup$ and infimum $\sqcap$ operations (with proofs they match the original) - A new Heyting implication operation $\Rightarrow$ (with proof it matches the original) - A new pseudo-complement operation $\neg$ (with proof it matches the original) - New set supremum $\bigsqcup$ and infimum $\bigsqcap$ operations (with proofs they match the original) The resulting structure maintains all frame axioms while potentially improving computational behavior.

Coframe.copy definition

 (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (sdiff : α → α → α)
  (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) (hnot : α → α)
  (eq_hnot : hnot = (by infer_instance : HNot α).hnot) (sSup : Set α → α)
  (eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
  (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : Coframe α

Full source

/-- A function to create a provable equal copy of a coframe with possibly different definitional
equalities. -/
def Coframe.copy (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sdiff : α → α → α) (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff)
    (hnot : α → α) (eq_hnot : hnot = (by infer_instance : HNot α).hnot)
    (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup)
    (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : Coframe α where
  toCompleteLattice := CompleteLattice.copy (@Coframe.toCompleteLattice α c)
    le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf
  __ := CoheytingAlgebra.copy (@Coframe.toCoheytingAlgebra α c)
    le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot

Copy of a coframe with modified definitions

Informal description

Given a coframe structure on a type $\alpha$, this function creates a new coframe structure with the same operations (join $\sqcup$, meet $\sqcap$, difference $\setminus$, negation $\neg$, top $\top$, bottom $\bot$, supremum $\bigsqcup$, and infimum $\bigsqcap$) and order relation $\leq$, but potentially with different definitional properties. The new structure is provably equal to the original one, while maintaining the adjunction property between $\setminus$ and $\sqcup$. Specifically, it takes: - An existing coframe $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new top element $top$ (with proof $eq\_top$ that it matches the original $\top$) - A new bottom element $bot$ (with proof $eq\_bot$ that it matches the original $\bot$) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) - A new difference operation $sdiff$ (with proof $eq\_sdiff$ that it matches the original $\setminus$) - A new negation operation $hnot$ (with proof $eq\_hnot$ that it matches the original $\neg$) - A new set supremum operation $sSup$ (with proof $eq\_sSup$ that it matches the original) - A new set infimum operation $sInf$ (with proof $eq\_sInf$ that it matches the original) and returns a new coframe structure with these components, while preserving all coframe axioms.

CompleteDistribLattice.copy definition

 (c : CompleteDistribLattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
  (eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
  (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
  (eq_inf : inf = (by infer_instance : Min α).min) (sdiff : α → α → α)
  (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) (hnot : α → α)
  (eq_hnot : hnot = (by infer_instance : HNot α).hnot) (himp : α → α → α)
  (eq_himp : himp = (by infer_instance : HImp α).himp) (compl : α → α)
  (eq_compl : compl = (by infer_instance : HasCompl α).compl) (sSup : Set α → α)
  (eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
  (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : CompleteDistribLattice α

Full source

/-- A function to create a provable equal copy of a complete distributive lattice
with possibly different definitional equalities. -/
def CompleteDistribLattice.copy (c : CompleteDistribLattice α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (top : α) (eq_top : top = (by infer_instance : Top α).top)
    (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sdiff : α → α → α) (eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff)
    (hnot : α → α) (eq_hnot : hnot = (by infer_instance : HNot α).hnot)
    (himp : α → α → α) (eq_himp : himp = (by infer_instance : HImp α).himp)
    (compl : α → α) (eq_compl : compl = (by infer_instance : HasCompl α).compl)
    (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup)
    (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) :
    CompleteDistribLattice α where
  toFrame := Frame.copy (@CompleteDistribLattice.toFrame α c) le eq_le top eq_top bot eq_bot sup
    eq_sup inf eq_inf himp eq_himp compl eq_compl sSup eq_sSup sInf eq_sInf
  __ := Coframe.copy (@CompleteDistribLattice.toCoframe α c) le eq_le top eq_top bot eq_bot sup
    eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot sSup eq_sSup sInf eq_sInf

Copy of a complete distributive lattice with modified definitions

Informal description

Given a complete distributive lattice structure on a type $\alpha$, this function creates a provably equal copy with potentially different definitional properties. The new structure has: - A new order relation $\leq$ (with proof that it matches the original) - A new top element $\top$ and bottom element $\bot$ (with proofs that they match the original) - New supremum $\sqcup$ and infimum $\sqcap$ operations (with proofs they match the original) - A new difference operation $\setminus$ (with proof it matches the original) - A new negation operation $\neg$ (with proof it matches the original) - A new Heyting implication operation $\Rightarrow$ (with proof it matches the original) - A new pseudo-complement operation $\neg$ (with proof it matches the original) - New set supremum $\bigsqcup$ and infimum $\bigsqcap$ operations (with proofs they match the original) The resulting structure maintains all complete distributive lattice axioms while potentially improving computational behavior.

ConditionallyCompleteLattice.copy definition

 (c : ConditionallyCompleteLattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (sup : α → α → α)
  (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
  (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
  (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : ConditionallyCompleteLattice α

Full source

/-- A function to create a provable equal copy of a conditionally complete lattice
with possibly different definitional equalities. -/
def ConditionallyCompleteLattice.copy (c : ConditionallyCompleteLattice α)
    (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
    (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
    (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min)
    (sSup : Set α → α) (eq_sSup : sSup = (by infer_instance : SupSet α).sSup)
    (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) :
    ConditionallyCompleteLattice α where
  toLattice := Lattice.copy (@ConditionallyCompleteLattice.toLattice α c)
    le eq_le sup eq_sup inf eq_inf
  sSup := sSup
  sInf := sInf
  le_csSup := by intro _ _ hb h; subst_vars; exact le_csSup _ _ hb h
  csSup_le := by intro _ _ hb h; subst_vars; exact csSup_le _ _ hb h
  csInf_le := by intro _ _ hb h; subst_vars; exact csInf_le _ _ hb h
  le_csInf := by intro _ _ hb h; subst_vars; exact le_csInf _ _ hb h

Copy of a conditionally complete lattice with modified definitions

Informal description

Given a conditionally complete lattice structure on a type $\alpha$, this function creates a new conditionally complete lattice structure with the same operations and order relation, but potentially with different definitional properties. The new structure is provably equal to the original one, but may have better computational behavior. Specifically, it takes: - An existing conditionally complete lattice $c$ on $\alpha$ - A new order relation $le$ (with proof $eq\_le$ that it matches the original) - A new supremum operation $sup$ (with proof $eq\_sup$ that it matches the original join) - A new infimum operation $inf$ (with proof $eq\_inf$ that it matches the original meet) - A new set supremum operation $sSup$ (with proof $eq\_sSup$ that it matches the original) - A new set infimum operation $sInf$ (with proof $eq\_sInf$ that it matches the original) and returns a new conditionally complete lattice structure with these components, while preserving all lattice axioms and conditional completeness properties.