Stream: Coq users

Topic: ✔ Stuck with a seemingly simple proof.

view this post on Zulip Notification Bot (Aug 07 2022 at 12:15):

Lessness has marked this topic as resolved.

view this post on Zulip 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.
  exact (match v with vnil _ => eq_refl end).

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

Last updated: Feb 09 2023 at 00:03 UTC