如何证明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.

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