Is defeq transitive?

Stream: lean4

[Daniel Weber]

Is defeqness transitive (without metavariables)? That is, if a = b is true by rfl and b = c is true by rfl, will a = c always be true by rfl?

[Markus Himmel]

No, see Section 3.1.1 of #leantt.

[Daniel Weber]

What am I doing wrong here?

import Mathlib

variable (n : ℕ) (P : ℕ → Prop) [DecidablePred P]

def f : Acc (· > ·) n → Bool := Acc.rec (fun n _ g ↦ if P n then g (n + 1) (lt_add_one n) else true)

example : f 0 P a = f 0 P (Acc.intro 0 (fun _ ↦ Acc.inv a)) := rfl

example : f 0 P (Acc.intro 0 (fun _ ↦ Acc.inv a)) = f 1 P (Acc.inv a (lt_add_one 0)) := rfl -- this should work

example : f 0 P a = f 1 P (Acc.inv a (lt_add_one 0)) := rfl

[Mauricio Collares]

Daniel Weber said:

Is defeqness transitive (without metavariables)? That is, if a = b is true by rfl and b = c is true by rfl, will a = c always be true by rfl?

This was Mario's example in https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/What.20is.20the.20subject.20reduction.20debate.3F/near/274338966:

import Batteries.WF

variable {A : Type} {R : A → A → Prop} (x : A) (h : Acc R x)

def my_rec : ∀ x : A, Acc R x → Nat := @Acc.rec A R (λ _ _ => Nat) (λ _ _ _ => 1)
def inv {x : A} (h : Acc R x) : Acc R x := Acc.intro x (λ y h' => Acc.inv h h')
example : inv h = h := rfl -- ok
#reduce my_rec x (inv h) -- 1
#reduce my_rec x h -- acc.rec _ h

-- failure of transitivity
#check (rfl : my_rec x (inv h) = 1) -- ok
#check (rfl : inv h = h) -- ok
#check (rfl : my_rec x (inv h) = my_rec x h) -- ok
#check (rfl : my_rec x h = 1) -- fail

-- failure of SR:
#check @id (my_rec x h = 1) (@id (my_rec x (inv h) = 1) rfl) -- ok
#check @id (my_rec x h = 1) (@id (1 = 1) rfl) -- fail

[Daniel Weber]

Thanks

[Johan Commelin]

Did you rediscover this on your own? That's actually pretty cool, I think

[Mario Carneiro]

I think Daniel's first post is a transcription of the counterexample in sec 3.1.1 of #leantt

[Johan Commelin]

aah, ok

[Mario Carneiro]

the counterexample doesn't translate precisely to lean because it's actually an undecidability proof for the idealized typing judgment, not a non-transitivity proof for the real typing judgment

[Mario Carneiro]

The example Mauricio linked is the latter

[Arthur Adjedj]

Note that the current implementation of Lean's type theory contains other examples of failure of transitivity for defeq, related mainly to (the lack of) certain eta-expansions in certain situations (see i.e lean4#3213 and lean4#2258)

[Kevin Buzzard]

When I first learnt about this phenomenon I was kind of horrified, but it never ever seems to get in the way of the mathematics I do in mathlib and FLT so I now view it as a pathology which doesn't affect me, much like the way I view the incompleteness theorem (it might be true in theory but it doesn't seem to have any practical consequences in the Langlands program).

[Mario Carneiro]

to be fair, the langlands program is incomplete