Stream: Equations devs & users

Topic: Prodn map2


view this post on Zulip Rudy Peterson (Apr 13 2023 at 23:34):

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!

view this post on Zulip Paolo Giarrusso (Apr 14 2023 at 08:00):

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.

view this post on Zulip Paolo Giarrusso (Apr 14 2023 at 08:01):

First you can try this with an explicit arg to confirm that's the problem

view this post on Zulip Matthieu Sozeau (Apr 14 2023 at 09:17):

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