CODEWITHSUNDEEP
coqdependent-typetheorem-proving
simpadjo
simpadjo

Reputation: 4017

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?

Upvotes: 2

Views: 152

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33429

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.

Upvotes: 4

Related Questions