如何证明由coq中相同归纳的两个不同构造函数产生的项的不等式？

Question

考虑一下我有一个归纳法：

Inductive DirectSum{L R: Type}: Type := 
| Left: L -> DirectSum L R
| Right: R -> DirectSum L R
.

我如何证明

forall L R: Type, forall l: L, forall r: R, Left L <> Right R. 

？

Answer 1

easy策略足以解决此问题：

Inductive DirectSum (L R: Type): Type :=
| Left: L -> DirectSum L R
| Right: R -> DirectSum L R
.
Arguments Left {_ _}.
Arguments Right {_ _}.

Goal forall L R: Type, forall l: L, forall r: R, Left l <> Right r.
easy.
Qed.

这在内部起作用的原因是模式匹配。我们可以编写一个函数，在True上返回Left，在False上返回Right。如果条件相等，我们将得到True = False，这带来了矛盾。