Equality without axioms

Stream: Type theory

[Mirek Olšák]

I was curious about this question (and thought it could be known). Assume, for some definitions a, b, we prove

theorem some_eq : a = b := ...

without assumptions, and even without the use of the standard three axioms (propext, Quot.sound, Classical.choice). Do then a, b must be definitionally equal? If not, what is a simple counterexample?

[Kyod]

In vanilla (intensional) Martin-Löf Type Theory (MLTT), a closed proof of propositional equality of two closed terms a and b indeed imply that a and b are definitionally equal (by canonicity).

This fail if you add functional extensionality (for instance in extensional MLTT), takinga := fun n : Nat => n and b := fun n : Nat => 0 + n that are equal by funext + induction but are not convertible.

I would expect Lean without axioms is quite close to intensional MLTT.

[Mirek Olšák]

But funext requires Quot.sound in Lean, right?

[Mirek Olšák]

I see, so judgemental equality without axioms likely implies definitional, thanks.

[Robin Arnez]

I think this statement is a consequence of "every closed term of an inductive type reduces to constructors" where the fact that the proof of some_eq reduces to Eq.refl _ implies that a = b holds definitionally. I'm pretty sure that new statement is true but Acc.rec might get in the way, not sure.

[Mirek Olšák]

Which is the "new statement"?

[Mirek Olšák]

I was thinking of transfinite constructions but they require building functions, so without functional extensionality, it is hard to get somewhere...

[Robin Arnez]

I mean "every closed term of an inductive type reduces to constructors" is probably true without axioms and that implies your statement

[Kevin Buzzard]

theorem foo (f g : Unit -> Empty) : f = g := by
  -- rfl -- fails
  cases (f .unit)

#print axioms foo -- 'foo' does not depend on any axioms

[Robin Arnez]

That has assumptions though

[Kevin Buzzard]

