Zulip Chat Archive

Stream: new members

Topic: deep recursion with append


view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 17 2020 at 16:28):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 17 2020 at 20:38):

simp

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jason Orendorff (Jun 17 2020 at 20:51):

I don't have string.to_list_inj

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 17 2020 at 20:58):

Clearly we need a norm_str tactic

view this post on Zulip Jason Orendorff (Jun 17 2020 at 20:58):

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

view this post on Zulip 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

view this post on Zulip Jason Orendorff (Jun 17 2020 at 21:20):

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

view this post on Zulip 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