2

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?

Improve this question

1 Answer 1

Reset to default
4

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.
Improve this answer
5
  • Thank you. I tried to apply inversion and it of course got me nowhere.
    – simpadjo
    Commented May 11, 2019 at 21:51
  • @HTNW thank you for providing the proof script. I proved it a bit differently (see my edits). Could you please explain what does induction 1 mean?
    – simpadjo
    Commented May 12, 2019 at 7:24
  • Hm, my edit is not yet visible because it requires peer review. Here is the proof: intros. induction x. assumption. Qed.
    – simpadjo
    Commented May 12, 2019 at 7:26
  • 1
    @simpadjo induction 1 is the same as intros x. induction x with a fresh name x. trivial is a variant of auto, except it tries even less to solve the goal. auto always checks for assumptions first. Here's the documentation.
    – HTNW
    Commented May 12, 2019 at 8:13
  • Actually, now that I think about it, you can just say now induction 1.
    – HTNW
    Commented May 12, 2019 at 8:22

Not the answer you're looking for? Browse other questions tagged or ask your own question.