CODEWITHSUNDEEP
coq
Iva Kam
Iva Kam

Reputation: 962

How to prove non-equality of terms produced by two different constructors of the same inductive in coq?

Consider I have an inductive: 

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

How do I prove that 

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

?

Upvotes: 0

Views: 31

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

The easy tactic is powerful enough to solve this:

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.

The reason this works, internally, is pattern matching. We can write a function that returns True on Left and False on Right. If the terms were equal, we would get True = False, which entails a contradiction.

Upvotes: 1

Related Questions