Sugar-free Semigroup

Stream: new members

[Paul Wilson]

I'm trying to understand the core of LEAN by proving a simple theorem without additional language features. Specifically, I want to understand how structure unpacks into the core type theory.

Here's some code using struture:

structure Semigroup (α : Type u) :=
  (mul : α → α → α)
  (mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c))

#check Eq.symm

theorem unique_identity {α : Type u} (s : Semigroup α) (eL eR : α)
  (hL : ∀ a : α, s.mul eL a = a)
  (hR : ∀ a : α, s.mul a eR = a) :
  eR = eL :=
  let x : eR = s.mul eL eR := Eq.symm (hL eR)
  let y : s.mul eL eR = eL := hR eL
  Eq.trans x y

I would like to understand what is actually going on when I prove unique_identity. As far as my understanding goes:

1. structure is desugared somehow into a term of the core type theory
2. The theorem unique_identity is similarly transformed into a term $t$
3. $t$ is type-checked

And if (3) succeeds, the theorem is proven. But I don't understand what the term $t$ actually looks like. What does the structure Semigroup desugar to? What about the unique_identity theorem?

[Mario Carneiro]

A structure declaration is not desugared to the declaration of a term in the same way as def or theorem. Instead, it is desugared to an instance of the inductive command

[Mario Carneiro]

The theorem unique_identity is however the declaration of a plain term, and you can see what it looks like using #print but it's pretty much exactly what you wrote

[Paul Wilson]

Isn't the inductive machinery also sugar for something?

[Paul Wilson]

I would have guessed that semigroup is church encoded (or something like that), but I don't quite see how that would look

[Paul Wilson]

Mario Carneiro said:

The theorem unique_identity is however the declaration of a plain term, and you can see what it looks like using #print but it's pretty much exactly what you wrote

The problem with this is that I don't see how to actually do anything with this term without knowing how to "unpack" the (s : Semigroup α) and its associated expressions s.mul.

[Mario Carneiro]

Paul Wilson said:

Isn't the inductive machinery also sugar for something?

No, it's a primitive of the type system

[Mario Carneiro]

Paul Wilson said:

I would have guessed that semigroup is church encoded (or something like that), but I don't quite see how that would look

Not at all. The primitive objects you get out of an inductive type are:

• The type
• The constructor(s)
• The recursor
• also: a computation rule relating the recursor applied to constructors

A structure is sugar for an inductive with one constructor and one argument to that constructor for each field of the constructor, and the field projections are automatically defined using the recursor.

[Mario Carneiro]

You can't "unpack" Semigroup α because it is one of the primitives produced above (the type). You can unpack s.mul, at least in principle, by looking at #print Semigroup.mul and you will see it has a definition, but it will be somewhat confusing because actually lean also has primitive projections which are a form of "built-in sugar" for an application of the recursor, for performance reasons.

[Mario Carneiro]

but roughly speaking, the desugaring of your Semigroup definition is:

inductive Semigroup (α : Type u) where
  | mk
    (mul : α → α → α)
    (mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c))
    : Semigroup α

-- defines:
#print Semigroup
#print Semigroup.mk
#print Semigroup.rec
-- and a computation rule:
example {α : Type u} {motive : Semigroup α → Sort v}
    (F : (mul : α → α → α) →
        (mul_assoc : ∀ (a b c : α), mul (mul a b) c = mul a (mul b c)) → motive (Semigroup.mk mul mul_assoc))
    (mul : α → α → α)
    (mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c)) :
    @Semigroup.rec α motive F (Semigroup.mk mul mul_assoc) = F mul mul_assoc := rfl

noncomputable def Semigroup.mul {α} (s : Semigroup α) : α → α → α :=
  Semigroup.rec (fun mul _ => mul) s

theorem Semigroup.mul_assoc {α} (s : Semigroup α) :
    ∀ a b c : α, s.mul (s.mul a b) c = s.mul a (s.mul b c) :=
  Semigroup.rec (fun _ mul_assoc => mul_assoc) s

[Paul Wilson]

Thanks, this is really helpful, although surprising! I usually think about languages as having a fixed set of primitive operations; is it fair to say that with this core-language-plus-inductive-types, you extend this set of primitives? Happy to receive a pointer to some reading which explains this too.

[Mario Carneiro]

That is one way to think about it. Another way is that inductive is a "primitive schema", which is to say an algorithm for spitting out new objects which have to satisfy some rules. You can prove the soundness of the whole schema, which makes it qualitatively different from axiom which is also a way of extending the system but not in a way which is generally sound, so you have to keep track of precisely which axioms are added. def is also a primitive schema in the same sense: it allows you to add objects to the system in a way which can be proved sound once-and-for-all

[Mario Carneiro]

You may find my paper #leantt helpful for understanding how the rules can be defined formally

[Paul Wilson]

Thanks, this helps - the paper seems to be exactly what I'm looking for too! I notice there are slides as well- is there a recording of a talk by any chance?

[Mario Carneiro]

https://youtu.be/3sKrSNhSxik