Zulip Chat Archive

Stream: general

Topic: rewrite le.antisymm from Lean 2


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 25 2020 at 04:42):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 25 2020 at 04:50):

that looks like you're in tactic mode

view this post on Zulip Jalex Stark (Jul 25 2020 at 04:51):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 04:51):

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

view this post on Zulip 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!)

view this post on Zulip Utensil Song (Jul 25 2020 at 04:52):

Yeah, there would return to Q2

view this post on Zulip 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!)

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Jul 25 2020 at 04:55):

But even simp_rw and rw are different tactics.

view this post on Zulip 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.

view this post on Zulip 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

image.png

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 25 2020 at 05:13):

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

view this post on Zulip Utensil Song (Jul 25 2020 at 05:16):

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.

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:10):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:11):

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

view this post on Zulip 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.

view this post on Zulip 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