## Stream: Coq users

### Topic: How to create inductively defined dependent proposition

#### 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 ?

#### 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 [#].
``````

#### 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.

#### 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`.

#### 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...

#### 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 `∀`

#### 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)…

#### 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.

#### walker (Apr 08 2022 at 13:31):

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

Last updated: Oct 05 2023 at 02:01 UTC