如何在字符串的布尔等式上进行模式匹配，并同时在Coq的证明中获得所需的命题等式？

Question

我在尝试证明SF中的substi_correct定理时陷入困境，因为我不知道如何分解布尔相等性，同时又将其断言为命题相等性。

Theorem substi_correct : forall s x t t',
  [x:=s]t = t' <-> substi s x t t'.
Proof.
  intros. 
  split. 
  + generalize dependent t'.
    induction t; intros.
    - simpl in H.
      subst.
      case (eqb_string x0 s0).
      * constructor. (*Doesn't work*)

证明目标如下，不需要H：x0 = s0，以便我可以继续。

  s : tm
  x0, s0 : string
  ============================
  substi s x0 (var s0) s

在Maps.v章节中，我们证明了一个错误的案例，此外]

Theorem eqb_string_true_iff : forall x y : string,
    eqb_string x y = true <-> x = y.
但是在（eqb_string x0 s0）上进行模式匹配时，我该如何使用然后继续进行？我是否应该将其用作证明中的引理，或者是否有更简单的方法进行？

我在尝试证明SF中的substi_correct定理时陷入困境，因为我不知道如何分解布尔相等性，同时又将其断言为命题相等性。定理...

Answer 1

您可以将destruct策略的变体与eqn:子句一起使用，以添加一个假设来记住您所处的情况：