walker (Apr 08 2022 at 11:02): 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 [#].
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: Apr 20 2024 at 06:02 UTC