Is `Nat.noConfusionType` in Lean 4 Circular Reasoning When P

Stream: Is there code for X?

[Lingwei Peng (彭灵伟)]

I noticed that in Lean 4, when proving 0 ≠ n.succ, Nat.noConfusionType is used. It is defined as follows:

def Nat.noConfusionType.{u} : Sort u → Nat → Nat → Sort u :=
  fun P v1 v2 => Nat.casesOn v1 (Nat.casesOn v2 (P → P) fun n => P) fun n => Nat.casesOn v2 P fun n_1 => (n = n_1 → P) → P

My understanding is that this expression is equivalent to:

if v1 = 0 then
  if v2 = 0 then P → P else P
else
  if v2 = 0 then P else (n = v2 → P) → P

This essentially requires first defining when n = 0 and when n ≠ 0. So, is using Nat.noConfusionType to prove 0 ≠ n.succ a form of circular reasoning?

[Kevin Buzzard]

No it's definitely not circular reasoning -- that is not allowed in lean. The axiom of recursion says that you can define a function on natural numbers by saying what to do with zero and what to do with successors, and you're just noticing that this axiom is enough to imply noConfusion.

[suhr]

colorlessboy said:

My understanding is that this expression is equivalent to:

if v1 = 0 then
  if v2 = 0 then P → P else P
else
  if v2 = 0 then P else (n = v2 → P) → P

This essentially requires first defining when n = 0 and when n ≠ 0. So, is using Nat.noConfusionType to prove 0 ≠ n.succ a form of circular reasoning?

It is not equivalent: casesOn uses the recursor of Nat, for which Lean has a built-in computation rule, while if ... then ... else works in a much more roundabout way: under the hood it's application of the ite function which uses an instance of the Decidable inferred for the given proposition.

[suhr]

Here's an example (open it in Lean 4 playground):

def foo : Sort u → Nat → Nat → Sort u :=
  fun P v1 v2 =>
    if v1 = 0 then
      if v2 = 0 then P → P else P
    else
      if v2 = 0 then P else (v1 = v2 → P) → P

set_option pp.notation false in
  #print foo

You can click on ite to see the implicit arguments.

[Lingwei Peng (彭灵伟)]

Thanks. Do you mean Decidable n = 0?

[suhr]

Decidable (v1 = 0), but yeah. By the way, you can find the instance with #synth ∀n: Nat, Decidable (n = 0).

[suhr]

By the way, here are computation rules for Nat.rec:

Nat.rec z s (Nat.zero)   ≡ z
Nat.rec z s (Nat.succ n) ≡ s n (Nat.rec z s n)

Which also imply that Nat.rec has the following type:

Nat.rec.{u}: {motive: Nat → Sort u} →
  motive Nat.zero →
  ((n: Nat) → motive n → motive n.succ) →
  ∀(t: Nat),  motive t

In the same way one can deduce the computation rules and the type of the recursor for any other inductive type.

[suhr]

Works for type families too. For example, computation rules for Nat.le.rec:

Nat.le.rec r s (@Nat.le.refl n)     ≡ r
Nat.le.rec r s (@Nat.le.step n m h) ≡ s m h (Nat.le.rec r s h)

And the type of the recursor:

Nat.le.rec: ∀{n: Nat} {motive: ∀m: Nat, n ≤ m → Prop},
  motive n Nat.le.refl →
  (∀{m: Nat} (h: n ≤ m), motive m h → motive m.succ (Nat.le.step h)) →
  ∀{m: Nat} (h: n ≤ m), motive m h

[Lingwei Peng (彭灵伟)]

I find this chain of reasoning quite complex: Decidable n = 0 → instDecidableEqNat → Nat.decEq → Nat.eq_of_beq_eq_true, and I think it is related to some implicit kernel behaviors. I understand the recursor, but I don’t fully understand why noConfusion can be derived from it. It seems more like a language rule for inductive types rather than a theorem (such as injectivity and disjointness of constructors).

[Kevin Buzzard]

