Zulip Chat Archive

Stream: new members

Topic: Conclusion of the type of a term.


view this post on Zulip 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) :=
begin
  apply foo,
end

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Oct 22 2020 at 00:52):

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


Last updated: May 10 2021 at 00:31 UTC