在 Coq 中求解 (BEq a0 = BTrue \/ BEq a0 = BFalse)

Question

(BEq a a0 = BTrue \/ BEq a a0 = BFalse) 为真或假，因为 a==a0 或 a!=a0。但是，我不确定如何让 Coq 看到这一点。这是我的完整证明 window:

4 subgoal a : aexp a0 : aexp st : state ______________________________________(1/4) (BEq a a0 = BTrue \/ BEq a a0 = BFalse) \/ (exists b' : bexp, BEq a a0 / st ==>b b')

对如何进行有什么建议吗？

定义：

Inductive bexp : Type :=
    BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp
.
Inductive aexp : Type :=
    ANum : nat -> aexp
  | AId : id -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp
.

Inductive bstep : state -> bexp -> bexp -> Prop :=
  | BS_Eq : forall st n1 n2,
      (BEq (ANum n1) (ANum n2)) / st ==>b 
      (if (beq_nat n1 n2) then BTrue else BFalse)
  | BS_Eq1 : forall st a1 a1' a2,
      a1 / st ==>a a1' ->
      (BEq a1 a2) / st ==>b (BEq a1' a2)
  | BS_Eq2 : forall st v1 a2 a2',
      aval v1 -> 
      a2 / st ==>a a2' ->
      (BEq v1 a2) / st ==>b (BEq v1 a2')
  | BS_LtEq : forall st n1 n2,
      (BLe (ANum n1) (ANum n2)) / st ==>b 
               (if (ble_nat n1 n2) then BTrue else BFalse)
  | BS_LtEq1 : forall st a1 a1' a2,
      a1 / st ==>a a1' ->
      (BLe a1 a2) / st ==>b (BLe a1' a2)
  | BS_LtEq2 : forall st v1 a2 a2',
      aval v1 ->
      a2 / st ==>a a2' ->
      (BLe v1 a2) / st ==>b (BLe v1 (a2'))
  | BS_NotTrue : forall st,
      (BNot BTrue) / st ==>b BFalse
  | BS_NotFalse : forall st,
      (BNot BFalse) / st ==>b BTrue
  | BS_NotStep : forall st b1 b1',
      b1 / st ==>b b1' ->
      (BNot b1) / st ==>b (BNot b1')
  | BS_AndTrueTrue : forall st,
      (BAnd BTrue BTrue) / st ==>b BTrue
  | BS_AndTrueFalse : forall st,
      (BAnd BTrue BFalse) / st ==>b BFalse
  | BS_AndFalse : forall st b2,
      (BAnd BFalse b2) / st ==>b BFalse
  | BS_AndTrueStep : forall st b2 b2',
      b2 / st ==>b b2' ->
      (BAnd BTrue b2) / st ==>b (BAnd BTrue b2')
  | BS_AndStep : forall st b1 b1' b2,
      b1 / st ==>b b1' ->
      (BAnd b1 b2) / st ==>b (BAnd b1' b2)

  where " t '/' st '==>b' t' " := (bstep st t t').

Answer 1

由于 BEq 是您的 bexp 类型的构造函数，所以一开始没有理由让我相信您的陈述是正确的。这只是一个名称，如 BLe，因此没有任何内容告诉 Coq 这应该被解释为 bexp 上的等式。但是，您可以使用 bstep.

的描述来证明您的完整陈述

目前我不能做更多的事情，因为我们缺少 ==>a（astep 我想）和 state.

的定义

Answer 2

我相当确定这是无法证明的。鉴于您的证明上下文：

4 subgoal
a : aexp
a0 : aexp
st : state
______________________________________(1/4)
(BEq a a0 = BTrue \/ BEq a a0 = BFalse) \/
(exists b' : bexp, BEq a a0 / st ==>b b')

您需要能够证明至少一个析取式。 BEq a a0 = BTrue 无法证明。 Beq 和 BTrue 是同一类型的两个不同构造函数，因此在 Coq 的相等性下，这永远不会成立。 BEq a a0 = BFalse 也是如此。其实我可以证明这些东西不相等：

Theorem BeqBFalseNeq : forall a a0, BEq a a0 <> BFalse.
Proof.
  intros a a0 contra. inversion contra. 
Qed. 

Theorem BeqBTrueNeq : forall a a0, BEq a a0 <> BTrue.
Proof.
  intros a a0 contra. inversion contra. 
Qed.

有人可能认为 exists b' : bexp, BEq a a0 / st ==>b b' 可以通过在 a 上归纳然后销毁 a0 来证明。这会给你一堆案例，你需要证明对于每个案例你都可以采取步骤，但是，你将不可避免地发现自己处于无法证明可以采取步骤的情况下.例如，如果 a 是 APlus (AId x) (ANum 12)，而 a0 是其他任意表达式，那么您需要证明 BEq (APlus (AId x) (ANum 12)) a0 是可能的迈出一步。你可能认为你可以使用 BS_Eq1 规则，但是，你不能保证 APlus (AId x) (ANum 12) 可以在你的 ==>a 关系下采取步骤，假设要使用 id，它需要处于当前状态。如果 x 目前在给定状态下不存在，您将无法进行下一步。

在 Coq 中求解 (BEq a0 = BTrue \/ BEq a0 = BFalse)

Solving (BEq a a0 = BTrue \/ BEq a a0 = BFalse) in Coq

proof

coq