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.
def
bounded_order.copy
{α : Type u}
{h h' : has_le α}
(c : bounded_order α)
(top : α)
(eq_top : top = bounded_order.top)
(bot : α)
(eq_bot : bot = bounded_order.bot)
(le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A function to create a provable equal copy of a bounded order with possibly different definitional equalities.
def
lattice.copy
{α : Type u}
(c : lattice α)
(le : α → α → Prop)
(eq_le : le = lattice.le)
(sup : α → α → α)
(eq_sup : sup = lattice.sup)
(inf : α → α → α)
(eq_inf : inf = lattice.inf) :
lattice α
A function to create a provable equal copy of a lattice with possibly different definitional equalities.
Equations
- c.copy le eq_le sup eq_sup inf eq_inf = {sup := sup, le := le, lt := semilattice_sup.lt._default le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := inf, inf_le_left := _, inf_le_right := _, le_inf := _}
def
distrib_lattice.copy
{α : Type u}
(c : distrib_lattice α)
(le : α → α → Prop)
(eq_le : le = distrib_lattice.le)
(sup : α → α → α)
(eq_sup : sup = distrib_lattice.sup)
(inf : α → α → α)
(eq_inf : inf = distrib_lattice.inf) :
A function to create a provable equal copy of a distributive lattice with possibly different definitional equalities.
Equations
- c.copy le eq_le sup eq_sup inf eq_inf = {sup := sup, le := le, lt := lattice.lt._default le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := inf, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
def
complete_lattice.copy
{α : Type u}
(c : complete_lattice α)
(le : α → α → Prop)
(eq_le : le = complete_lattice.le)
(top : α)
(eq_top : top = complete_lattice.top)
(bot : α)
(eq_bot : bot = complete_lattice.bot)
(sup : α → α → α)
(eq_sup : sup = complete_lattice.sup)
(inf : α → α → α)
(eq_inf : inf = complete_lattice.inf)
(Sup : set α → α)
(eq_Sup : Sup = complete_lattice.Sup)
(Inf : set α → α)
(eq_Inf : Inf = complete_lattice.Inf) :
A function to create a provable equal copy of a complete lattice with possibly different definitional equalities.
Equations
- c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf = {sup := sup, le := le, lt := lattice.lt ((complete_lattice.to_lattice α).copy le eq_le sup eq_sup inf eq_inf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup, le_Sup := _, Sup_le := _, Inf := Inf, Inf_le := _, le_Inf := _, top := top, bot := bot, le_top := _, bot_le := _}
def
frame.copy
{α : Type u}
(c : order.frame α)
(le : α → α → Prop)
(eq_le : le = order.frame.le)
(top : α)
(eq_top : top = order.frame.top)
(bot : α)
(eq_bot : bot = order.frame.bot)
(sup : α → α → α)
(eq_sup : sup = order.frame.sup)
(inf : α → α → α)
(eq_inf : inf = order.frame.inf)
(Sup : set α → α)
(eq_Sup : Sup = order.frame.Sup)
(Inf : set α → α)
(eq_Inf : Inf = order.frame.Inf) :
A function to create a provable equal copy of a frame with possibly different definitional equalities.
Equations
- frame.copy c le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf = {sup := sup, le := le, lt := complete_lattice.lt ((order.frame.to_complete_lattice α).copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup, le_Sup := _, Sup_le := _, Inf := Inf, Inf_le := _, le_Inf := _, top := top, bot := bot, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _}
def
coframe.copy
{α : Type u}
(c : order.coframe α)
(le : α → α → Prop)
(eq_le : le = order.coframe.le)
(top : α)
(eq_top : top = order.coframe.top)
(bot : α)
(eq_bot : bot = order.coframe.bot)
(sup : α → α → α)
(eq_sup : sup = order.coframe.sup)
(inf : α → α → α)
(eq_inf : inf = order.coframe.inf)
(Sup : set α → α)
(eq_Sup : Sup = order.coframe.Sup)
(Inf : set α → α)
(eq_Inf : Inf = order.coframe.Inf) :
A function to create a provable equal copy of a coframe with possibly different definitional equalities.
Equations
- coframe.copy c le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf = {sup := sup, le := le, lt := complete_lattice.lt ((order.coframe.to_complete_lattice α).copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup, le_Sup := _, Sup_le := _, Inf := Inf, Inf_le := _, le_Inf := _, top := top, bot := bot, le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}
def
complete_distrib_lattice.copy
{α : Type u}
(c : complete_distrib_lattice α)
(le : α → α → Prop)
(eq_le : le = complete_distrib_lattice.le)
(top : α)
(eq_top : top = complete_distrib_lattice.top)
(bot : α)
(eq_bot : bot = complete_distrib_lattice.bot)
(sup : α → α → α)
(eq_sup : sup = complete_distrib_lattice.sup)
(inf : α → α → α)
(eq_inf : inf = complete_distrib_lattice.inf)
(Sup : set α → α)
(eq_Sup : Sup = complete_distrib_lattice.Sup)
(Inf : set α → α)
(eq_Inf : Inf = complete_distrib_lattice.Inf) :
A function to create a provable equal copy of a complete distributive lattice with possibly different definitional equalities.
Equations
- c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf = {sup := order.frame.sup (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), le := order.frame.le (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), lt := order.frame.lt (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := order.frame.inf (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := order.frame.Sup (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), le_Sup := _, Sup_le := _, Inf := order.frame.Inf (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), Inf_le := _, le_Inf := _, top := order.frame.top (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), bot := order.frame.bot (frame.copy (complete_distrib_lattice.to_frame α) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf), le_top := _, bot_le := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}
def
conditionally_complete_lattice.copy
{α : Type u}
(c : conditionally_complete_lattice α)
(le : α → α → Prop)
(eq_le : le = conditionally_complete_lattice.le)
(sup : α → α → α)
(eq_sup : sup = conditionally_complete_lattice.sup)
(inf : α → α → α)
(eq_inf : inf = conditionally_complete_lattice.inf)
(Sup : set α → α)
(eq_Sup : Sup = conditionally_complete_lattice.Sup)
(Inf : set α → α)
(eq_Inf : Inf = conditionally_complete_lattice.Inf) :
A function to create a provable equal copy of a conditionally complete lattice with possibly different definitional equalities.
Equations
- c.copy le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf = {sup := sup, le := le, lt := lattice.lt._default le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := Sup, Inf := Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}