n : Nat defeq to n+1

Stream: lean4

[Kenny Lau]

Is it possible to make an expression n with elaborated type Nat such that n is defeq to n+1?

[Aaron Liu]

only in an inconsistent context

[Kenny Lau]

yes, in an inconsistent context

[Aaron Liu]

I think it's probably possible

[Robin Arnez]

Well,

example (n : Nat) : haveI : Add Nat := ⟨fun a _ => a⟩;
    n = n + 1 :=
  rfl

but I don't think the same is possible if you said n.succ

[Aaron Liu]

theorem k (h : False) : ∃ n, n = n + 1 :=
  ⟨@Acc.rec Nat (fun _ _ => False) (fun _ _ => Nat)
    (fun x hx ih => ih x h + 1) 0 h.elim, by
  conv => lhs; rhs; change Acc.intro 0 h.elim⟩

/--
info: fun h =>
  Exists.intro (Acc.rec (fun x hx ih => Nat.succ (ih x h)) (False.rec (fun x => Acc (fun x x => False) 0) h))
    (Eq.refl
      (Acc.rec (fun x hx ih => Nat.succ (ih x h))
          (False.rec (fun x => ∀ (y : Nat), False → Acc (fun x x => False) y) h 0 h)).succ)
-/
#guard_msgs in
#reduce (proofs := true) (types := true) k

[Aaron Liu]

for some reason rfl didn't work

[Aaron Liu]

but these are all defeq transformations

[Aaron Liu]

you can even see #reduce gives you Eq.refl

[Kyle Miller]

It might be a little more compelling if it weren't in an Exists.

However, I'm getting a kernel type error with this:

noncomputable def bad_n (h : False) : Nat :=
  @Acc.rec Nat (fun _ _ => False) (fun _ _ => Nat)
    (fun x _ ih => ih x h.elim + 1) 0 (Acc.intro 0 h.elim)

example (h : False) :
    bad_n h = bad_n h + 1 := by
  delta bad_n
  conv => lhs; rhs; change Acc.intro 0 h.elim

[Aaron Liu]

theorem k (h : False) :
  @Acc.rec Nat (fun _ _ => False) (fun _ _ => Nat)
    (fun x hx ih => ih x h + 1) 0 h.elim =
  @Acc.rec Nat (fun _ _ => False) (fun _ _ => Nat)
    (fun x hx ih => ih x h + 1) 0 h.elim + 1 := by
  conv => lhs; rhs; change Acc.intro 0 h.elim

/--
info: fun h =>
  Eq.refl
    (Acc.rec (fun x hx ih => Nat.succ (ih x h))
        (False.rec (fun x => ∀ (y : Nat), False → Acc (fun x x => False) y) h 0 h)).succ
-/
#guard_msgs in
#reduce (proofs := true) (types := true) k

[Aaron Liu]

you have to be careful around the kernel here

[Aaron Liu]

since it can sometimes just decide not to iota reduce your Acc.rec

[Kenny Lau]

i mean, acc.rec is well-known to be evil

[Parth Shastri]

noncomputable def inf : Acc (fun _ _ => True) () → Nat := Acc.rec fun _ _ ih => ih () ⟨⟩ + 1

example : inf h = inf h + 1 := @id (inf h = inf ⟨_, fun _ _ => h⟩) rfl
-- example : inf h = inf h + 1 := rfl -- fails

-- https://arxiv.org/abs/1911.08174
def F : Prop := ∀ p, (p → p) → p
def δ (z : F) : F := fun p η => η (z (F → F) id z p η)
def ω (h : ∀ p q : Prop, p = q) : F := fun p _ => h (F → F) p ▸ δ
def Ω (h : ∀ p q : Prop, p = q) : Acc (fun _ _ => True) () := δ (ω h) (Acc (fun _ _ => True) ()) (⟨_, fun _ _ => ·⟩)

example : inf (Ω h) = inf (Ω h) + 1 := rfl

[Aaron Liu]

oh you can make it run for a while

set_option maxRecDepth 10000 in
example : inf (Ω h) = inf (Ω h) + 1000 := rfl

[Aaron Liu]

oh you can make it run forever

set_option maxRecDepth 0 in
example {n : Nat} : inf (Ω h) = inf (Ω h) + n := rfl

[Kenny Lau]

wow, someone dug into the arXivs

[Aaron Liu]

I think I remember seeing something like this before

[Aaron Liu]

oh I found it: #general > Normalization fails in lean @ 💬

[Wuyang]

Interesting exploration of how inconsistent contexts and Acc.rec tricks can yield n = n + 1 in Lean. You may try searching on LeanFinder: www.leanfinder.org.

[Wuyang]

@leanfinder Lean proofs and examples showing n = n + 1 via inconsistent contexts, Acc.rec, and normalization quirks.

