正确的证明术语是什么，以便 ssreflect 教程适用于准确的：hAiB 示例？

Question

我正在阅读教程 https://hal.inria.fr/inria-00407778/document< /a> 对于 ssreflect ，他们有证据：

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.

但它实际上不起作用，因为目标

B

让我困惑......这是什么不起作用，因为 coq 版本改变了？或者也许还有别的什么？确切的论据应该是什么？

---

我想我确实理解 exact 参数的作用。它通过确保给出的证明项（程序）具有当前目标的类型来完成当前的子目标。例如，

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.

用于证明加法的交换律。

---

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.

我正在使用的完整脚本。为什么不把假设放在当地环境中呢？

Answer 1

您的示例失败的原因可能是您没有打开一个部分。您声明的各种假设将被视为“公理”，而不是在目标的背景下。

另一方面，如果您在发布的文本片段之前开始一个部分，则一切正常，因为 exact: hAiB. 策略之前的目标还包含假设 hA，这是 exact: 成功所必需的。

这是完整的脚本（在 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.