Как доказать неравенство членов, порожденных двумя разными конструкторами одной и той же индуктивности в 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 tacti c достаточно мощный, чтобы решить эту проблему:

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, что влечет за собой противоречие.