Stream: new members
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
There are two things I could see might be happening here.
The type of
foomatches with the type of the goal, up to the types of the variables which are then inferred, closing the goal or
applymatches 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
fooand 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 (Oct 22 2020 at 00:43):
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
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