The recursor is a much more powerful tool than it initially appears. Peano's original axioms included things like zero != n.succ and injectivity of succ but they can all be derived from the recursor

[suhr]

colorlessboy said:

It seems more like a language rule for inductive types rather than a theorem (such as injectivity and disjointness of constructors).

Remember that the Lean core is not a logic but a theory of constructions. Propositions and proofs are merely special cases of mathematical constructions.

[suhr]

Here's an example for booleans with some annotations:

#print Bool.noConfusionType

#reduce Bool.noConfusionType False false false  -- False → False
#reduce Bool.noConfusionType False false true   -- False
#reduce Bool.noConfusionType False true false   -- False
#reduce Bool.noConfusionType False true true    -- False → False

def bool_d {P: Sort u}(b: Bool): Bool.noConfusionType P b b :=
  b.casesOn
    ((λp ↦ p) : Bool.noConfusionType P false false)
    ((λp ↦ p) : Bool.noConfusionType P true true)

example (h: false = true): False :=
  -- Bool.noConfusionType False false true ≡ False
  show Bool.noConfusionType False false true from
    Eq.subst
      (motive := λt ↦ Bool.noConfusionType _ false t)
      h
      (bool_d false : Bool.noConfusionType False false false)

Computationally equal types are the same... and that's the key for noConfusion.

[Lingwei Peng (彭灵伟)]

Computationally equal types are the same. This is clear. But I cannot understand the other part: why computationally different types are considered to be different.

I think the second part is more like an implicit axiom implemented in the kernel, rather than a theorem. But I am not sure.

The Lean 4 kernel has many implicit axioms that are not explicitly coded. For example:

example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
  rfl

This rfl works because the kernel automatically simplifies Quot.lift f f_respects (Quot.mk mod7Rel a) into f a, which looks like a provable theorem but is actually an axiom.

[suhr]

It's again not an axiom but a computation rule. These are indeed are documented rather poorly in Lean.

[suhr]

The Lean Reference merely mentions the reduction rule for inductive types: https://lean-lang.org/doc/reference/latest//The-Type-System/Inductive-Types/#iota-reduction. And I don't see a reduction rule for quotients in the reference.

[Sebastian Ullrich]

"Reduction" is mentioned many times in the quotient chapter

[suhr]

Oh, it's mentioned en passant:

https://lean-lang.org/doc/reference/latest//The-Type-System/Quotients/#Quot___sound

In addition to the above constants, Lean's kernel contains a reduction rule for Quot.lift that causes it to reduce when used with Quot.mk, analogous to ι-reduction for inductive types. Given a relation r over α, a function f from α to β, and a proof resp that f respects r, the term Quot.lift f resp (Quot.mk r x) is definitionally equal to f x.

[suhr]

By the way, Coq documentation is more straightforward: it lists all reduction rules in a separate section, and gives an example for ι-reduction while discussing inductive types.

[Lingwei Peng (彭灵伟)]

Yes, it is quite complex for beginners like me. When I eagerly look into which axioms are used after a theorem, I often encounter things I can’t fully grasp. The result is usually some kernel behavior hidden in the corners of the documentation.

Thanks for the Coq documentation.

I think noConfusion might be more complicated than the reduction example above. I’ll need more time to understand it.

[suhr]

Nat.noConfusion and Bool.noConfusion are very similar (you can see this by #print Bool.noConfusion and #print Nat.noConfusion) so if you understand how the example for Bool works you will be able to do the same for Nat.

Thanks for the Coq documentation.

Keep in mind that theories of Coq and Lean are slightly different: for example, Lean uses recursors while Coq uses fixpoints.

[Lingwei Peng (彭灵伟)]

suhr said:

Nat.noConfusion and Bool.noConfusion are very similar (you can see this by #print Bool.noConfusion and #print Nat.noConfusion) so if you understand how the example for Bool works you will be able to do the same for Nat.

Thanks for the Coq documentation.

Keep in mind that theories of Coq and Lean are slightly different: for example, Lean uses recursors while Coq uses fixpoints.

Thanks a lot! The Bool example is very clear.