Ergonomic or elimination

Stream: new members

[Ioannis Konstantoulas]

In order to simplify my workflow, I have the following theorem:

theorem or_of_left_id {p q : Prop} (or_pred: p ∨ q) (proof : p → q) : q :=
  Or.elim or_pred
    proof
    id

which automates id in one of the two branches of an or. I use it like this for example:

theorem pos_of_nz {n : Nat} (nz : n ≠ 0) : n > 0 :=
  or_of_left_id (Nat.eq_zero_or_pos n) (nz . |>.elim)

Is there an internal way in Lean to do this without a custom theorem? Or some syntax/notation that is easier and clearer to read?

[Kevin Buzzard]

pos_of_nz is proved in Std as docs#Nat.pos_of_ne_zero . It uses docs#Or.resolve_left. If you don't want to use std or mathlib then I guess you have to reprove them yourself.

[Ioannis Konstantoulas]

Kevin Buzzard said:

pos_of_nz is proved in Std as docs#Nat.pos_of_ne_zero . It uses docs#Or.resolve_left. If you don't want to use std or mathlib then I guess you have to reprove them yourself.

Or.resolve_left is what I was thinking of; but what I am wondering is if there is some standard syntax trick to write this more cleanly. For example, (with my non-existent syntax writing skills),

theorem or_of_left_id {p q : Prop} (or_pred: p ∨ q) (proof : p → q) : q :=
  Or.elim or_pred
    proof
    id

notation orp " ∨⋆ " pr => or_of_left_id orp pr

theorem pos_of_nz {n : Nat} (nz : n ≠ 0) : n > 0 :=
  (Nat.eq_zero_or_pos _) ∨⋆ (nz . |>.elim)

but something more elegant, perhaps.

[Ruben Van de Velde]

by tauto might work

[Ioannis Konstantoulas]

This leads to a somewhat unrelated question (perhaps deserving its own topic?): how can I see all the unicode symbols I can enter in Lean through VS Code, and the character sequence (e.q. \l for lambda) to print them?

[Alex J. Best]

The full list is here https://github.com/leanprover/vscode-lean4/blob/02a6d4917f658bc1ee98933a809c0369e9827a0d/vscode-lean4/src/abbreviation/abbreviations.json, but it can often be easier to paste the symbol you want into vscode and hover over it with your mouse and it will show the character sequence for it

[Alex J. Best]

If you press ctrl-shift-p in vscode and type "Lean 4: show all abbreviations" you can look at this list in vscode too