什么是正确的证明术语，以便 ssreflect 教程与 exact: hAiB 示例一起工作？

Question

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

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.

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

这让我感到困惑...这是因为 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.

(* 

*)
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.

什么是正确的证明术语，以便 ssreflect 教程与 exact: hAiB 示例一起工作？

What is the right proof term so that the ssreflect tutorial work with the exact: hAiB example?

coq

coq-tactic