Zulip Chat Archive

Stream: new members

Topic: Conclusion of the type of a term.

Gihan Marasingha (Oct 22 2020 at 00:40):

I realise that though I can use it, I don't really understand what apply does. The docs state that apply tries to match the current goal with the conclusion of the type of the term. Consider the following example. I use apply with the term foo.

There are two things I could see might be happening here.

  1. The type of foo matches with the type of the goal, up to the types of the variables which are then inferred, closing the goal or

  2. apply matches the 'conclusion' of the type of foo (which I'd guess to be something like q ∧ p) with the goal. But this is where I'm stuck in understanding what is meant by the current goal. Certainly, (a → b) ∧ (b ∧ a) → (b ∧ a) ∧ (a → b) doesn't seem to match with q ∧ p. So is it that the 'conclusion' of the goal is matched with the conclusion of the type of foo and the proof of the remaining subgoals closed by inference?

Or is it something entirely different?

I'm sure someone more versed in meta programming than I could understand things perfectly just by reading the source. But is there a simple description of what is meant by the conclusion of the type of a term and (say in the example below) how it matches with the goal?

theorem foo (p q : Prop) : p  q  q  p :=
λ h, h.2, h.1

example (a b : Prop) : (a  b)  (b  a)  (b  a)  (a  b) :=
  apply foo,

Reid Barton (Oct 22 2020 at 00:43):

Basically apply foo means refine foo followed by some _s, the number of which is determined by a heuristic

Reid Barton (Oct 22 2020 at 00:44):

The heuristic is: look at the types of the goal and foo and see how many Pi/->s each one ends in, and subtract the former from the latter.

Reid Barton (Oct 22 2020 at 00:47):

This heuristic probably sounds like it would always work, but it doesn't and sometimes apply inserts the wrong number of _s, which we call "the apply bug".

Adam Topaz (Oct 22 2020 at 00:47):

When cleaning up proofs, I often replace apply foo with refine foo and start adding _ until lean doesn't complain. This is a good strategy I think when you want to replace a bunch of apply foos with exact bar

Bryan Gin-ge Chen (Oct 22 2020 at 00:52):

We should add some of the above info to the tactic doc!

Last updated: Dec 20 2023 at 11:08 UTC