如何证明，如果两个变量的场不相等，那么归纳类型的两个变量是不相等的?

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.

1 个解决方案

#1

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.