structure Law.MagmaLaw (α : Type u_1) : Type u_1

• lhs : FreeMagma α
• rhs : FreeMagma α

instance Law.instDecidableEqMagmaLaw : {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Law.MagmaLaw α)

Equations

• Law.instDecidableEqMagmaLaw = Law.decEqMagmaLaw✝

def Law.«term_≃_» : Lean.TrailingParserDescr

Equations

• Law.«term_≃_» = Lean.ParserDescr.trailingNode `Law.term_≃_ 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ ") (Lean.ParserDescr.cat `term 61))

@[reducible, inline]

abbrev Law.NatMagmaLaw : Type

Equations

• Law.NatMagmaLaw = Law.MagmaLaw ℕ

instance Law.instToJsonMagmaLaw {α : Type u_1} [Lean.ToJson α] : Lean.ToJson (Law.MagmaLaw α)

Equations

• Law.instToJsonMagmaLaw = { toJson := fun (x : Law.MagmaLaw α) => match x with | lhs ≃ rhs => Lean.Json.mkObj [("lhs", Lean.toJson lhs), ("rhs", Lean.toJson rhs)] }

@[reducible, inline]

abbrev Ctx (α : Type u_1) : Type u_1

Equations

• Ctx α = Set (Law.MagmaLaw α)

instance Ctx.Membership (α : Type u_1) : Membership (Law.MagmaLaw α) (Ctx α)

Equations

• Ctx.Membership α = { mem := Membership.mem }

instance instSingletonMagmaLawCtx {α : Type} : Singleton (Law.MagmaLaw α) (Ctx α)

Equations

• instSingletonMagmaLawCtx = { singleton := Set.singleton }

inductive derive {α : Type u} (Γ : Ctx α) : Law.MagmaLaw α → Type u

Definition for derivability

• Ax: {α : Type u} → {Γ : Ctx α} → {E : Law.MagmaLaw α} → E ∈ Γ → Γ ⊢ E
• Ref: {α : Type u} → {Γ : Ctx α} → {t : FreeMagma α} → Γ ⊢ t ≃ t
• Sym: {α : Type u} → {Γ : Ctx α} → {t u : FreeMagma α} → Γ ⊢ t ≃ u → Γ ⊢ u ≃ t
• Trans: {α : Type u} → {Γ : Ctx α} → {t u v : FreeMagma α} → Γ ⊢ t ≃ u → Γ ⊢ u ≃ v → Γ ⊢ t ≃ v
• Subst: {α : Type u} → {Γ : Ctx α} → {t u : FreeMagma α} → (σ : α → FreeMagma α) → Γ ⊢ t ≃ u → Γ ⊢ t ⬝ σ ≃ u ⬝ σ
• Cong: {α : Type u} → {Γ : Ctx α} → {t₁ t₂ u₁ u₂ : FreeMagma α} → Γ ⊢ t₁ ≃ t₂ → Γ ⊢ u₁ ≃ u₂ → Γ ⊢ t₁ ⋆ u₁ ≃ t₂ ⋆ u₂

inductive derive' {α : Type u} {β : Type v} (Γ : Ctx α) : Law.MagmaLaw β → Type (max u v)

Definition for derivability where Subst can only be applied to Ax

• SubstAx: {α : Type u} → {β : Type v} → {Γ : Ctx α} → {E : Law.MagmaLaw α} → E ∈ Γ → (σ : α → FreeMagma β) → Γ ⊢' E.lhs ⬝ σ ≃ E.rhs ⬝ σ
• Ref: {α : Type u} → {β : Type v} → {Γ : Ctx α} → {t : FreeMagma β} → Γ ⊢' t ≃ t
• Sym: {α : Type u} → {β : Type v} → {Γ : Ctx α} → {t u : FreeMagma β} → Γ ⊢' t ≃ u → Γ ⊢' u ≃ t
• Trans: {α : Type u} → {β : Type v} → {Γ : Ctx α} → {t u v : FreeMagma β} → Γ ⊢' t ≃ u → Γ ⊢' u ≃ v → Γ ⊢' t ≃ v
• Cong: {α : Type u} → {β : Type v} → {Γ : Ctx α} → {t₁ t₂ u₁ u₂ : FreeMagma β} → Γ ⊢' t₁ ≃ t₂ → Γ ⊢' u₁ ≃ u₂ → Γ ⊢' t₁ ⋆ u₁ ≃ t₂ ⋆ u₂

