Hello!
I am trying to write a map2
for a prodn data type.
Inductive prodn : forall {n : nat}, Vec.t Type n -> Type :=
| nil : prodn []%vector
| cons : forall {A : Type} {n : nat} {v : Vec.t Type n},
A -> prodn v -> prodn (A :: v)%vector.
Derive Signature NoConfusion NoConfusionHom Subterm for t.
Equations map2 :
forall {n : nat} {dom1 : Vec.t Type n} {dom2 : Vec.t Type n} {ran : Vec.t Type n},
prodn (vec_map3 (fun A B C : Type => A -> B -> C) dom1 dom2 ran) ->
prodn dom1 -> prodn dom2 -> prodn ran := {
map2 [] [] [] := [];
map2 (f :: fp) (a :: p1) (b :: p2) := f a b :: map2 fp p1 p2
}.
Where vec_map3
is:
Section Map3.
Import Vec.VectorNotations.
Local Open Scope vector_scope.
Context {A B C D : Type}.
Variable f : A -> B -> C -> D.
Equations vec_map3 :
forall {n : nat}, Vec.t A n -> Vec.t B n -> Vec.t C n -> Vec.t D n := {
vec_map3 [] [] [] := [];
vec_map3 (a :: v1) (b :: v2) (c :: v3) :=
f a b c :: vec_map3 v1 v2 v3
}.
End Map3.
I get the error:
Error:
Unable to build a covering for:
map2 map2 n dom1 dom2 ran t t0 t1
In context:
map2 :
let H := fixproto in
forall (n : nat) (dom1 dom2 ran : Vec.t Type n) (_ : t (vec_map3 (fun A B C : Type => forall (_ : A) (_ : B), C) dom1 dom2 ran)) (_ : t dom1) (_ : t dom2), t ran
n : nat
dom1 : Vec.t Type n
dom2 : Vec.t Type n
ran : Vec.t Type n
t : t (vec_map3 (fun A B C : Type => forall (_ : A) (_ : B), C) dom1 dom2 ran)
t0 : ProdN.t dom1
t1 : ProdN.t dom2
When I try to add more information via:
Equations map2 :
forall {n : nat} {dom1 : Vec.t Type n} {dom2 : Vec.t Type n} {ran : Vec.t Type n},
prodn (vec_map3 (fun A B C : Type => A -> B -> C) dom1 dom2 ran) ->
prodn dom1 -> prodn dom2 -> prodn ran := {
map2 (n := O) (ran := []%vector) [] [] [] := [];
map2 (n := S _) (ran := (_ :: _)%vector) (f :: fp) (a :: p1) (b :: p2) := f a b :: map2 fp p1 p2
}.
It complains:
Error: This pattern must be innaccessible and equal to 0
How do I convince Coq to accept the definition?
Thanks!
Oh, is the last error asking you to mark (n := O) as inaccessible since it's not matched at runtime but deduced? That'd be a dotted pattern in Agda; Equations writes them in ?(pattern) (according to the manual, but not sure how to write that for implicits.
First you can try this with an explicit arg to confirm that's the problem
Equations map2 :
forall {n : nat} {dom1 : Vec.t Type n} {dom2 : Vec.t Type n} {ran : Vec.t Type n},
prodn (vec_map3 (fun A B C : Type => A -> B -> C) dom1 dom2 ran) ->
prodn dom1 -> prodn dom2 -> prodn ran := {
map2 (ran := []) _ _ _ := nil;
map2 (ran := ty :: tys) (cons f fp) (cons a p1) (cons b p2) := cons (f a b) (map2 fp p1 p2)
}.
The above definition works, but you do need Set Equations Transparent
before the vec_map3 definition, otherwise, Equations won't be able to unfold the vec_map3
call once it knows ran is nil or cons. Also there's confusion between the notations for nil and cons for prodn and vec
Last updated: Oct 13 2024 at 01:02 UTC