Less than on natural numbers is an accessible relation

Stream: lean4

[Mukesh Tiwari]

Hi everyone,

When I am pattern matching on an element of type Acc R n , Lean typechecker says, "invalid alternative name Acc.intro". How can I do this? (In Coq, I would use inversion ih)

import Init.WF
import Init.Data.Nat


theorem nat_lt : ∀ n : Nat,
  Acc (fun (x y : Nat) => x < y) n := by
  intros n
  induction n with
  | zero =>
    focus
      apply Acc.intro
      intros y Hy
      cases Hy
  | succ n ih =>
      focus
        apply Acc.intro
        intros y Hy
        apply Acc.intro
        intros z Hz
        cases ih with
        | Acc.intro _ R => _  (* Typechecker complains:  invalid alternative name 'Acc.intro'  *)

[Marcus Rossel]

I have no clue why this doesn't work, but if you want a workaround until someone else can explain the problem, try this:

cases ih
case succ.h.h.intro R =>
  ...

[Horațiu Cheval]

You simply use introto refer to the case.

cases ih with
| intro _ R => _

[Horațiu Cheval]

I guess in general the tag name doesn't include the namespace. Just as in your example if you replace succ with Nat.succ it will be an invalid tag

[Marcus Rossel]

So when using cases/induction with with, the cases are identified by tags? I always thought with means that we're back to "normal" pattern matching.

[Horațiu Cheval]

And if the type you're casing on has just one constructor as with Acc you can even put an underscore in place of the name, which I think is nice: cases ih with | _ _ R => instead of cases ih with | intro _ R => .

[Marcus Rossel]

Also, when you only have a single constructor you can perform destructuring with have ⟨_, R⟩ := ih.

[Mukesh Tiwari]

Horațiu Cheval said:

cases ih with | _ _ R => .

Interesting, I thought I tried it and it did not work in the past, but now that you answered my question, it's working :). Thank you both @Horațiu Cheval @Marcus Rossel .

Since, we are here how do you search for relevant lemmas and tactics? Right now, I need to discharge:

Hy : y < Nat.succ n
z : Nat
Hz : z < y
⊢ z < n

[Horațiu Cheval]

Marcus Rossel said:

So when using cases/induction with with, the cases are identified by tags? I always thought with means that we're back to "normal" pattern matching.

The first example works, but the second doesn't, with an invalid tag error

example : Nat → Nat := fun n => match n with
| Nat.succ n => sorry
| Nat.zero => sorry

example : Nat → Nat := by
  intros n
  cases n with
  | Nat.succ n => sorry
  | Nat.zero => sorry

[Marcus Rossel]

Mukesh Tiwari said:

Since, we are here how do you search for relevant lemmas and tactics? Right now, I need to discharge:

Hy : y < Nat.succ n
z : Nat
Hz : z < y
⊢ z < n

There used to be a library_search tactic which hasn't been ported to Lean 4 yet (IIRC).
These days I tend to use the Lean 3 web editor to then use library_search :sweat_smile:

[Alex Keizer]

library_search has been ported as part of mathlib4 (https://github.com/leanprover-community/mathlib4).

[Ruben Van de Velde]

docs4#lt_of_lt_of_le seems like a first step

[Ruben Van de Velde]

And docs4#Nat.lt_succ_iff

[Mukesh Tiwari]

Thanks everyone!

import Init.WF
import Init.Data.Nat


theorem nat_lt : ∀ n : Nat,
  Acc (fun (x y : Nat) => x < y) n := by
  intros n
  induction n with
  | zero =>
    focus
      apply Acc.intro
      intros y Hy
      cases Hy
  | succ n ih =>
      focus
        apply Acc.intro
        intros y Hy
        apply Acc.intro
        intros z Hz
        cases ih with
        | _ _ R =>
          apply R
          have Ht := Nat.le_of_lt_succ Hy
          have Hw := Nat.lt_of_lt_of_le Hz Ht
          exact Hw
````

[Arthur Paulino]

Btw, no need to import content from Init. It's already imported by default