def derive_of_derive' {α : Type u_1} {Γ : Ctx α} {E : Law.MagmaLaw α} : Γ ⊢' E → Γ ⊢ E

Equations

• derive_of_derive' (derive'.SubstAx h σ) = derive.Subst σ (derive.Ax h)
• derive_of_derive' derive'.Ref = derive.Ref
• derive_of_derive' h.Sym = (derive_of_derive' h).Sym
• derive_of_derive' (htu.Trans huv) = (derive_of_derive' htu).Trans (derive_of_derive' huv)
• derive_of_derive' (h₁.Cong h₂) = (derive_of_derive' h₁).Cong (derive_of_derive' h₂)

def derive'_of_derive {α : Type u_1} {Γ : Ctx α} {E : Law.MagmaLaw α} (H : Γ ⊢ E) : Γ ⊢' E

Equations

• derive'_of_derive H = ⋯.mp (derive'_of_derive.go Lf H)

def derive'_of_derive.go {α : Type u_1} {Γ : Ctx α} {β : Type u_1} (σ : α → FreeMagma β) {E : Law.MagmaLaw α} : Γ ⊢ E → Γ ⊢' E.lhs ⬝ σ ≃ E.rhs ⬝ σ

Equations

• derive'_of_derive.go σ (derive.Ax h) = derive'.SubstAx h σ
• derive'_of_derive.go σ derive.Ref = derive'.Ref
• derive'_of_derive.go σ h.Sym = (derive'_of_derive.go σ h).Sym
• derive'_of_derive.go σ (htu.Trans huv) = (derive'_of_derive.go σ htu).Trans (derive'_of_derive.go σ huv)
• derive'_of_derive.go σ (derive.Subst σ_1 h) = ⋯.mpr (derive'_of_derive.go (FreeMagma.evalInMagma σ ∘ σ_1) h)
• derive'_of_derive.go σ (h₁.Cong h₂) = (derive'_of_derive.go σ h₁).Cong (derive'_of_derive.go σ h₂)

def satisfiesPhi {α : Type u_1} {G : Type u_2} [Magma G] (φ : α → G) (E : Law.MagmaLaw α) : Prop

Definitions of entailment

Equations

• satisfiesPhi φ E = (E.lhs ⬝ φ = E.rhs ⬝ φ)

def satisfies {α : Type u_1} (G : Type u_2) [Magma G] (E : Law.MagmaLaw α) : Prop

satisfies G E, or G ⊧ E, means that all evaluations of E in G are true.

Equations

• (G ⊧ E) = ∀ (φ : α → G), satisfiesPhi φ E

def satisfiesSet {α : Type u_1} (G : Type u_2) [Magma G] (Γ : Ctx α) : Prop

satisfiesSet G Γ, or G ⊧ Γ, means that G satisfies every element of Γ.

Equations

• (G ⊧ Γ) = ∀ E ∈ Γ, G ⊧ E

def models {α : Type u_1} {β : Type u_2} (Γ : Ctx α) (E : Law.MagmaLaw β) : Prop

models Γ E, or Γ ⊧ E, means that every magma G satisfying Γ also satisfies E.

Equations

• (Γ ⊧ E) = ∀ (G : Type) [inst : Magma G], G ⊧ Γ → G ⊧ E

Notation for derivability and entailment

def «term_⊧_» : Lean.TrailingParserDescr

satisfies G E, or G ⊧ E, means that all evaluations of E in G are true.

Equations

• «term_⊧_» = Lean.ParserDescr.trailingNode `term_⊧_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ ") (Lean.ParserDescr.cat `term 51))

def «term_⊧__1» : Lean.TrailingParserDescr

satisfiesSet G Γ, or G ⊧ Γ, means that G satisfies every element of Γ.

Equations

• «term_⊧__1» = Lean.ParserDescr.trailingNode `term_⊧__1 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ ") (Lean.ParserDescr.cat `term 51))

def «term_⊧__2» : Lean.TrailingParserDescr

models Γ E, or Γ ⊧ E, means that every magma G satisfying Γ also satisfies E.

Equations

• «term_⊧__2» = Lean.ParserDescr.trailingNode `term_⊧__2 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ ") (Lean.ParserDescr.cat `term 51))

def «term_⊢_» : Lean.TrailingParserDescr

Definition for derivability

Equations