Oh apologies, I must have not understood the question :-(

[Mirek Olšák]

It is an interesting example anyway. It shows that opaque can introduce such examples too

opaque a : Unit := ()
opaque b : Unit := ()

example : a = b := by
  cases a
  cases b
  rfl

#print axioms some_eq -- 'some_eq' does not depend on any axioms

[Aaron Liu]

This one is also just rfl

[Aaron Liu]

because of unit-eta

[Mirek Olšák]

Doesn't work for me...

example : a = b := rfl -- Type mismatch
example : a = b := by rfl' -- Tactic `rfl` failed

[Mirek Olšák]

Although decide works...

[Aaron Liu]

opaque a : Unit := ()
opaque b : Unit := ()

example : a = b := Eq.refl ()

[Robin Arnez]

This is very strange

example (a b : Unit) : a = b := rfl

works but

opaque a : Unit := ()
opaque b : Unit := ()

example : a = b := rfl

doesn't and

example : a = b := Eq.refl ()

does?!

[Robin Arnez]

This seems like a bug

[Robin Arnez]

At least the kernel has no problem

import Lean

opaque a : Unit := ()
opaque b : Unit := ()

open Lean Elab Tactic
theorem th : a = b := by
  run_tac
    (← getMainGoal).assign (mkApp2 (.const ``rfl [1]) (mkConst ``Unit) (mkConst `a))

[Mirek Olšák]

By the way, I realized there is a cleaner way of using opaque to break definitional equality

structure EqPair where
  a : Nat
  b : Nat
  eq : a = b

opaque eqPair : EqPair := ⟨0, 0, rfl⟩

def a := eqPair.a
def b := eqPair.b

theorem some_eq : a = b := eqPair.eq -- not definitionally equal
#print axioms some_eq

it feels a bit cheap though... What was the idea with Acc.rec?

[Aaron Liu]

Lean's definitional equality algorithm doesn't respect substitution:

theorem foo : True ∧ True := ⟨trivial, trivial⟩

/--
error: Type mismatch
  Eq.refl 0
has type
  0 = 0
but is expected to have type
  And.rec (fun x x_1 => 0) foo = 0
-/
#guard_msgs in
example : foo.rec (fun _ _ => 0) = 0 :=
  Eq.refl 0

example : foo.rec (fun _ _ => 0) = 0 :=
  congrArg (fun p => (p.rec (fun _ _ => 0) : Nat)) (proof_irrel foo ⟨trivial, trivial⟩)

[Aaron Liu]

see also lean4#3213

[Mirek Olšák]

This one seems kernel defeq.

theorem foo : True ∧ True := ⟨trivial, trivial⟩
example : foo.rec (fun _ _ => 0) = 0 := by rfl'

[Robin Arnez]

... because the kernel has no trouble unfolding the theorem. If you use opaque, then the kernel fails too:

import Lean

opaque foo : True ∧ True := ⟨trivial, trivial⟩
example : foo.rec (fun _ _ => false) = false := by
  run_tac
    (← Lean.Elab.Tactic.getMainGoal).assign Lean.reflBoolFalse

[James E Hanson]

Mirek Olšák said:

What was the idea with Acc.rec?

Something like this?

def f (n : Nat) (p : Acc (· < ·) n) : Bool :=
  match p with
  | Acc.intro n h => match n with
                      | 0          => true
                      | Nat.succ m => f m (h m Nat.le.refl)

def inv' {α : Sort u} {R : α → α → Prop} (x : α) (h : Acc R x) (y : α) : R y x → Acc R y :=
  Acc.inv h

opaque p : Acc (· < ·) 1 := Nat.lt_wfRel.2.1 _

theorem eq_0 : f 1 p = f 1 (Acc.intro 1 (inv' 1 p)) := rfl
theorem eq_1 : f 1 (Acc.intro 1 (inv' 1 p)) = f 0 (inv' 1 p 0 Nat.le.refl) := rfl

theorem eq_2 : f 1 p = f 0 (inv' 1 p 0 Nat.le.refl) := Eq.trans eq_0 eq_1

/-- info: 'eq_2' does not depend on any axioms -/
#guard_msgs in
#print axioms eq_2

/--
error: Type mismatch
  rfl
has type
  ?m.14 = ?m.14
but is expected to have type
  f 1 p = f 0 ⋯
-/
#guard_msgs in
#check (rfl : f 1 p = f 0 (inv' 1 p 0 Nat.le.refl))

This is based on one of the two examples of the failure of transitivity of definitional equality in Mario's thesis. Mario helped me adapt it to Lean 4 a while ago. I feel like I was able to clean it up further at some point, but I can't find it right now.

This does need p to be opaque.

[James E Hanson]

Ah okay here's an example with no opaques:

def f (n : Nat) (p : Acc (· < ·) n) : Bool :=
  match p with
  | Acc.intro n h => match n with
                      | 0          => true
                      | Nat.succ m => f m (h m Nat.le.refl)

def inv' {α : Sort u} {R : α → α → Prop} (x : α) (h : Acc R x) (y : α) : R y x → Acc R y :=
  Acc.inv h

theorem eq_0 : (fun p ↦ f 1 p) = (fun p ↦ f 1 (Acc.intro 1 (inv' 1 p))) := rfl
theorem eq_1 : (fun p ↦ f 1 (Acc.intro 1 (inv' 1 p))) = (fun p ↦ f 0 (inv' 1 p 0 Nat.le.refl)) := rfl

theorem eq_2 : (fun p ↦ f 1 p) = (fun p ↦ f 0 (inv' 1 p 0 Nat.le.refl)) := Eq.trans eq_0 eq_1

/-- info: 'eq_2' does not depend on any axioms -/
#guard_msgs in
#print axioms eq_2

/--
error: Type mismatch
  rfl
has type
  ?m.24 = ?m.24
but is expected to have type
  (fun p => f 1) = ?m.19
-/
#guard_msgs in
#check (rfl : (fun p ↦ f 1) = (fun p ↦ f 0 (inv' 1 p 0 Nat.le.refl)))

[Kevin Buzzard]

(There's a typo f 1 -> f 1 pin the last line I think but I suspect that this doesn't change your point)

[Arthur Adjedj]

Robin Arnez said:

... because the kernel has no trouble unfolding the theorem. If you use opaque, then the kernel fails too:

import Lean

opaque foo : True ∧ True := ⟨trivial, trivial⟩
example : foo.rec (fun _ _ => false) = false := by
  run_tac
    (← Lean.Elab.Tactic.getMainGoal).assign Lean.reflBoolFalse

This is an instance of lean4#3213. As said previously, the fact that propositionally equal terms in an empty context are definitionally equal should hold in Lean’s meta-theory (as in, with a judgemental definitional equality, not the existing algorithm implemented), but in practice that’s not really the case for a few reasons as pointed out here, namely that the kernel has a few completeness issues making some "obvious" examples fail, that defeq is undecidable in general, and that lean adds a lot of axioms to the context in practice.

[Kevin Buzzard]

So James' example is exposing the difference between "definitionally equal in Lean's metatheory" and "provable by rfl".

[James E Hanson]

Here's a simpler example:

def X : Prop := Quot (fun _ _ ↦ True : True → True → Prop)

def a : X := Quot.mk _ trivial

def g : X → Nat := Quot.lift (fun _ ↦ 0) (fun _ _ _ ↦ rfl)

theorem eq_0 : (fun x ↦ g x) = (fun _ ↦ g a) := rfl

theorem eq_1 : (fun (_ : X) ↦ g a) = (fun _ ↦ 0) := rfl

theorem eq_2 : (fun x ↦ g x) = (fun _ ↦ 0) := Eq.trans eq_0 eq_1

/-- info: 'eq_2' does not depend on any axioms -/
#guard_msgs in
#print axioms eq_2

/--
error: Type mismatch
  rfl
has type
  ?m.9 = ?m.9
but is expected to have type
  (fun x => g x) = fun x => 0
-/
#guard_msgs in
#check (rfl : (fun x ↦ g x) = (fun _ ↦ 0))

[Arthur Adjedj]

Kevin Buzzard said:

So James' example is exposing the difference between "definitionally equal in Lean's metatheory" and "provable by rfl".

It looks like it, yes. Namely, since Acc can be eliminated to Type, its recursor can get stuck in places where another proof of accessibility (that would be defeq to the other thanks to proof-irrel) wouldn't, producing relevant terms that "get stuck" in places they shouldn't. Since Acc is not a structure, lean can't simply eta-expand the term in such cases to makes the recursor progress nonetheless. In systems without definitional proof-irrelevance like Rocq, eq_0 wouldn't work:

Require Import Coq.Arith.Le.

Fixpoint f (n : nat) (p : Acc (fun n1 n2 => n1 < n2) n) : bool :=
  match p with
    | Acc_intro _ h => match n as m return (n = m -> bool) with
      | O => fun _ => true
      | S m => fun h2 =>  f m (h m ltac:(rewrite h2; apply le_refl))
      end eq_refl
  end.

Fail Definition eq_0 : (fun p => f 1 p) = (fun p => f 1 (Acc_intro 1 (@Acc_inv _ _ 1 p))) := eq_refl.

Definition eq_1 : (fun p => f 1 (Acc_intro 1 (@Acc_inv _ _ 1 p))) = (fun p => f 0 (@Acc_inv _ _ 1 p 0 (le_refl _))) := eq_refl.

[Arthur Adjedj]

James E Hanson said:

Here's a simpler example:

def X : Prop := Quot (fun _ _ ↦ True : True → True → Prop)

def a : X := Quot.mk _ trivial

def g : X → Nat := Quot.lift (fun _ ↦ 0) (fun _ _ _ ↦ rfl)

theorem eq_0 : (fun x ↦ g x) = (fun _ ↦ g a) := rfl

theorem eq_1 : (fun (_ : X) ↦ g a) = (fun _ ↦ 0) := rfl

theorem eq_2 : (fun x ↦ g x) = (fun _ ↦ 0) := Eq.trans eq_0 eq_1

/-- info: 'eq_2' does not depend on any axioms -/
#guard_msgs in
#print axioms eq_2

/--
error: Type mismatch
  rfl
has type
  ?m.9 = ?m.9
but is expected to have type
  (fun x => g x) = fun x => 0
-/
#guard_msgs in
#check (rfl : (fun x ↦ g x) = (fun _ ↦ 0))

This is caused by the fact that you're allowed to quotient over Props, I don't see why it is like this, but I feel it shouldn't.

[James E Hanson]

Kevin Buzzard said:

So James' example is exposing the difference between "definitionally equal in Lean's metatheory" and "provable by rfl".

Lean's source code doesn't seem to agree with you about what the phrase 'definitional equality' means:

import Qq

open Qq

def X : Prop := Quot (fun _ _ ↦ True : True → True → Prop)

def g : X → Nat := Quot.lift (fun _ ↦ 0) (fun _ _ _ ↦ rfl)

/-- info: false -/
#guard_msgs in
#eval Lean.Meta.isDefEq q(fun x ↦ g x) q(fun _ ↦ 0 : X → Nat)

[François G. Dorais]

Could this quirk be about the old way of making IO work? It used to be that IO.RealWorld was just Unit. This was (correctly) changed in lean4#9631 but there may be leftover workarounds that are not useful anymore.

[James E Hanson]

François G. Dorais said:

Could this quirk be about the old way of making IO work? It used to be that IO.RealWorld was just Unit. This was (correctly) changed in lean4#9631 but there may be leftover workarounds that are not useful anymore.

Which quirk? The fact that those terms are not definitionally equal?

[Miyahara Kō]

Not Meta.isDefEq but Kernel.isDefEq:

import Qq

open Qq

def X : Prop := Quot (fun _ _ ↦ True : True → True → Prop)

def g : X → Nat := Quot.lift (fun _ ↦ 0) (fun _ _ _ ↦ rfl)

/- true -/
#eval do
  let a := Lean.Kernel.isDefEq (← Lean.getEnv) Lean.LocalContext.empty q(fun x ↦ g x) q(fun _ ↦ 0 : X → Nat)
  return a.toBool

[Robin Arnez]

Well, the kernel not producing an error doesn't mean that it thinks that they are defeq:

import Qq

open Qq

def X : Prop := Quot (fun _ _ ↦ True : True → True → Prop)

def g : X → Nat := Quot.lift (fun _ ↦ 0) (fun _ _ _ ↦ rfl)

/-- info: false -/
#guard_msgs in
#eval do
  let a := Lean.Kernel.isDefEq (← Lean.getEnv) Lean.LocalContext.empty q(fun x ↦ g x) q(fun _ ↦ 0 : X → Nat)
  match a with
  | .error e => Lean.throwKernelException e
  | .ok b => return b

[Miyahara Kō]

Oh, sorry:disappointed:.