## Stream: new members

### Topic: simpler proof 0<2?

#### 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


#### Mario Carneiro (Apr 12 2019 at 13:55):

use norm_num

#### Mario Carneiro (Apr 12 2019 at 13:55):

the auto proof should be something like bit0_pos one_pos

#### Mario Carneiro (Apr 12 2019 at 13:56):

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

#### 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

#### 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


#### Kenny Lau (Apr 12 2019 at 14:14):

two_pos

#### Patrick Massot (Apr 12 2019 at 14:15):

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

#### Patrick Massot (Apr 12 2019 at 14:15):

Joe, why do you add anything to this line?

#### Joseph Corneli (Apr 12 2019 at 14:25):

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

#### 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.

#### Mario Carneiro (Apr 13 2019 at 01:30):

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

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

#### 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

#### 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


#### Scott Morrison (Apr 13 2019 at 01:42):

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

#### 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.

#### 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"

#### 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