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_lattice.copy
{α : Type u}
(c : bounded_lattice α)
(le : α → α → Prop)
(eq_le : le = bounded_lattice.le)
(top : α)
(eq_top : top = bounded_lattice.top)
(bot : α)
(eq_bot : bot = bounded_lattice.bot)
(sup : α → α → α)
(eq_sup : sup = bounded_lattice.sup)
(inf : α → α → α) :
inf = bounded_lattice.inf → bounded_lattice α
A function to create a provable equal copy of a bounded 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 := 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 := _, top := top, le_top := _, bot := bot, bot_le := _}
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 : α → α → α) :
inf = distrib_lattice.inf → distrib_lattice α
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 α → α) :
Inf = complete_lattice.Inf → complete_lattice α
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 := bounded_lattice.lt ((complete_lattice.to_bounded_lattice α).copy le eq_le top eq_top bot eq_bot 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 := _, top := top, le_top := _, bot := bot, bot_le := _, Sup := Sup, Inf := Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_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 α → α) :
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 := sup, le := le, lt := complete_lattice.lt ((complete_distrib_lattice.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 := _, top := top, le_top := _, bot := bot, bot_le := _, Sup := Sup, Inf := Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _, infi_sup_le_sup_Inf := _, inf_Sup_le_supr_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 α → α) :
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 := _}