Iota-reduction and rfl issues

Stream: Type theory

[Arthur Adjedj]

Hi, while trying to break Lean, I found some inconsistencies with regards to the reduction of Prop-recursors. I have come to understand that such recursors simply don't reduce, in order to avoid an undecidable type-checking due to i.e the elimination of Acc. In practice however, the reduction of such recursors seems inconsistent ? See, in the following code:

def tautext {A B : Prop} (a : A) (b : B)
: A = B := propext (Iff.intro (λ _ => b) (λ _ => a))
def True' : Prop := ∀ A : Prop, A → A
def delta : True' → True' := λ z : True' => z _  id z
def omega : True' := λ _ a => cast (tautext id a) delta
def Omega : True' := delta omega --non-terminating term

def f (h : True ∧ True) : Nat := And.rec (motive := fun _ => Nat) (fun _ _ => 1) h
example : f ⟨.intro,.intro⟩ = 1 := rfl --recursor reduces here

#reduce f (Omega _ ⟨.intro,.intro⟩) --infinite recursion, maxRecDepth error

--despite that, a type mismatch error still appears instead of an infinite loop during defeq
example : f (Omega _ ⟨.intro,.intro⟩) = 1 := rfl

Here,And.rec reduces, and even leads to an infinite reduction thanks to Omega. However, when checking for definitional equality, the term doesn't get reduced.

Weirdly enough, if I add an implicit binder to True''s forall, reduction doesn't trigger on f (@Omega _ ⟨.intro,.intro⟩) , as one would expect:

def tautext {A B : Prop} (a : A) (b : B)
: A = B := propext (Iff.intro (λ _ => b) (λ _ => a))
def True' : Prop := ∀ {A : Prop}, A → A -- A is now implicit, only change made here
def delta : True' → True' := λ z : True' => z  id z
def omega : True' := λ a => cast (tautext id a) delta
def Omega : True' := delta omega --non-terminating term

def f (h : True ∧ True) : Nat := And.rec (motive := fun _ => Nat) (fun _ _ => 1) h

#reduce f (Omega ⟨.intro,.intro⟩) -- And.rec (fun x x => 1) (_ : True ∧ True)

Any idea what's going on here ?

[Arthur Adjedj]

Nevermind, it turns out that #reduce tries to do a full normal form, thus reducing Omega _ ⟨.intro,.intro⟩ even though the recursor doesn't reduce, though i'm still confused as to why f ⟨.intro,.intro⟩ = 1 := rflwould type-check here.

[Mario Carneiro]

I don't think anything other than #reduce reduces proofs. And.rec f h reduces to f h.1 h.2 by eta for structures IIRC

[Arthur Adjedj]

As discussed here, eta for structures isn't triggered during the reduction of recursors that are in Prop, so I believe this isn't supposed to type-check, even though it does:

example : f ⟨.intro,.intro⟩ = 1 := rfl --works

Furthermore, I have found what I believe to be an inconsistency between the kernel reduction in the kernel and the elaborator. It's nothing dangerous, but it shows (to me) that reduction with Prop-recursors can have inconsistent behaviours:

import Lean

open Lean Meta Elab Term Command

def whnfKernel (e : Expr) : MetaM Expr := do
    let env ← getEnv
    let lctx ← getLCtx
    match Kernel.whnf env lctx e with
      | .ok e => return e
      | .error e => throwKernelException e

elab "#whnf" t:term : command => runTermElabM fun _xs => do
 let t ← whnf (← elabTermAndSynthesize t none)
 logInfo t

elab "#whnf_kernel" t:term : command => runTermElabM fun _xs => do
 let t ← whnfKernel (← elabTermAndSynthesize t none)
 logInfo t


def tautext {A B : Prop} (a : A) (b : B)
: A = B := propext (Iff.intro (λ _ => b) (λ _ => a))
def True' : Prop := ∀ A : Prop, A → A
def delta : True' → True' := λ z : True' => z _  id z
def omega : True' := λ _ a => cast (tautext id a) delta
def Omega : True' := delta omega --non-terminating term


def f (h : True ∧ True) : Nat := And.rec (motive := fun _ => Nat) (fun _ _ => 1) h
example : f (id ⟨.intro,.intro⟩) = 1 := rfl --recursor reduces here

#whnf f (id ⟨.intro,.intro⟩)
#whnf f (Omega (True ∧ True) ⟨.intro,.intro⟩) --doesn't reduce
#whnf_kernel f (Omega (True ∧ True) ⟨.intro,.intro⟩) --infinite loop

Knowing that the kernel's isDefEq may be called instead of the elaborator's in certain cases for proofs by reflection, perhaps it would be best to have consistent results between the two.

[Arthur Adjedj]

Because of this, conversion is still undecidable, at least in the kernel, and I believe it would be possible to make this leak out in the elaborator thanks to proofs by reflection:

elab "#is_def_eq_kernel" t₁:term "#" t₂:term "#" : command => runTermElabM fun _xs => do
 let t₁ ← elabTermAndSynthesize t₁ none
 let t₂ ← elabTermAndSynthesize t₂ none
 let isDefEq ← isDefEqKernel t₁ t₂
 logInfo s!"{isDefEq}"

#is_def_eq_kernel (f (Omega (True ∧ True) ⟨.intro,.intro⟩)) # 1 # --infinite loop

[Arthur Adjedj]

Here is Lean looping indefinitely at the elaborator level:

def tautext {A B : Prop} (a : A) (b : B)
: A = B := propext (Iff.intro (λ _ => b) (λ _ => a))
def True' : Prop := ∀ A : Prop, A → A
def delta : True' → True' := λ z : True' => z _  id z
def omega : True' := λ _ a => cast (tautext id a) delta
def Omega : True' := delta omega --non-terminating term

def f (h : True ∧ True) : Nat := And.rec (motive := fun _ => Nat) (fun _ _ => 1) h
example : f (id ⟨.intro,.intro⟩) = 1 := rfl --recursor reduces here

example : (f (Omega _ ⟨.intro,.intro⟩)) = 1 := by rfl --infinite loop

This happens because the rfl tactic uses the kernel's isDefEq when checking the conversion of two closed terms with no metavariables (link)

[Wojciech Nawrocki]

Here is another one in Lean 3: lean#91