_ hidden_ goal_错误消息的含义是什么

Question

编辑：我包括了证明。

我将一个证明（从软件基金会获取的证明）从一个文件复制到另一个文件。在原始文件中，一切编译正常。在新文件中，错误：

Hs is used in hypothesis _the_hidden_goal_.

是由行引起的

rewrite H in Hs.

这是什么意思？谷歌搜索“ _the_hidden_​​goal_”后发现的唯一信息是here。根据该链接，我将有问题的行更改为

rewrite H in Hs *.

现在可以编译，但是我不明白为什么。

谢谢。

编辑：

这里是导致带有*的问题的证据。

Lemma eqb_string_true_iff : forall x y : string,
    eqb_string x y = true <-> x = y.
Proof.
   intros x y.
   unfold eqb_string.
   destruct (string_dec x y) as [H |Hs].
   - subst. split. reflexivity. reflexivity.
   - split.
     + intros contra. discriminate contra.
     + intros H. rewrite H in Hs *. destruct Hs. reflexivity.
Qed.

仅在包含证明，eqb_string和某些导入语句的文件中仍然会出现问题。这是文件的总内容。

From Coq Require Import Bool.Bool Init.Nat Arith.Arith Arith.EqNat
     Init.Datatypes Lists.List Strings.String.
Require Export Coq.Strings.String.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
Import ListNotations.
Open Scope string_scope.

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.


Lemma eqb_string_true_iff : forall x y : string,
    eqb_string x y = true <-> x = y.
Proof.
   intros x y.
   unfold eqb_string.
   destruct (string_dec x y) as [H |Hs].
   - subst. split. reflexivity. reflexivity.
   - split.
     + intros contra. discriminate contra.
     + intros H. rewrite H in Hs. destruct Hs. reflexivity.
Qed.
Close Scope string_scope.

Answer 1

当您输入rewrite H in Hs时，SSReflect大致执行如下：

set (_the_hidden_goal_ := _). (* hide the goal to prevent rewriting in it *)
revert Hs. (* put the hypothesis in the goal to rewrite in it *)
pattern x. (* extract the left-hand side of the equality *)
case H. (* perform the actual rewriting *)
intros Hs. (* put back the hypothesis in the context *)
unfold _the_hidden_goal_. (* restore the goal *)

由于Hs出现在_the_hidden_goal_的正文中，因此对revert Hs的调用失败，因此会出现错误消息。

通过使用rewrite H in Hs *，您告诉SSReflect您想同时重写Hs和目标。因此，SSReflect跳过了第一步和最后一步。这解决了问题。

注意，这里唯一反映SSReflect的东西是名称_the_hidden_goal_的用法。通过使用Coq的香草rewrite，您也会遇到类似的失败。更准确地说，rewrite -> H in Hs抱怨以下消息：Cannot change Hs, it is used in conclusion.