How do I show that if a hypothesis implies not, it's the same as saying the proposition equals false (coq)?

user_19122983 0
Viewed 41

I want to prove two characters are not equal. My environment currently looks like this:

H: c1 = c2 -> not
_____________________
Goal: (c1 =? c2)%char = false

It won't allow me to apply H or rewrite H to solve the goal, and H is not invertible. The goal directly follows from the hypothesis, so how can I prove this? Do I need a helper lemma?

coq-tactic coq proof functional-programming
1 Answers

Looks like there is a typo in your hypothesis H ?
Do you mean not (c1 = c2) (or c1 <> c2, or c1 = c2 -> False) ?

If so, you may apply a lemma of Standard Library:

Search (_ =? _)%char. 

Goal forall c1 c2: ascii,
    c1 <> c2 -> (c1 =? c2)%char = false.
Proof.
  intros c1 c2; apply eqb_neq.
Qed.

It may be interesting to look at the proof of eqb_neqtoo, in order to understand how to prove this kind of lemmas.

user_94151920
Related