CODEWITHSUNDEEP
logiccoq
Necto
Necto

Reputation: 2654

How to show that two variables of inductive type are inequal if their fields are not equal?

Suppose I have an inductive type:

Inductive addr : Type :=  mk_addr : Z -> Z -> addr.

Is it possible to prove the following goal?

Goal
  forall (x y z : Z),
  y <> z -> mk_addr x y <> mk_addr x z.

Upvotes: 0

Views: 28

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

congruence can take care of it:

Goal
  forall (x y z : Z),
  y <> z -> mk_addr x y <> mk_addr x z. 

congruence.
Qed.

Alternatively, you can prove the contrapositive of that statement:

Goal
 forall (x y z : Z),
 y <> z -> mk_addr x y <> mk_addr x z.
intros x y z H1 H2.
apply H1.
injection H2.
trivial.
Qed.

Upvotes: 3

Related Questions