• «term_⊢_» = Lean.ParserDescr.trailingNode `term_⊢_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 51))

def «term_⊢'_» : Lean.TrailingParserDescr

Definition for derivability where Subst can only be applied to Ax

Equations

• «term_⊢'_» = Lean.ParserDescr.trailingNode `term_⊢'_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢' ") (Lean.ParserDescr.cat `term 51))

def Law.MagmaLaw.symm {α : Type u_1} (l : Law.MagmaLaw α) : Law.MagmaLaw α

Equations

• l.symm = l.rhs ≃ l.lhs

@[simp]

theorem Law.MagmaLaw.symm_symm {α : Type u_1} (l : Law.MagmaLaw α) : l.symm.symm = l

def Law.MagmaLaw.map {α : Type u_1} {β : Type u_2} (f : α → β) : Law.MagmaLaw α → Law.MagmaLaw β

Equations

• Law.MagmaLaw.map f (lhs ≃ rhs) = (FreeMagma.fmapHom f) lhs ≃ (FreeMagma.fmapHom f) rhs

theorem Law.MagmaLaw.map_id {α : Type u_1} (m : Law.MagmaLaw α) : Law.MagmaLaw.map id m = m

theorem Law.MagmaLaw.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (m : Law.MagmaLaw α) : Law.MagmaLaw.map g (Law.MagmaLaw.map f m) = Law.MagmaLaw.map (g ∘ f) m

def Law.MagmaLaw.Mem {α : Type u_1} (a : α) (m : Law.MagmaLaw α) : Prop

Equations

• Law.MagmaLaw.Mem a m = (FreeMagma.Mem a m.lhs ∨ FreeMagma.Mem a m.rhs)

