Something like Coq's discriminate

Stream: lean4

[Scott N. Walck]

Hi folks,

I like to try to learn more about lean by writing tactics and
seeing what sort of proof term is created. For this little
theorem,

theorem zero_not_one : 0 = 1 -> False := by simp
#print zero_not_one

I get

theorem zero_not_one : 0 = 1 → False :=
of_eq_true (Eq.trans (implies_congr (eq_false_of_decide (Eq.refl false)) (Eq.refl False)) Init.Core._auxLemma.4)

but what is Init.Core._auxLemma.4 ? I looked in the source code
for such a thing, but I couldn't find anything like it.

A second question: Is there a tactic similar to Coq's
discriminate, one that could conclude a proof from a hypothesis
of the form c1 x = c2 y, where c1 and c2 are different
constructors of some data type?

Thanks!

[Patrick Massot]

Please do not post the same message twice. The only possible effect of that strategy is that someone wastes time answering your question while someone already answered the other copy.

[Patrick Massot]

Init.Core._auxLemma.4 is some internal lemma you shouldn’t try to access directly. For your second question, the answer is probably injection but it’s hard to tell without a #mwe.

[Scott N. Walck]

Sorry for the double post. I didn't realize the first one went through.

[Kevin Buzzard]

If you think Init.Core._auxLemma.4 is bad, try proving $(x+y)^2=x^2+2xy+y^2$ with ring and inspecting the term that the tactic generates; it's completely incomprehensible. And other tactics are worse. My take on tactics is that they're exactly there to be used when you don't want to see the term, you just want to prove the theorem.

I would imagine that cases h would close a goal if h : c1 x = c2 y.

[Scott N. Walck]

Thanks for the advice. And

theorem zero_is_not_one : 0 = 1 -> False := by
  intro h
  cases h

works just great.

[Patrick Massot]

I think injection h should also work.

[Scott N. Walck]

theorem zero_is_not_one' : 0 = 1 -> False := by
  intro h
  injection h

also works great. Thanks.

[Kyle Miller]

Init.Core._auxLemma.4 is generated by simp. It's going to be wrapping a single simp lemma. If you use simp? you can see the list of simp lemmas that were used, and that will give you a good idea of what it could be. Mario gave a hack to print such a lemma if you want to dig in.