Zulip Chat Archive

Stream: general

Topic: guess the error

Kevin Buzzard (Mar 29 2018 at 15:31):

theorem  easy : let H : 0  <  2  := dec_trivial in
(⟨0,H⟩ : fin 2) = ⟨0,H⟩ := rfl

Gabriel Ebner (Mar 29 2018 at 16:01):

Ah, I guess there are two ways in which a lemma can fail to be rfl: either the proof is not rfl, or the proposition is not an equation.

Gabriel Ebner (Mar 29 2018 at 16:02):

Note that easy would not work as a simp lemma, since it matches on the let instead of the fin.mk (and the exact decidability proof):

#eval simp_lemmas.mk.add_simp ``easy >>= simp_lemmas.pp >>= tactic.trace
-- simplification rules for iff
-- [easy] #0, let H : 0 < 2 := _ in ⟨0, H⟩ = ⟨0, H⟩ ↦ true

Gabriel Ebner (Mar 29 2018 at 16:04):

To explain: lemma foo : ... = ... := rfl is only intended to be used for simp-lemmas. And then it literally needs to be rfl on the right-hand side. Not eq.refl _, not by refl, but rfl.

Gabriel Ebner (Mar 29 2018 at 16:05):

So in your case you can just use by refl or eq.refl _ and easy will work.

Kevin Buzzard (Mar 29 2018 at 17:46):

So this let isn't just syntactic sugar?

Sebastian Ullrich (Mar 30 2018 at 15:38):

No, let is a primitive term kind supported by the kernel

Kevin Buzzard (Jun 13 2020 at 12:23):

import tactic

lemma fish : 2 + 2 = 4 :=
begin
  refl
end

(doesn't compile)

Reid Barton (Jun 13 2020 at 12:26):

I'm hoping the error is that there is already a lemma named fish

Kevin Buzzard (Jun 13 2020 at 12:26):

Furthermore, it's not just some random test lemma, there's even a little API for it. We have fish_pipe and fish_pure for example.

Johan Commelin (Jun 13 2020 at 12:26):

That's why you should always call your lemmas fishy.

Reid Barton (Jun 13 2020 at 12:26):

ohh

Reid Barton (Jun 13 2020 at 12:26):

ok, now I know what it is

Kevin Buzzard (Jun 13 2020 at 12:27):

What the heck is a fish pipe?

Reid Barton (Jun 13 2020 at 12:27):

I didn't know it was actually called fish though, that's funny.

Reid Barton (Jun 13 2020 at 12:27):

It's the (a -> m b) -> (b -> m c) -> a -> m c thing right?

Johan Commelin (Jun 13 2020 at 12:27):

@Kevin Buzzard >=> |?

Kevin Buzzard (Jun 13 2020 at 12:28):

(I just needed a random lemma name so I could #print it to check I got a more useful answer than "Lean forgot the proof of your lemma" (and indeed I do))

Reid Barton (Jun 13 2020 at 12:29):

I hope this is going in some setup documentation

Reid Barton (Jun 13 2020 at 12:29):

"To check that you have installed Lean correctly, type #print fish"

Last updated: Dec 20 2023 at 11:08 UTC