## Stream: new members

### Topic: deep recursion with append

#### Jason Orendorff (Jun 17 2020 at 16:26):

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 (Jun 17 2020 at 16:28):

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

#### Reid Barton (Jun 17 2020 at 16:29):

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

#### ROCKY KAMEN-RUBIO (Jun 17 2020 at 17:47):

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 (Jun 17 2020 at 17:56):

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

#### Jalex Stark (Jun 17 2020 at 18:04):

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 (Jun 17 2020 at 20:37):

#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 (Jun 17 2020 at 20:38):

simp

#### Bryan Gin-ge Chen (Jun 17 2020 at 20:41):

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

#### Jason Orendorff (Jun 17 2020 at 20:49):

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 (Jun 17 2020 at 20:49):

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 (Jun 17 2020 at 20:51):

I don't have string.to_list_inj

#### Bryan Gin-ge Chen (Jun 17 2020 at 20:57):

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 (Jun 17 2020 at 20:58):

Clearly we need a norm_str tactic

#### Jason Orendorff (Jun 17 2020 at 20:58):

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

#### Bryan Gin-ge Chen (Jun 17 2020 at 20:59):

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 (Jun 17 2020 at 21:20):

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

#### Mario Carneiro (Jun 17 2020 at 21:40):

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

Last updated: May 08 2021 at 18:17 UTC