Conclusion of the type of a term.

Stream: new members

[Gihan Marasingha]

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) :=
begin
  apply foo,
end

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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