[leanfinder]

Here’s what I found:

• lemma rec_add_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) (n : ℕ) : Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n) := rfl "For any type family $C : \mathbb{N} \to \text{Sort}^*$ and given:

• A base case $h_0 : C(0)$

• An inductive step function $h : \forall n, C(n) \to C(n+1)$

The recursion principle Nat.rec evaluated at $n+1$ satisfies $\text{Nat.rec}\ h_0\ h\ (n+1) = h(n, \text{Nat.rec}\ h_0\ h\ n)$. This means that the value at $n+1$ is obtained by applying the step function $h$ to $n$ and the recursively computed value at $n$. " (score: 0.683)

• theorem rec_eq_recC : @Acc.rec = @Acc.recC := by funext α r motive intro a t induction t with | intro x h ih => dsimp only [recC_intro intro h] congr; funext y hr; exact ih _ hr "The theorem states that the recursive function \texttt{Acc.rec} is equal to \texttt{Acc.recC}. This is shown by using function extensionality and induction on the accessibility predicate. Specifically, for a type $\alpha$, a relation $r$, and a motive, the functions are equal for any accessible element $a$ and its proof $t$. The proof proceeds by induction on $t$, showing that the two functions produce the same result by congruence and function extensionality." (score: 0.683)

• theorem ndrec_eq_ndrecC : @Acc.ndrec = @Acc.ndrecC := by funext α r motive intro a t rw [Acc.ndrec, rec_eq_recC, Acc.ndrecC] "The recursion principle Acc.ndrec is equal to the computable version Acc.ndrecC for accessible elements." (score: 0.679)

• theorem Nat.rec_add_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) (n : ℕ) : Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n) := rfl "For any type family $C : \mathbb{N} \to \text{Sort}^*$, given a base case $h_0 : C(0)$ and a step function $h : \forall n, C(n) \to C(n+1)$, the recursive computation of $C$ at $n+1$ satisfies $\text{rec}(h_0, h, n+1) = h(n, \text{rec}(h_0, h, n))$." (score: 0.678)

• @[simp] lemma rec_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : Nat.rec (motive := C) h0 h 1 = h 0 h0 := rfl "For any type family $C : \mathbb{N} \to \text{Sort}^*$ and given:

• A base case $h_0 : C(0)$

• An inductive step function $h : \forall n, C(n) \to C(n+1)$

The recursion principle Nat.rec evaluated at one satisfies $\text{Nat.rec}\ h_0\ h\ 1 = h(0, h_0)$. This means that starting from the base case $h_0$, applying the inductive step function once results in $h(0, h_0)$. " (score: 0.677)

• theorem ndrecOn_eq_ndrecOnC : @Acc.ndrecOn = @Acc.ndrecOnC := by funext α r motive intro a t rw [Acc.ndrecOn, rec_eq_recC, Acc.ndrecOnC] "The recursion principle Acc.ndrecOn is equal to the computable version Acc.ndrecOnC. This equality holds for any type $\alpha$, relation $r$, and motive." (score: 0.675)

• lemma leRecOn_self {C : ℕ → Sort*} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) : (leRecOn n.le_refl next x : C n) = x := leRec_self _ _ "For any type family $C : \mathbb{N} \to \text{Sort}^*$, natural number $n$, and step function $\text{next} : \forall k, C(k) \to C(k+1)$, applying the recursion principle with initial value $x \in C(n)$ when $n \leq n$ yields:
  $\text{leRecOn}(n \leq n, \text{next}, x) = x$
  where the result is of type $C(n)$. This establishes the base case for recursion." (score: 0.673)

• lemma not_succ_lt_self : ¬ succ n < n := Nat.not_lt_of_ge n.le_succ "For any natural number $n$, the successor of $n$ is not less than $n$, i.e., $\neg (n + 1 < n)$. This follows from the fact that $n \leq n + 1$." (score: 0.672)

• theorem Nat.rec_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : Nat.rec (motive := C) h0 h 1 = h 0 h0 := rfl "For any type family $C : \mathbb{N} \to \text{Sort}^*$, base case $h_0 : C(0)$, and inductive step function $h : \forall n, C(n) \to C(n+1)$, the recursion principle applied to $1$ satisfies $\text{Nat.rec}\ h_0\ h\ 1 = h\ 0\ h_0$." (score: 0.671)
• theorem PFunctor.M.agree'_refl {n : ℕ} (x : M F) : Agree' n x x := by induction' n with _ n_ih generalizing x <;> induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl intros apply n_ih "For any natural number $n$ and any element $x$ of the M-type $\mathsf{M}\,F$ (the final coalgebra of a polynomial functor $F$), the depth-$n$ agreement relation $\text{Agree'}\,n\,x\,x$ holds. That is, any tree is identical to itself up to any depth $n$." (score: 0.669)