## Stream: general

### Topic: rewrite le.antisymm from Lean 2

#### Utensil Song (Jul 25 2020 at 04:42):

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 (Jul 25 2020 at 04:42):

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

#### Utensil Song (Jul 25 2020 at 04:44):

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

#### Utensil Song (Jul 25 2020 at 04:46):

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 (Jul 25 2020 at 04:48):

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 (Jul 25 2020 at 04:49):

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

image.png

#### Jalex Stark (Jul 25 2020 at 04:50):

that looks like you're in tactic mode

#### Jalex Stark (Jul 25 2020 at 04:51):

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

#### Jalex Stark (Jul 25 2020 at 04:51):

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

#### Jalex Stark (Jul 25 2020 at 04:52):

(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 (Jul 25 2020 at 04:53):

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!)

#### Jalex Stark (Jul 25 2020 at 04:54):

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 (Jul 25 2020 at 04:54):

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 (Jul 25 2020 at 04:55):

But even simp_rw and rw are different tactics.

#### Scott Morrison (Jul 25 2020 at 04:55):

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

#### Utensil Song (Jul 25 2020 at 04:55):

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

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

#### Utensil Song (Jul 25 2020 at 04:58):

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 (Jul 25 2020 at 05:13):

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

#### Jalex Stark (Jul 25 2020 at 05:13):

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

#### Utensil Song (Jul 25 2020 at 05:16):

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 (Jul 25 2020 at 11:39):

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 (Jul 25 2020 at 12:10):

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

#### Scott Morrison (Jul 25 2020 at 12:10):

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

#### Scott Morrison (Jul 25 2020 at 12:11):

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

#### Scott Morrison (Jul 25 2020 at 12:11):

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

#### Utensil Song (Jul 25 2020 at 13:17):

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 (Jul 25 2020 at 13:23):

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.

Last updated: May 13 2021 at 20:13 UTC