deep recursion with append

Stream: new members

[Jason Orendorff]

never mind why I want to know the result of gluing all these strings together, but

#reduce "~" ++ ("∃" ++ "a" ++ ":" ++ ("S" ++ "a" ++ "=" ++ "0"))

this gives deep recursion was detected at 'replace' (potential solution: increase stack space in your system) locally (and in the browser it just seems to run forever)

Even just #reduce "~" ++ ("∃") doesn't finish in the browser for me.

[Reid Barton]

I think #reduce with characters is super slow. Would #eval work for you?

[Reid Barton]

A character is something like a natural number plus a proof that it lies in the range of valid Unicode characters

[ROCKY KAMEN-RUBIO]

I've run into surprisingly different behavior with #eval and #reduce. @Jalex Stark I remember you saying you got a noticeable speedup when you allocated more processing power to Lean on your drive . Could this be a useful simple way to test that?

[Bryan Gin-ge Chen]

#reduce and #eval are completely different. See the discussion here: https://leanprover.github.io/reference/expressions.html#computation

[Jalex Stark]

i don't see a reason why #reduce should be memory-limited. things that spawn a bunch of parallel processes might be faster with more memory, if memory was limiting the number of processes running in parallel

[Jason Orendorff]

#eval is great, but now what I want is to establish that "~" ++ ("∃" ++ "a" ++ ":" ++ ("S" ++ "a" ++ "=" ++ "0")) = "~∃a:Sa=0". Apparently refl is like reduce, not like eval

[Mario Carneiro]

simp

[Bryan Gin-ge Chen]

simp doesn't work most likely because we don't have many lemmas about string.

[Jason Orendorff]

I'm trying to write those lemmas myself now ... I don't know that I can do it without access to string_imp.

[Bryan Gin-ge Chen]

Oh, actually this works:

import data.string.basic

example : "~" ++ ("∃" ++ "a" ++ ":" ++ ("S" ++ "a" ++ "=" ++ "0")) = "~∃a:Sa=0" := begin
  apply string.to_list_inj.1,
  change ['~','∃','a',':','S','a','=','0'] = _,
  refl
end

[Jason Orendorff]

I don't have string.to_list_inj

[Bryan Gin-ge Chen]

What version of Lean / mathlib are you using? The lemma was added about 2 years ago: https://github.com/leanprover-community/mathlib/commit/a30b7c773db17cf7d1b551ba0f24645079296628#diff-6ab0314160d20014ac5f2e53531740b1R57

[Reid Barton]

Clearly we need a norm_str tactic

[Jason Orendorff]

facepalm I was working in a scratch .lean file with no mathlib installed, silly mistake

[Bryan Gin-ge Chen]

If you don't want all of mathlib, you can also just copy and paste the theorem into your file:

namespace string
theorem to_list_inj : ∀ {s₁ s₂}, to_list s₁ = to_list s₂ ↔ s₁ = s₂
| ⟨s₁⟩ ⟨s₂⟩ := ⟨congr_arg _, congr_arg _⟩
end string

[Jason Orendorff]

Why doesn't unfold string.to_list manage to unfold "~".to_list?

[Mario Carneiro]

string has a private implementation, which is somewhat unusual for a lean data structure