Zulip Chat Archive

Stream: new members

Topic: simpler proof 0<2?


view this post on Zulip Joseph Corneli (Apr 12 2019 at 13:53):

In general I would view a one-line proof as simple, but this one generates a big proof term. Is this the preferred proof?

import data.real.basic tactic.linarith
lemma simple : (0:) < 2 :=
begin
linarith,
end

#print simple

view this post on Zulip Mario Carneiro (Apr 12 2019 at 13:55):

use norm_num

view this post on Zulip Mario Carneiro (Apr 12 2019 at 13:55):

the auto proof should be something like bit0_pos one_pos

view this post on Zulip Mario Carneiro (Apr 12 2019 at 13:56):

PS: why always with the reals? They are a pain to import

view this post on Zulip Mario Carneiro (Apr 12 2019 at 13:59):

By the way, this is one of the reasons I don't like too much blasty in my tactics. Like you say, a simple looking proof should actually be simple. Big super tactics break this connection - a tiny by tidy might be a huge term behind the scenes, and the only direct exposure you have to it is in compile times, which kill you in tiny distributed amounts until the library is so slow and there is no easy fix

view this post on Zulip Joseph Corneli (Apr 12 2019 at 14:07):

Ah that's much nicer, thanks Mario. The reals are b/c I'm doing continuity proofs.

theorem simple : 0 < 2 :=
eq.mpr (id (eq_true_intro (bit0_pos zero_lt_one))) trivial

view this post on Zulip Kenny Lau (Apr 12 2019 at 14:14):

two_pos

view this post on Zulip Patrick Massot (Apr 12 2019 at 14:15):

lemma simple : (0:ℝ) < 2 := bit0_pos zero_lt_one

view this post on Zulip Patrick Massot (Apr 12 2019 at 14:15):

Joe, why do you add anything to this line?

view this post on Zulip Joseph Corneli (Apr 12 2019 at 14:25):

@Patrick Massot the somewhat longer proof was what was supplied by norm_num.

view this post on Zulip Scott Morrison (Apr 13 2019 at 00:55):

I wonder a bit why we don't call dsimp on the generated proofs themselves, for things like norm_num. We don't have all the relevant lemmas written for simplifying proofs themselves, but I think sometimes it's valuable --- especially if people are copying and pasting tactic generated proofs.

view this post on Zulip Mario Carneiro (Apr 13 2019 at 01:30):

I've tried it, lean doesn't like to simplify proofs

view this post on Zulip Mario Carneiro (Apr 13 2019 at 01:31):

which means you have to deal with any cruft added by upstream tactics (this one is simp's fault)

view this post on Zulip Mario Carneiro (Apr 13 2019 at 01:36):

There are a lot of easy simplifications you can apply; one easy one I would like to do is if a subterm of P proves the same theorem T as P itself, then you can replace P with the subterm. This looks really obviously unprofessional in #explode, I'm thinking "why are you still working? You did it already". This is part of the metamath workflow, but somehow there isn't a good way to do this in lean and so #print foo just shows you crappy proofs most of the time

view this post on Zulip Scott Morrison (Apr 13 2019 at 01:42):

Hmm... I'm pretty sure I've simplified proofs in the past. I've certainly made use of the lemmas

@[simp] lemma congr_arg_refl {α : Sort*} {β : Sort*} {f : α → β} {a : α} :
  congr_arg f (eq.refl a) = eq.refl (f a) := rfl

@[simp] lemma congr_fun_refl {α : Sort*} {β : Sort*} {f : α → β} {a : α} :
  congr_fun (eq.refl f) a = eq.refl (f a) := rfl

@[simp] lemma congr_refl_fun {α : Sort*} {β : Sort*} {f : α → β} {a₁ a₂ : α} (h : a₁ = a₂) :
  congr (eq.refl f) h = congr_arg f h := rfl

@[simp] lemma congr_refl_arg {α : Sort*} {β : Sort*} {f₁ f₂ : α → β} {a : α} (h : f₁ = f₂) :
  congr h (eq.refl a) = congr_fun h a := rfl

view this post on Zulip Scott Morrison (Apr 13 2019 at 01:42):

I wonder when you can and can't run the simplifier on proofs.

view this post on Zulip Scott Morrison (Apr 13 2019 at 01:43):

I've needed these lemmas times that a strange eq.rec has appeared, and I can't even see the underlying non-definitional equality that caused the problem, because it's stacked up inside a million congr and eq.mpr and eq.symms, etc.

view this post on Zulip Mario Carneiro (Apr 13 2019 at 02:28):

I am pretty sure the problem is simp ignores arguments of prop type because it thinks "proofs are irrelevant"

view this post on Zulip Mario Carneiro (Apr 13 2019 at 02:29):

It's possible you can get it to sometimes trigger, but it doesn't work on large scale


Last updated: May 10 2021 at 18:22 UTC