Search code examples
coqdependent-typetheorem-proving

Coq: prove that an inductive type w/o a non-recursive constructor is uninhabitated

I'm new to Coq an its underlying theory. Suppose there is an inductive type which have no non-recursive constructors. It's impossible to produce an instance of it. But could it be proven?

Inductive impossible : Type :=
  | mk (x : impossible).

Theorem indeed_impossible : forall (x : impossible), False.

If no - is it a drawback of Coq or a feature of CoC?

Solution

  • This is easily proved by induction on x. You only get an inductive step with an absurd induction hypothesis, and no base case which would require you to actually produce an absurdity.

    Theorem indeed_impossible : forall (x : impossible), False.
Proof.
  induction 1.
  (* just need to show [False |- False] *)
  trivial.
Qed.

    Edit by: @simpadjo: Alternative proof which is more clear for me personally:

    Theorem indeed_impossible : forall (x : impossible), False.
Proof.
 intros. induction x. assumption. Qed.