No such contradiction error

Using Coq
1

Hello, I am trying to use contradiction tactic to proof several cases automatically but getting error.

  b : bexp
  c : com
  IHc : forall (st st1 st2 : state) (s1 s2 : result),
        st =[ c ]=> st1 / s1 -> st =[ c ]=> st2 / s2 -> st1 = st2 /\ s1 = s2
  st1, st2 : state
  H2 : st1 =[ WHILE b DO c END ]=> st2 / SContinue
  H1 : st1 =[ WHILE b DO c END ]=> st1 / SContinue
  H6 : beval st1 b = false
  st4 : state
  H10 : st1 =[ c ]=> st4 / SContinue
  H9 : beval st1 b = true
  H14 : st4 =[ WHILE b DO c END ]=> st2 / SContinue
  ============================
  st1 = st2 /\ SContinue = SContinue

Here is the state

Error: Ltac call to "contradiction (constr_with_bindings_opt)" failed.
       No such contradiction

And here is error I am getting.

Should the contradiction tactic find that H6 and H9 contradict to each other? Is this expected behavior?

And if it is, then how to perform

rewrite H6 in H9 ; discriminate.

automatically for all similar cases?

2

The tactic congruence will do what you expected. Note that
contradiction can be applied if a hypothesis is False. In your case,
the congruence tactic will conclude that false = true; the goal
is then discharged similarly to the discriminate tactic.

(The following should also work: rewrite H6 in H6; discriminate.)

2 Likes
3

I assumed you meant rewrite H6 in H9; discriminate. (or rewrite H9 in H6; discriminate.)

1 Like