tpil issue: 'equation compiler failed'

Stream: general

[Gihan Marasingha]

@Jeremy Avigad
The following code, from Chapter 8 of #tpil, gives 4 error messages in Lean 3.30. It works fine in (e.g.) Lean 3.23.

example {α : Type*} (p q : α → Prop) :
  (∃ x, p x ∨ q x) → (∃ x, p x) ∨ (∃ x, q x)
| (exists.intro x (or.inl px)) := or.inl (exists.intro x px)
| (exists.intro x (or.inr qx)) := or.inr (exists.intro x qx)

The error message on the first line is equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details).

The two messages on the third line are invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )') exists.intro x (or.inl px) and a similar message with qx in place of px.

The error message on the final line is don't know how to synthesize placeholder (x)

The trace output is:

[eqn_compiler.elim_match] depth [1]
match _example : (∃ (x : α), p x) ∨ ∃ (x : α), q x[ᾰ]
  (exists.intro ⁇ (or.inl ⁇)) := or.inl (exists.intro ⁇ ⁇)
  (exists.intro ⁇ (or.inr ⁇)) := or.inr (exists.intro ⁇ ⁇)
example: (ᾰ)
[eqn_compiler.elim_match] compilation failed at
match _example : (∃ (x : α), p x) ∨ ∃ (x : α), q x[ᾰ]
  (exists.intro ⁇ (or.inl ⁇)) := or.inl (exists.intro ⁇ ⁇)
  (exists.intro ⁇ (or.inr ⁇)) := or.inr (exists.intro ⁇ ⁇)
example: (ᾰ)

[Eric Rodriguez]

Exists.intro works, the type is now callled Exists but there's still some abbreviations to the old one

[Eric Rodriguez]

exists.intro has @[pattern], though, which I think should make it work

[Gihan Marasingha]

@Eric Rodriguez brilliant! A suggestion: the introduction to #tpil states, "This tutorial describes the current version of Lean, known as Lean 3". Is is worth being more precise about the Lean version against which #tpil has been tested?

[Bryan Gin-ge Chen]

(deleted)

[Gihan Marasingha]

@Eric Rodriguez I note that the type was called Exists in Lean 3.23 too. The difference I see is that Lean 3.33 has

@[pattern]
lemma exists.intro {α : Sort u} {p : α → Prop} (w : α) (h : p w) : ∃ x, p x := ⟨w, h⟩

in logic.lean whereas Lean 3.23 has

@[pattern]
def exists.intro := @Exists.intro

I think this is another example of the dreaded lemma vs def issue I asked about recently! I'll PR.

Sorry, I can't PR as this is core Lean!

[Bryan Gin-ge Chen]

It looks like @Floris van Doorn made the change in lean#545 to fix a linting issue. I don't know if the breakage you're seeing is intentional though.

[Mario Carneiro]

Note that def is sometimes used to make aliases like this without having to state the type. In mathlib we can use alias instead, which gets lemma/def right, but it's not available in core

[Jeremy Avigad]

@Eric Rodriguez @Gihan Marasingha Thanks for catching this mistake and debugging. I'll fix it. Give me a few days to get to it -- I'll update to the latest version of Lean and re-check all the code.

The title page of the PDF documentation indicates the version of Lean. (It's set in a config file, so it's only correct if I remember to update it when I bump and retest.) I don't think we need to emphasize it in the text -- we should just aim to describe the current version.

[Gihan Marasingha]

@Jeremy Avigad thanks. But is this an issue with #tpil or with the new definition of exists.intro in core Lean? Is the behaviour exhibited by the new definition what one would expect?

[Jeremy Avigad]

Good question. It would be best if exists.intro could be made to work... If not, I don't know the best workaround. @Floris van Doorn, what do you think?

[Jeremy Avigad]

(I wouldn't mind simply deleting the example, or using Exists.intro and explaining that we had to use the capital "E" to make the pattern matching work.)

[Floris van Doorn]

I think we can go back and make exists.intro a def. I'm happy to add the exception "Prop sorted declarations are allowed to be def if they have the @[pattern] attribute" to the linter.

[Floris van Doorn]

lean#582 & #7785