guard that a proof fails?

Stream: new members

[Michal Wallace (tangentstorm)]

Is there a way to express the idea that I don't want a theorem to succeed for a particular input?

For example the following definition allows me to prove that 6 is prime.

import Mathlib.Data.Nat.Prime.Basic

theorem prime_of_sifted
  (c: Nat) (h2c: 2 ≤ c) (hfac: ∀p<c, p.Prime → ¬p∣c)
: c.Prime  := by sorry

example : Nat.Prime 7 :=
  prime_of_sifted 7 (by decide) (by decide)

example : Nat.Prime 6 :=
  prime_of_sifted 6 (by decide) (by decide)

The fact that the bottom line succeeds is meant to help me catch a deliberate mistake in the definition... But as soon as I fix the mistake, the bottom line produces an error.

I want to keep the line in, suppress the error because it's expected, and only have Lean complain if I accidentally mess up the definition again and don't get the error.

Possible?

[Michal Wallace (tangentstorm)]

(I am aware of #guard_msgs but if it does what I'm asking, I don't understand how to use it in this case...)

[Eric Wieser]

Michal Wallace (tangentstorm) said:

For example the following definition allows me to prove that 6 is prime.

Arguably this is a theorem, not a definition. If you are worried about your theorem allowing you to prove something false, then your best defense is to fill in the sorry

[Michal Wallace (tangentstorm)]

Well, right. But that's exactly what I'm trying to avoid.

I don't want to spend 5 hours trying and failing to remove sorry for a statement that I'm sure is provable only to discover I had a subtle typo all along and was trying to prove the wrong thing.

[Michal Wallace (tangentstorm)]

(Especially as a beginner, I don't know what ought to be easy or hard to prove, and I'm probably going to struggle either way. I'm looking for a way to sanity check my goals somewhat before I invest the time into proving them.)

[Bjørn Kjos-Hanssen]

You can check if decide is able to produce a contradiction from all the things l1, l2, ... you proved so far, with the following primitive method:

import Mathlib.Data.Nat.Prime.Basic

theorem prime_of_sifted
  (c: Nat) (h2c: 2 ≤ c) (hfac: ∀p<c, p.Prime → ¬c∣p)
: c.Prime  := by sorry

lemma l1 : Nat.Prime 7 :=
  prime_of_sifted 7 (by decide) (by decide)

lemma l2 : Nat.Prime 6 :=
  prime_of_sifted 6 (by decide) (by decide)

lemma test : False := by
  have L1 := l1
  have L2 := l2
  revert L1 L2
  decide

[Michal Wallace (tangentstorm)]

Huh. That's an interesting thought. I was thinking about adding this idea to a video I'm making for people who've never heard of lean. I like this, but if I can't get it in one line or command, I'll probably just cut that section.

[Adomas Baliuka]

There's also slim_checkand maybe native_decidethat could sometimes help checking if statements are true before starting a proof