## Stream: Coq users

### Topic: ✔ Stuck with a seemingly simple proof.

#### Lessness (Aug 07 2022 at 09:49):

``````Inductive vector A: nat -> Type :=
| vnil: vector A 0
| vcons: forall (n: nat), A -> vector A n -> vector A (S n).

Theorem test A (v: vector A 0): v = vnil A.
Proof.
``````

#### Gaëtan Gilbert (Aug 07 2022 at 10:03):

``````  set (n := 0) in v.
change (match n return vector A n -> Prop with
| 0 => fun v => v = vnil A
| S _ => fun _ => True
end v).
destruct v;trivial.
``````

#### Lessness (Aug 07 2022 at 10:08):

Thank you very much!

#### Yann Leray (Aug 07 2022 at 10:20):

You can even let Coq fill in the `S _` case with something like `exact (match v in vector _ 0 => vnil _ => eq_refl end).`

#### Notification Bot (Aug 07 2022 at 12:15):

Lessness has marked this topic as resolved.

#### Malcolm Sharpe (Aug 08 2022 at 07:07):

Turns out even the `in` is not needed, so it comes out to the remarkably concise:

``````Inductive vector A: nat -> Type :=
| vnil: vector A 0
| vcons: forall (n: nat), A -> vector A n -> vector A (S n).

Theorem test A (v: vector A 0): v = vnil A.
Proof.
exact (match v with vnil _ => eq_refl end).
Qed.
``````

(I'm just a beginner, so I'm still working on understanding why this works...)

Last updated: Jun 14 2024 at 19:02 UTC