CODEWITHSUNDEEP
coq
rosi javi
rosi javi

Reputation: 35

How to provide proof that two values are different?

I am looking for an example in Coq for difference between two statements. True is equal to false and true is not equal to true. I do not find how to finish the proof, if have this expression. true <> true.

Upvotes: 0

Views: 133

Answers (2)

Tiago Campos
Tiago Campos

Reputation: 538

Let's check a casual example when you have :

Theorem easily : true <> false.
  -------------------------------
true <> false.

you can just desugar the <> negation to some Prop -> False,

Theorem easily : true <> false.
  intro H.
--------------------------------
H : true = false
--------------------------------
False

As H is a contradiction, you can just use inversion H and finish the proof, dependently typed talking you just have to provide anti-congruence absurd between the values, in Coq it can be done with eq_rect.

Theorem easily : true <> false.
  intro H.
  (*check eq_rect with Compute eq_rect*)
  pose (fun h => @eq_rect _ _ (fun x => match x with
                    |true => True
                    |false => False
                 end) h _ H) as c.
  simpl in c.
--------------------------------
H : true = false
c := fun h : True =>
 eq_rect true (fun x : bool => if x then True else False) h false H 
   : True -> False
--------------------------------
False
--------------------------------
  exact (c I).
  Qed.

In your example, you just have to provide proof that true = true.

Theorem easily : true <> true -> False.
  intro H.
  cbv in H.
  exact (H (eq_refl)).
  Restart. (* or just contradiction *)
  contradiction.
Qed.

Remember with easily you can finish any goal that has true <> true as a premise.

Upvotes: 1

Th&#233;o Winterhalter
Th&#233;o Winterhalter

Reputation: 5108

When you have something like this, you can use tactics like contradiction. to close the goal.

Upvotes: 0

Related Questions