CODEWITHSUNDEEP
coqtheorem-proving
ScarletAmaranth
ScarletAmaranth

Reputation: 5101

Behaviour of the apply tactic when the goal and the applied term match

Suppose we have A B C : Prop.
Given a context with H : A -> B -> C and a single goal A -> B -> C,
why is it possible to apply H to finish the proof, solving the current and only goal?

I thought the apply tactic generates a new goal for each of the arguments of the term being applied should its conclusion match (or be unifiable with) the current goal.

Upvotes: 1

Views: 69

Answers (1)

Vinz
Vinz

Reputation: 6047

What you are describing would happen if your goal was only C: to prove C from H: A -> B -> C, you would have to provide witnesses for A and B. However, your current situation is just an instance of proving P knowing P, whatever the shape of P is. Therefore, by applying H, you provide enough information to close the goal.

Upvotes: 1

Related Questions