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

(BEq a a0 = BTrue \/ BEq a a0 = BFalse) is either true or false since a==a0 or a!=a0. However, I'm not sure how I can get Coq to see this. Here is my complete proof 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')

Any suggestions on how to proceed?

Definitions:

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

Solution

I'm fairly certain that this is not provable. Given your proof context:

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')

You need to be able to prove at least one disjunct. BEq a a0 = BTrue is not provable. Beq and BTrue are two different constructors of the same type, so under Coq's equality, this will never hold. The same goes for BEq a a0 = BFalse. In fact, I can prove that these things are not equal:

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.

One might think that exists b' : bexp, BEq a a0 / st ==>b b' could be proven, by inducting on a and then destructing a0. This would give you a bunch of cases, and you would need to show that for each case you can take a step, however, you will inevitably find yourself in a case where you won't be able to show that a step can be taken. For example, if you have the case where a is APlus (AId x) (ANum 12), and a0 is some other arbitrary expression, then you will need to show that it is possible for BEq (APlus (AId x) (ANum 12)) a0 to take a step. You might think that you can use the BS_Eq1 rule, however, you have no guarantee that APlus (AId x) (ANum 12) can take a step under your ==>a relation, assuming that to use an id, it needs to be in the current state. If x does not currently exist in the given state, you will not be able to take a step.