Proving substitution property of successor over equality

Question

I'm trying to understand inductive types from chapter 7 of "theorem proving in lean".

I set myself a task of proving that successor of natural numbers has a substitution property over equality:

inductive natural : Type
| zero : natural
| succ : natural -> natural

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) := sorry

After some guesswork and fairly exhaustive search I was able to satisfy the compiler with a couple of possibilities:

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) :=
    eq.rec_on H (eq.refl (natural.succ a))
    --eq.rec_on H rfl
    --eq.subst H rfl
    --eq.subst H (eq.refl (natural.succ a))
    --congr_arg (λ (n : natural), (natural.succ n)) H

I don't understand how any of the proofs I've just given actually work.

1. What is the full definition of the eq (inductive) type? In VSCode I can see the type signature of eq as eq Π {α : Type} α → α → Prop, but I can't see individual (inductive) constructors (analogues of zero and succ from natural). The best I could find in source code doesn't look quite right.
2. Why is eq.subst happy to accept a proof of (natural.succ a) = (natural.succ a) to provide a proof of (natural.succ a) = (natural.succ b)?
3. What is higher order unification and how does it apply to this particular example?
4. What is the meaning of the error I get when I type #check (eq.rec_on H (eq.refl (natural.succ a))), which is [Lean] invalid 'eq.rec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known eq.rec_on : Π {α : Sort u} {a : α} {C : α → Sort l} {a_1 : α}, a = a_1 → C a → C a_1

Hobart

the definition of eq lives in github.com/leanprover/lean/blob/master/library/init/core.lean – Nuris

as to why it accepts the proof, afaik when you destruct the equality it causes a and b to be considered the same (after all they are the same argument of the constructor) so in the return type it gets replaced as well, yielding a target object with type (natural.succ a)=(natural.succ a) which you happen to have – Nuris

I don't even understand a single sentence of this question :-) Good luck though! – Deer

Answer 1

1. eq is defined to be

   inductive eq {α : Sort u} (a : α) : α → Prop
   | refl : eq a
   

   The idea is that any term is equal to itself, and the only way for two terms to be equal is for them to be the same term. This may feel like a bit of ITT magic. The beauty comes from the automatically generated recursor for this definition:

   eq.rec : Π {α : Sort u_2} {a : α} {C : α → Sort u_1}, C a → Π {a_1 : α}, a = a_1 → C a_1
   

   This is the substitution principle for equality. "If C holds of a, and a = a_1, then C holds of a_1." (There's a similar interpretation if C is type-valued instead of Prop-valued.)

2. eq.subst is taking a proof of a = b along with the proof of succ a = succ a. Note that eq.subst is basically a reformulation of eq.rec above. Suppose that the property C, parametrized over a variable x, is succ a = succ x. C holds for a by reflexivity, and since a = b, we have that C holds of b.

3. When you write eq.subst H rfl, Lean needs to figure out what the property (or "motive") C is supposed to be. This is an example of higher order unification: the unknown variable needs to unify with a lambda expression. There's a discussion of this in section 6.10 in https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf, and some general information at https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification.

4. You're asking Lean to substitute a = b into succ a = succ a, without telling it what you're trying to prove. You could be trying to prove succ b = succ b, or succ b = succ a, or even succ a = succ a (by substituting nowhere). Lean can't infer the motive C unless it has this information.

In general, doing substitutions "manually" (with eq.rec, subst, etc) is difficult, since higher order unification is finicky and expensive. You'll often find that it's better to use tactics like rw (rewrite):

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) := by rw H

If you want to be clever, you can make use of Lean's equation compiler, and the fact that the "only" proof of a=b is rfl:

lemma succ_over_equality : Π (a b : natural),
   a = b → (natural.succ a) = (natural.succ b)
| ._ _ rfl := rfl

Strophe

Thanks, that's a lot of detail! I'll slowly chew it over :) – Hobart