Stream: Coq users

Topic: Proof without suitable constructor

view this post on Zulip Julin S (Apr 19 2023 at 16:50):

Hi. I got a couple of types like this:

Inductive foo : Type :=
| Foo.

Inductive fooDenote : list nat -> Type :=
| FooDenote: fooDenote nil.

Is it possible to prove this goal?

Goal
  fooDenote (cons 3 nil) -> False.
Proof.

I mean, there is no constructor which can make foo [3] true as it mentions only the case for foo [].

view this post on Zulip Laurent Théry (Apr 19 2023 at 17:16):

Goal
  fooDenote (cons 3 nil) -> False.
Proof.
intros H; inversion H.
Qed.

Last updated: Oct 04 2023 at 23:01 UTC