Overriding notation

Stream: new members

[Richard Copley]

Is it possible to override ∧, ∨, ¬ and ≤? If so, where did I go wrong?

class BooleanAlgebra (α : Type _) where
  or : α → α → α
  and : α → α → α
  not : α → α
  or_comm : ∀ {p q : α}, or p q = or q p
  or_assoc : ∀ {p q r : α}, or p (or q r) = or (or p q) r
  or_absorb : ∀ {p q : α}, or p (and p q) = p
  or_distrib : ∀ {p q r : α}, or p (and q r) = and (or p q) (or p r)
  or_bot : ∀ {p q : α}, or p (and q (not q)) = p
  and_comm : ∀ {p q : α}, and p q = and q p
  and_assoc : ∀ {p q r : α}, and p (and q r) = and (and p q) r
  and_absorb : ∀ {p q : α}, and p (or p q) = p
  and_distrib : ∀ {p q r : α}, and p (or q r) = or (and p q) (and p r)
  and_top : ∀ {p q : α}, and p (or q (not q)) = p

open BooleanAlgebra

infixr:135 " ∧ "  => BooleanAlgebra.and
infixr:130 " ∨ "  => BooleanAlgebra.or
notation:max "¬" p:140 => BooleanAlgebra.not p

theorem or_idem {α : Type _} [BooleanAlgebra α] {p : α} : p = p ∨ p := calc
  p = p ∨ (p ∧ p)                   := or_absorb.symm
  _ = (p ∨ p) ∧ (p ∨ p)             := or_distrib
  _ = ((p ∨ p) ∧ p) ∨ ((p ∨ p) ∧ p) := and_distrib
  _ = (p ∧ (p ∨ p)) ∨ (p ∧ (p ∨ p)) := by rw [and_comm]
  _ = p ∨ p                         := by rw [and_absorb]

-- Fails:
--   38:80:
--   application type mismatch
--     Or p
--   argument
--     p
--   has type
--     α : Type ?u.23329
--   but is expected to have type
--     Prop : Type
--def BooleanAlgebra.entails {α : Type _} [BooleanAlgebra α] (p q : α) : Prop := p ∨ q = q
--                                                                               ~

-- OK
def BooleanAlgebra.entails {α : Type _} [BooleanAlgebra α] (p q : α) : Prop := q = p ∨ q

infix:150 " ≤ " => BooleanAlgebra.entails

-- OK
theorem entails.rfl {α : Type _} [BooleanAlgebra α] {p : α} : p ≤ p := or_idem

-- Fails:
--   64:77:
--   application type mismatch
--     q ∧ q ≤ p
--   argument
--     q ≤ p
--   has type
--     Prop : Type
--   but is expected to have type
--     α : Type ?u.30939
--   64:69:
--   failed to synthesize instance
--     LE α
--theorem entails.antisymm {α : Type _} [BooleanAlgebra α] {p q : α} : p ≤ q ∧ q ≤ p → p = q := by sorry
--                                                                     ~       ~~~~~

[Jason Rute]

Here is the definition in mathlib. docs#GeneralizedBooleanAlgebra. If you look at the source and follow back the classes this extends you can see how type classes like docs#LE can be used for overloading.

[Richard Copley]

That would be sensible! Except...
The reason I want to do it in this unusual way is that I'm following a particular text (Logic As Algebra by Halmos and Givant). I want to use Lean as a guardrail/handholder.

[Jason Rute]

You can still follow the same override notation with type class pattern, no?

[Richard Copley]

Thanks! I'll try. (But if you will indulge a poor beginner: I don't know what you mean.)

[Richard Copley]

sorry! I can't get a handle on what it is you're suggesting.

I could work in a BooleanRing (or algebra), with the more usual notation and "multiplication is idempotent" as an axiom. I imagine if I skip a few lemmas, I will be able to join the text soon enough.

But the Y part of the XY? If I really wanted to override the notation, could I?

[Jason Rute]

I’m not sure about overriding notation the way you are. I’m sure someone here can give you a better answer on that. As for using the existing type classes (or reimplementing them), I give a simpler example in this PA answer.

[Richard Copley]

Seems like I should look to overload, not override. (Tomorrow.)

[Eric Wieser]

Note that docs#BooleanAlgebra in mathlib uses slightly different notation in order to avoid having to overload the And/Or notation

[Eric Wieser]

Your entails failure was just an operator precedence issue:

def BooleanAlgebra.entails {α : Type _} [BooleanAlgebra α] (p q : α) : Prop := (p ∨ q) = q

[Eric Wieser]

As is your last failure:

theorem entails.antisymm {α : Type _} [BooleanAlgebra α] {p q : α} : (p ≤ q) ∧ (q ≤ p) → p = q := by sorry