rewrite le.antisymm from Lean 2

Stream: general

[Utensil Song]

I'm trying to rewrite the proof example in the Lean 2 paper into Lean 3 while keeping its main structure which demonstrated different proof paradigms.

The original is here and I manage to get the following #mwe

import tactic

open int

theorem le.antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b :=
begin
assume a b : ℤ, assume (H₁ : a ≤ b) (H₂ : b ≤ a),
obtain ⟨n, Hn⟩ := int.le.dest H₁,
obtain ⟨m, Hm⟩ := int.le.dest H₂,
have H₃ : a + of_nat (n + m) = a + 0, from
  calc
    a + of_nat (n + m) = a + (of_nat n + m) : by refl
      ... = a + n + m                       : by simp only [add_assoc, of_nat_eq_coe]
      ... = b + m                           : by rw Hn
      ... = a                               : by rw Hm
      ... = a + 0                           : by rw add_zero,
have H₄ : of_nat (n + m) = of_nat 0, from add_left_cancel H₃,
have H₅ : n + m = 0,                 from of_nat.inj H₄,
have h₆ : n = 0,                     from nat.eq_zero_of_add_eq_zero_right H₅,
show a = b, from
  calc
    a = a + 0    : by simp only [add_zero]
  ... = a + n    : by simp only [h₆, int.coe_nat_zero]
  ... = b        : Hn
end

which is working but:

Q1: I don't know how to get rid of the simp only(use more atomic rw/apply/.... instead) and the *coe* lemmas which were not there in the original proof.

[Scott Morrison]

I'm not sure that simp only is any less atomic than rw!

[Utensil Song]

Q2: I don't know how to recover the explicit types for n and Hn in the obtain line.

[Utensil Song]

Scott Morrison said:

I'm not sure that simp only is any less atomic than rw!

Why? I thought rw is quite mechanical and simp only at least has some heuristic (not sure if it's the right word) logic?

[Jalex Stark]

my model of simp only is that it keeps trying to rw things from the list it's passed until it can't anymore

[Utensil Song]

Q3: VSCode can't give me type prompts when I hover but the prompts for the tactic:

image.png

[Jalex Stark]

that looks like you're in tactic mode

[Jalex Stark]

VSCode can't figure out what H is, that's kind of a "Lean-complete" problem

[Jalex Stark]

you should be able to figure out the type of H from the infoview

[Jalex Stark]

(if you haven't updated your vscode lean plugin in the past month, you might have "lean goal" and "lean messages" tabs instead of a "lean infoview" tab. The latter is way better and you should update!)

[Utensil Song]

Yeah, there would return to Q2

[Utensil Song]

Jalex Stark said:

(if you haven't updated your vscode lean plugin in the past month, you might have "lean goal" and "lean messages" tabs instead of a "lean infoview" tab. The latter is way better and you should update!)

I had and I joined the widget world already. :tada:

[Jalex Stark]

so you can get the types of those things from the widgets as long you can get the constants into your tactic state

[Scott Morrison]

Both simp and rw use different strategies for replacing sub-expressions, so work in slightly different situations. A big difference, of course, is that simp tries to rewrite multiple times, and by default includes a large pool of lemmas to try rewriting by (if you don't use only).

[Scott Morrison]

But even simp_rw and rw are different tactics.

[Scott Morrison]

If you want to make simp only do even less work, you can replace it with a suitable simp_rw tactic.

[Utensil Song]

Jalex Stark said:

so you can get the types of those things from the widgets as long you can get the constants into your tactic state

image.png

I can't get it from the view, am I missing something?

[Utensil Song]

Utensil Song said:

Q2: I don't know how to recover the explicit types for n and Hn in the obtain line.

Not just recover, I wish to write it out explicitly like:

obtain ⟨n, Hn⟩ : ⟨ℕ, a + n = b⟩ := int.le.dest H₁, -- not legal Lean

[Jalex Stark]

it looks like the things you want to find the type of are not in your tactic state

[Jalex Stark]

if you get them into your tactic state, then you can mouse-over + click them there

[Utensil Song]

image.png

Another case is this 0. VSCode can't figure out whether this 0 is a nat or an int so it downgrades to showing prompts for from.

[Utensil Song]

Is this a bug of simp_rw? I was trying to figure out the partial order relation between rw, simp_rw, simp only, simp:

import tactic

variables (a b c d e : ℕ)
variable h1 : a = b
variable h2 : b = c + 1
variable h3 : c = d
variable h4 : e = 1 + d

include h1 h2 h3 h4

example : a = e := by rw [h1, h2, h3, add_comm, h4]

/-
ERROR: simplify tactic failed to simplify
-/
example : a = e := by simp_rw [h1, h2, h3, add_comm, h4]

/-
WORKS after reordering
-/
example : a = e := by simp_rw [h1, h2, h3, h4, add_comm]

example : a = e := by simp only [h1, h2, h3, add_comm, h4]

example : a = e := by simp [h1, h2, h3, add_comm, h4]

[Scott Morrison]

add_comm is a dangerous simp lemma. Used in simp (rather than simp_rw) it would obviously loop forever.

[Scott Morrison]

So there is some scary unspecified heuristic that decides whether it should fire or not.

[Scott Morrison]

Unfortunately it seems this heuristic is still applied in simp_rw, when it probably shouldn't be.

[Scott Morrison]

I agree it sounds like a bug... or at least an undesirable feature. :-)

[Utensil Song]

I see.

I'm aware of the existence of such heuristic logic (maybe from changelog) in simp(in C++ I think), that's probably when this logic change applied to simp_rw because it calls simp only [rule] at l for every rule in the ruleset in order.

[Utensil Song]

Utensil Song said:

I wish to write it out explicitly like:

obtain ⟨n, Hn⟩ : ⟨ℕ, a + n = b⟩ := int.le.dest H₁, -- not legal Lean

Silly me, it's actually very simple:

obtain ⟨n, Hn⟩ : ∃ n : ℕ, a + n = b := int.le.dest H₁,
obtain ⟨m, Hm⟩ : ∃ m : ℕ, b + m = a := int.le.dest H₂,

the "type" is just the proposition for the proof after :=, I was confused by the destructed pattern.