I was going through the tutorial https://hal.inria.fr/inria-00407778/document for ssreflect and they have the proof:
Variables A B C : Prop.
Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).
Lemma HilbertS2 :
C.
Proof.
apply: hAiBiC; first by apply: hA.
exact: hAiB.
Qed.
but it doesn't actually work since the goal is
B
which puzzled me...what is this not working because the coq version changed? Or perhaps something else? What was the exact argument supposed to be anyway?
I think I do understand what the exact argument does. It completes the current subgoal by making sure the proof term (program) given has the type of the current goal. e.g.
Theorem add_easy_induct_1_exact:
forall n:nat,
n + 0 = n.
Proof.
exact (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
(fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH) n).
Qed.
for the proof of addition's commutativity.
Module ssreflect1.
(* Require Import ssreflect ssrbool eqtype ssrnat. *)
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Theorem three_is_three:
3 = 3.
Proof. by []. Qed.
(*
https://stackoverflow.com/questions/71388591/what-does-apply-tactic-on-its-own-do-in-coq-i-e-without-specifying-a-rul
*)
Lemma HilbertS :
forall A B C : Prop,
(A -> B -> C) -> (A -> B) -> A -> C.
(* A ->(B -> C)*)
Proof.
move=> A B C. (* since props A B C are the 1st things in the assumption stack, this pops them and puts them in the local context, note using the same name as the proposition name.*)
move=> hAiBiC hAiB hA. (* pops the first 3 premises from the hypothesis stack with those names into the local context *)
move: hAiBiC. (* put hAiBiC tactic back *)
apply.
by [].
(* move: hAiB.
apply. *)
by apply: hAiB.
(* apply: hAiB.
by [].dd *)
Qed.
Variables A B C : Prop.
Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).
Lemma HilbertS2 :
C.
Proof.
apply: hAiBiC; first by apply: hA.
exact: hAiB.
Qed.
Lemma HilbertS2 :
C.
Proof.
(* apply: hAiBiC; first by apply: hA. *)
apply: hAiBiC. (* usually we think of : as pushing to the goal stack, so match c with conclusion in
selected hypothesis hAiBiC and push the replacement, so put A & B in local context. *)
by apply: hA. (* discharges A *)
exact: hAiB.
End ssreflect1.
full script I was using. Why does that not put the hypothesis in the local context?
The reason why your example fails is probably that you did not open a section. The various hypotheses that you declare are then treated as "axioms" and not in the context of the goal.
On the other hand, if you start a section before the fragment of text that you posted, everything works, because then the goal before the exact: hAiB. tactic also contains hypothesis hA, which is necessary for exact: to succeed.
Here is the full script (tested on coq 8.15.0)
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section sandbox.
Variables A B C : Prop.
Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).
Lemma HilbertS2 :
C.
Proof.
apply: hAiBiC; first by apply: hA.
exact: hAiB.
Qed.
End sandbox.