simpler proof 0<2?

Stream: new members

[Joseph Corneli]

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]

use norm_num

[Mario Carneiro]

the auto proof should be something like bit0_pos one_pos

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

two_pos

[Patrick Massot]

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

[Patrick Massot]

Joe, why do you add anything to this line?

[Joseph Corneli]

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

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Scott Morrison]

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]

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

[Mario Carneiro]

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