show_term produces invalid term?

Stream: general

[Alexandre Rademaker]

The term https://gist.github.com/arademaker/d380c85c91a4f61391009f25a09ecf54#file-simple-lean-L28 was produced by show_term from both tactic-based proofs above it. The last proof would be the more direct term-based proof. But the term produced by show_term is an error, Lean says invalid constructor ⟨...⟩, expected type is not an inductive type any explanation?

[Yakov Pechersky]

Because it is an example, it doesn't infer that you're making an and term. So it doesn't understand that the constructor syntax you're using is valid here. You could use or.inl (and.intro h.left hb) for example. Or say or.inl (⟨h.left, hb⟩ : (A ∧ B))

[Alexandre Rademaker]

oh. do you mean I would have different results with I was creating a lemma instead of an example? I tried and it didn't work. Yes, the correct and more verbose proof I constructed in https://gist.github.com/arademaker/d380c85c91a4f61391009f25a09ecf54#file-simple-lean-L30-L33. But don't you think it is a 'bug' of the show_term?

[Eric Wieser]

The bug is in the pretty-printer - Lean 3 is notoriously bad at emitting expressions that contain enough information for the elaborator to read them back.

[Kevin Buzzard]

I would have said "very good, except for a couple of gotchas which people have got used to"...

[Eric Wieser]

Well, from my pespective it has frequently been so bad that I just avoid change entirely because I stand no hope of actually writing down the goal state that I was hoping to get to, and instead have to find the appropriately named refl lemmas

[Eric Wieser]

But that might just be a function of the sorts of objects I'm working with

[Eric Wieser]

Maybe I should blame the elaborator instead of the pretty printer though, since sometimes I just cannot write the expression I need:
https://github.com/leanprover-community/mathlib/blob/20b49fbd453fc42c91c36ee30ecb512d70f48172/src/linear_algebra/pi_tensor_product.lean#L466-L467

[Yakov Pechersky]

Another golf:

example (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
λ ⟨f, g⟩, g.imp (and.intro f) (and.intro f)

[Bryan Gin-ge Chen]

Here are some related issues: #5659, lean#394. Note that this is very unlikely to be fixed in Lean 3; the story in Lean 4 should be much better.