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

Question

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


4个子目标
a:aexp
a0:aexp
st : 状态
______________________________________(1/4)
(BEq a a0 = BTrue\/BEq a a0 = BFalse)\/
(存在 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

我相当确定这是无法证明的。鉴于您的证明背景:

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. 

有人可能认为存在 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 当前在给定状态下不存在，您将无法采取任何步骤。