Stream: Coq users

Topic: How to create inductively defined dependent proposition


view this post on Zulip walker (Apr 08 2022 at 11:02):

Lets say I want to have something like this but for vector of arbitrary size n:

Inductive AllZeros : list nat -> Prop :=
| AllZeros_Empty : AllZeros []
| AllZeros_Cons (l: list nat) (n : nat): n = 0 -> AllZeros l -> AllZeros (n::l).

So This is the minimal error reproducer and I cannot understand the error:

From stdpp Require Import vector.
Inductive AllZeros {n: nat}: (vec nat n) -> Prop :=
| AllZeros_Empty : AllZeros [#].

The error is cannot unify "0" and "n". But this does not make sense ... it looks completely fine because in this case n will be 0.
What am I missing ?

view this post on Zulip Paolo Giarrusso (Apr 08 2022 at 11:29):

Concretely, you want:

Require Import stdpp.vector.
Inductive AllZeros :  {n: nat}, (vec nat n) -> Prop :=
| AllZeros_Empty : AllZeros [#].

view this post on Zulip Paolo Giarrusso (Apr 08 2022 at 11:30):

binding n after the equal makes it an _index_ — that is, it lets different constructors constrain n, which you need here.

view this post on Zulip Paolo Giarrusso (Apr 08 2022 at 11:31):

Binding n before the n, as you did, makes it a parameter (while xs : vec nat n remains an index) — which means that all constructors must be able to produce AllZeros n xs. for some xs.

view this post on Zulip Paolo Giarrusso (Apr 08 2022 at 11:34):

However, beware that vector isn't so convenient to use in Coq. Definition tuple A n := { xs : list A | length xs = n }. works better...

view this post on Zulip walker (Apr 08 2022 at 13:17):

I have one more questions not related to coq, how do you always write those nice looking symbols ? like

view this post on Zulip Paolo Giarrusso (Apr 08 2022 at 13:27):

I have unicode shortcuts in mac/iOS, vscode (and usually in emacs but I must reinstall them)…

view this post on Zulip Paolo Giarrusso (Apr 08 2022 at 13:30):

https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md has extensive docs and configs — only downside is that it’s a bit focused on Iris.

view this post on Zulip walker (Apr 08 2022 at 13:31):

Thanks, It is ok, I am planning to learn iris soon so it is upside (:


Last updated: Jan 27 2023 at 01:03 UTC