Deep Recursion

Stream: new members

[Saroj N]

I am not sure why this code says there is an issue of deep recursion:
theorem ok {c : char} :
c = '∧' → c ≠ '∨' :=
begin finish end
When I replace '∧' and '∨' with 'a' and 'b', there is no error though. Thanks!

[Kevin Buzzard]

It's because the unicode character for '∧' will correspond to a number like 37 gazillion, and finish is not adapted to dealing with large numbers.

[Eric Wieser]

>>> ord('∧')
8743

[Eric Wieser]

Which amazingly, has 37 as a divisor, making "a gazillion" exactly 236

[Kevin Lacker]

<never mind>

[Adam Topaz]

Where's the gazillion emoji?

[Eric Wieser]

well, chr(236) is ì...

[Kevin Buzzard]

I don't know much python but I'm a bit skeptical about the claim that 37*236=8743

[Eric Wieser]

It turns out that the human brain isn't reliable as a clipboard. I typed 8732 by accident

[Kevin Buzzard]

unless we're talking about nat.div in which case I'm totally on board

[Adam Topaz]

It's 236.29729....

[Kevin Lacker]

this works though: lemma foo (c : ℕ) : c = 88888 → c ≠ 99999 := by finish

[Kevin Buzzard]

maybe the issue is that char does something crazy, this has come up before

[Kevin Buzzard]

chars are somehow unusable in Lean 3

[Kevin Buzzard]

The problem is something to do with this code in core:

@[reducible] def is_valid_char (n : nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)

lemma is_valid_char_range_1 (n : nat) (h : n < 0xd800) : is_valid_char n :=
or.inl h

lemma is_valid_char_range_2 (n : nat) (h₁ : 0xdfff < n) (h₂ : n < 0x110000) : is_valid_char n :=
or.inr ⟨h₁, h₂⟩

/-- The `char` type represents an unicode scalar value.
    See http://www.unicode.org/glossary/#unicode_scalar_value). -/
structure char :=
(val : nat) (valid : is_valid_char val)

Checking that you're in the right range is really painful.

[Mario Carneiro]

You just need the right lemmas and to use the tool for the job:

theorem char.of_nat_inj {a b} (h₁ : is_valid_char a) (h₂ : is_valid_char b) :
  char.of_nat a = char.of_nat b → a = b :=
by simp [char.of_nat, *]; intro e; exact char.veq_of_eq e

theorem ok {c : char} : c = '∧' → c ≠ '∨' :=
begin
  rintro rfl,
  refine mt (char.of_nat_inj _ _) _; norm_num [is_valid_char]
end

[Bjørn Kjos-Hanssen]

Here's a ridiculous solution: replace ∧ and ∨ by ASCII characters . and v and do

import tactic.basic

#eval 'v'.val
#eval '.'.val

lemma ok {c : char} : c = '.' →  c ≠ 'v' :=
  λ dot: c = '.', λ vee: c = 'v',
    have 118 = 46, from calc 118 = 'v'.val : refl ('v'.val)
                             ... =   c.val : by rw vee
                             ... = '.'.val : by rw dot
                             ... =      46 : refl ('.'.val),
    have same_num: 72 = 0, from by tidy,

    nat.succ_ne_zero 71 (eq.trans (refl (nat.succ 71)) same_num)