def Law.MagmaLaw.elems {α : Type u_1} [DecidableEq α] (m : Law.MagmaLaw α) : { l : List α // l.Nodup ∧ ∀ (a : α), a ∈ l ↔ Law.MagmaLaw.Mem a m }

Equations

• m.elems = match m.lhs.elems with | ⟨l, ⋯⟩ => match m.rhs.elems with | ⟨r, ⋯⟩ => ⟨l ∪ r, ⋯⟩

instance Law.MagmaLaw.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (a : α) (m : Law.MagmaLaw α) : Decidable (Law.MagmaLaw.Mem a m)

Equations

• Law.MagmaLaw.instDecidableMemOfDecidableEq a m = decidable_of_iff (a ∈ ↑m.elems) ⋯

def Law.MagmaLaw.finEquiv {α : Type u_1} [DecidableEq α] (m : Law.MagmaLaw α) : Fin (↑m.elems).length ≃ { a : α // Law.MagmaLaw.Mem a m }

Equations

• m.finEquiv = ⋯.mp (List.Nodup.getEquiv ↑m.elems ⋯)

def Law.MagmaLaw.pmap {α : Type u_1} {β : Type u_2} (m : Law.MagmaLaw α) : ((a : α) → Law.MagmaLaw.Mem a m → β) → Law.MagmaLaw β

Equations

• (lhs ≃ rhs).pmap f = (lhs.pmap fun (a : α) (h : FreeMagma.Mem a lhs) => f a ⋯) ≃ rhs.pmap fun (a : α) (h : FreeMagma.Mem a rhs) => f a ⋯

def Law.MagmaLaw.attach {α : Type u_1} (m : Law.MagmaLaw α) : Law.MagmaLaw { a : α // Law.MagmaLaw.Mem a m }

Equations

• m.attach = m.pmap Subtype.mk

theorem Law.MagmaLaw.attach_map_val {α : Type u_1} (m : Law.MagmaLaw α) : Law.MagmaLaw.map (fun (x : { a : α // Law.MagmaLaw.Mem a m }) => ↑x) m.attach = m

def Law.MagmaLaw.toFin {α : Type u_1} [DecidableEq α] (m : Law.MagmaLaw α) : Law.MagmaLaw (Fin (↑m.elems).length)

Equations

• m.toFin = Law.MagmaLaw.map (⇑m.finEquiv.symm) m.attach

def Law.MagmaLaw.toNat {α : Type u_1} [DecidableEq α] (m : Law.MagmaLaw α) : Law.MagmaLaw ℕ

Equations

• m.toNat = Law.MagmaLaw.map (fun (x : Fin (↑m.elems).length) => ↑x) m.toFin

theorem Law.MagmaLaw.pmap_eq_map {α : Type u_1} {β : Type u_2} (m : Law.MagmaLaw α) (f : (a : α) → Law.MagmaLaw.Mem a m → β) (g : α → β) (h : ∀ (a : α) (h : Law.MagmaLaw.Mem a m), f a h = g a) : m.pmap f = Law.MagmaLaw.map g m

theorem Law.satisfiesPhi_symm_law {α : Type u_1} {G : Type u_2} [Magma G] (φ : α → G) (E : Law.MagmaLaw α) (h : satisfiesPhi φ E) : satisfiesPhi φ E.symm

theorem Law.satisfiesPhi_map {α : Type u_1} {β : Type u_2} {G : Type u_3} [Magma G] {φ : β → G} {f : α → β} {E : Law.MagmaLaw α} : satisfiesPhi φ (Law.MagmaLaw.map f E) ↔ satisfiesPhi (φ ∘ f) E

theorem Law.satisfiesPhi_pmap {α : Type u_1} {β : Type u_2} {G : Type u_3} [Magma G] {φ : β → G} {ψ : α → G} (E : Law.MagmaLaw α) (f : (a : α) → Law.MagmaLaw.Mem a E → β) (H : ∀ (a : α) (h : Law.MagmaLaw.Mem a E), φ (f a h) = ψ a) : satisfiesPhi φ (E.pmap f) ↔ satisfiesPhi ψ E

theorem Law.satisfiesPhi_attach {α : Type u_1} {G : Type u_2} [Magma G] {φ : α → G} {E : Law.MagmaLaw α} : satisfiesPhi (fun (x : { a : α // Law.MagmaLaw.Mem a E }) => φ ↑x) E.attach ↔ satisfiesPhi φ E

theorem Law.satisfiesPhi_symm {α : Type u_1} {G : Type u_2} [Magma G] (φ : α → G) (w₁ : FreeMagma α) (w₂ : FreeMagma α) (h : satisfiesPhi φ (w₁ ≃ w₂)) : satisfiesPhi φ (w₂ ≃ w₁)

theorem Law.equiv_satisfiesPhi {α : Type u_1} {G : Type u_2} {H : Type u_3} [Magma G] [Magma H] {φ : α → G} (e : G ≃◇ H) {E : Law.MagmaLaw α} : satisfiesPhi (⇑e ∘ φ) E ↔ satisfiesPhi φ E

theorem Law.satisfies_symm_law {α : Type u_1} {G : Type u_2} [Magma G] {E : Law.MagmaLaw α} (h : G ⊧ E) : G ⊧ E.symm

theorem Law.satisfies_map {α : Type u_1} {β : Type u_2} {G : Type u_3} [Magma G] (f : α → β) {E : Law.MagmaLaw α} (h : G ⊧ E) : G ⊧ Law.MagmaLaw.map f E

theorem Law.satisfies_map_injective {α : Type u_1} {β : Type u_2} {G : Type u_3} [Magma G] (f : α → β) (hf : Function.Injective f) {E : Law.MagmaLaw α} : G ⊧ Law.MagmaLaw.map f E ↔ G ⊧ E

theorem Law.satisfies_map_equiv {α : Type u_1} {β : Type u_2} {G : Type u_3} [Magma G] (f : α ≃ β) {E : Law.MagmaLaw α} : G ⊧ Law.MagmaLaw.map (⇑f) E ↔ G ⊧ E

theorem Law.satisfies_attach {α : Type u_1} {G : Type u_2} [DecidableEq α] [Magma G] {E : Law.MagmaLaw α} : G ⊧ E.attach ↔ G ⊧ E

theorem Law.satisfies_toFin {α : Type u_1} {G : Type u_2} [DecidableEq α] [Magma G] {E : Law.MagmaLaw α} : G ⊧ E.toFin ↔ G ⊧ E

theorem Law.satisfies_toNat {α : Type u_1} {G : Type u_2} [DecidableEq α] [Magma G] {E : Law.MagmaLaw α} : G ⊧ E.toNat ↔ G ⊧ E

theorem Law.satisfies_symm {α : Type u_1} {G : Type u_2} [Magma G] {w₁ : FreeMagma α} {w₂ : FreeMagma α} (h : G ⊧ w₁ ≃ w₂) : G ⊧ w₂ ≃ w₁

theorem Law.satisfies_equiv {α : Type u_1} {G : Type u_2} {H : Type u_3} [Magma G] [Magma H] (e : G ≃◇ H) {E : Law.MagmaLaw α} : G ⊧ E ↔ H ⊧ E

theorem Law.satisfiesSet_symm {α : Type u_1} {G : Type u_2} [Magma G] {Γ : Ctx α} (h : G ⊧ Γ) : G ⊧ (fun (x : Law.MagmaLaw α) => x.symm) '' Γ

theorem Law.satisfiesSet_equiv {α : Type u_1} {G : Type u_2} {H : Type u_3} [Magma G] [Magma H] (e : G ≃◇ H) {Γ : Ctx α} : G ⊧ Γ ↔ H ⊧ Γ

theorem Law.satisfiesSet_toNat {α : Type u_1} {G : Type u_2} [DecidableEq α] [Magma G] {Γ : Ctx α} : G ⊧ (fun (x : Law.MagmaLaw α) => x.toNat) '' Γ ↔ G ⊧ Γ

theorem Law.models_symm_law {α : Type u_1} {Γ : Ctx α} {E : Law.MagmaLaw α} (h : Γ ⊧ E) : Γ ⊧ E.symm

theorem Law.models_symm {α : Type u_1} (Γ : Ctx α) (w₁ : FreeMagma α) (w₂ : FreeMagma α) (h : Γ ⊧ w₁ ≃ w₂) : Γ ⊧ w₂ ≃ w₁

theorem Law.models_toNat {α : Type u_1} {β : Type u_2} [DecidableEq β] {Γ : Ctx α} {E : Law.MagmaLaw β} : Γ ⊧ E.toNat ↔ Γ ⊧ E

theorem Law.toNat_models {α : Type u_1} {β : Type u_2} [DecidableEq α] {Γ : Ctx α} {E : Law.MagmaLaw β} : (fun (x : Law.MagmaLaw α) => x.toNat) '' Γ ⊧ E ↔ Γ ⊧ E

@[irreducible]

def Law.derive'_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {Γ : Ctx α} {E : Law.MagmaLaw β} : Γ ⊢' E → Γ ⊢' Law.MagmaLaw.map f E

Equations

• Law.derive'_map (derive'.SubstAx h σ) = ⋯.mpr (derive'.SubstAx h (⇑(FreeMagma.fmapHom f) ∘ σ))
• Law.derive'_map derive'.Ref = derive'.Ref
• Law.derive'_map h.Sym = (Law.derive'_map h).Sym
• Law.derive'_map (h1.Trans h2) = (Law.derive'_map h1).Trans (Law.derive'_map h2)
• Law.derive'_map (h1.Cong h2) = (Law.derive'_map h1).Cong (Law.derive'_map h2)

theorem Law.derive'_map_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} (hf : Function.Injective f) {Γ : Ctx α} {E : Law.MagmaLaw β} : Nonempty (Γ ⊢' Law.MagmaLaw.map f E) ↔ Nonempty (Γ ⊢' E)

def Law.derive'_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] {Γ : Ctx α} {E : Law.MagmaLaw β} (f : (a : β) → Law.MagmaLaw.Mem a E → γ) : Γ ⊢' E → Γ ⊢' E.pmap f

Equations

• Law.derive'_pmap f = ⋯.mpr Law.derive'_map

def Law.derive'_attach {α : Type u_1} {β : Type u_2} [DecidableEq β] {Γ : Ctx α} {E : Law.MagmaLaw β} : Γ ⊢' E → Γ ⊢' E.attach

Equations

• Law.derive'_attach = Law.derive'_pmap Subtype.mk

theorem Law.derive'_attach_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {Γ : Ctx α} {E : Law.MagmaLaw β} : Nonempty (Γ ⊢' E.attach) ↔ Nonempty (Γ ⊢' E)

theorem Law.derive'_toFin_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {Γ : Ctx α} {E : Law.MagmaLaw β} : Nonempty (Γ ⊢' E.toFin) ↔ Nonempty (Γ ⊢' E)

theorem Law.derive'_toNat_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {Γ : Ctx α} {E : Law.MagmaLaw β} : Nonempty (Γ ⊢' E.toNat) ↔ Nonempty (Γ ⊢' E)

theorem Law.satisfies_fin_satisfies_nat {n : ℕ} (G : Type u_1) [Magma G] (E : Law.MagmaLaw (Fin n)) : G ⊧ Law.MagmaLaw.map Fin.val E ↔ G ⊧ E