theorem on ranges

Stream: Program verification

[Wax-byte]

Hi I am rather new to using Lean. Just wondering, why is below not automatically proven by aesop?

theorem sub_Range {x e: ℕ} {h1: x ∈ [:e]}: x ∈ [:e+1] := by aesop

[Wax-byte]

and here in the playground

[Daniel Weber]

There seems to be a lot of missing API for docs#Std.Range which causes this

[Wax-byte]

Thanks for the clarification. Trying to do more of the proof by hand. Good for learning.

[Wax-byte]

Managed to get the proof working, but unsure why I needed tauto instead of aesop at the end

theorem sub_Range {x e: Nat} {h: x ∈ [:e]}: x ∈ [:e+1] := by
  apply And.intro
  . aesop
  . simp
    . cases h
      tauto

[Kevin Buzzard]

The main application of tauto itself does nothing (in your case) but tauto calls solve_by_elim after running, which solves the goal.

[Bulhwi Cha]

Daniel Weber said:

There seems to be a lot of missing API for docs#Std.Range which causes this

Perhaps it'll be added to Lean's standard library in the future.

Kim Morrison said:

There will be more news coming about this later, and when a design document is available we will post it, but it is possible there will be a radical overhaul of the String library (indeed, even the definition of String), so I would hesitate to encourage significant work on String at the moment as it may become obsolete (even to the point of not being able to meaningfully migrate results).

[Bulhwi Cha]

Kim Morrison said:

Unfortunately overhauling String by the FRO has fallen back to medium priority, and in particular no one is actively working on it now.

I'm afraid Lean's still not ready to provide enough APIs for strings.