I am having trouble pattern matching, I have consulted the documentation but I do not understand it.

```
Inductive tlist@{u u0} (A : Type) (B : A → A → Type) : A → A → Type :=
tnil : ∀ i : A, tlist B i i
| tcons : ∀ i j k : A, B i j → tlist B j k → tlist B i k.
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k)(g : tlist edges j k) (p : i = j): Type :=
match f with
| tnil => match g with
| tnil => True
| _ => False
end
| @tcons _ _ x y z fhead ftail =>
match g with
| tnil => False
| @tcons _ _ x' y' z' ghead gtail =>
{ q : y = y' &
(Logic.transport (fun t => edges i t) q fhead ≈
Logic.transport_r (fun t => edges t y') p ghead) &
tlist_quiver_equiv k i j ftail gtail q }
end
end.
```

when I try to run this code I get the error

`The term "fhead" has type "edges x y" while it is expected to have type "edges i y". `

I get what's happening here but since we are matching against `f`

of type `tlist edges i j`

and the constructor is `tcons`

it must be the case that `x=i`

in this branch. Is there a way I can annotate the match statement with an "in" clause or a "return clause" so that this identification is performed automatically?

I tried to read the docs on 'in ' and 'as' clauses in pattern matching but i can't make sense of how they help me here.

I can build a similar term in the proof environment using tactics, the 'induction' tactic does this automatically when I call it on H. But the term thus constructed is ungainly.

First, have you considered using Coq-Equations rather than writing dependent pattern matches by hand? Coq-Equations would understand that `x = i`

automatically.

That is a great place for me to start, I think

otherwise,

```
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k)(g : tlist edges j k) (p : i = j): Type
Proof.
destruct f. Show Proof.
```

should show the right annotations — I'd try myself, but your example isn't self-contained and I don't know how to fix it

Ok, let me try to understand this

```
(λ (k i j : G) (f : tlist edges i k) (g : tlist edges j k) (p : i = j),
match f in (tlist _ a y) return (tlist edges j y → a = j → Type) with
| @tnil _ _ i0 =>
(λ (i1 : G) (g0 : tlist edges j i1) (p0 : i1 = j), ?Goal@{i:=i1; g:=g0; p:=p0}) i0
| @tcons _ _ i0 j0 k0 b t =>
(λ (i1 j1 k1 : G) (e : edges i1 j1) (f0 : tlist edges j1 k1) (g0 : tlist edges j k1)
(p0 : i1 = j), ?Goal0@{i:=i1; j0:=j1; k:=k1; f:=f0; g:=g0; p:=p0}) i0 j0 k0 b t
end g p)
```

okay I have a minimization, that gives sth close to what you show:

```
Require Import Utf8.
Inductive tlist {A : Type} (B : A → A → Type) : A → A → Type :=
| tnil : ∀ i : A, tlist B i i
| tcons : ∀ i j k : A, B i j → tlist B j k → tlist B i k.
Axiom G : Type.
Axiom edges : G -> G -> Type.
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k)(g : tlist edges j k) (p : i = j): Type.
Proof.
destruct f. Show Proof.
```

@Patrick Nicodemus googling for "Coq convoy pattern" will find some material. But the key idea is that the match only changes the _return type_, so if you want to change the type of some variable in the context, you must pass it to the match as a function argument

hence the `match f in (tlist _ a y) return (tlist edges j y → a = j → Type) with ... end g p`

part

Hi @Paolo Giarrusso , thank you for your help last night. I am looking at this again with fresh eyes this morning and I found Adam Chlipala's book has a chapter that discusses the convoy pattern.

Here is a self contained version of my thing from last night.

```
Class Quiver := {
nodes :> Type;
edges : nodes -> nodes -> Type
}.
Coercion nodes : Quiver >-> Sortclass.
Context (G : Quiver).
Equations tlist_quiver_equiv (k i j : G)
(f : tlist edges i k) (g : tlist edges j k) ( p : i = j) : Type :=
tlist_quiver_equiv k k k tnil tnil eq_refl := True ;
tlist_quiver_equiv _ _ _ _ tnil _ := False ;
tlist_quiver_equiv _ _ _ tnil _ _ := False ;
tlist_quiver_equiv k i j (@tcons _ _ _ i' _ fhead ftail) (@tcons _ _ _ j' _ ghead gtail) p :=
{ q : i' = j' &
(Logic.transport (fun t => edges i t) q fhead =
Logic.transport_r (fun t => edges t j') p ghead) &
tlist_quiver_equiv k i' j' ftail gtail q }.
```

This is the proof term I get from Equations

```
tlist_quiver_equiv@{u} =
fix tlist_quiver_equiv
(k i j : G) (f : tlist edges i k) (g : tlist edges j k) (p : i = j) {struct f} : Type :=
match f in (tlist _ n n0) return (∀ j0 : G, tlist edges j0 n0 → n = j0 → Type) with
| @tnil _ _ i0 =>
λ (j0 : G) (g0 : tlist edges j0 i0) (p0 : i0 = j0),
match g0 in (tlist _ n n0) return (n0 = n → Type) with
| @tnil _ _ i1 =>
λ p1 : i1 = i1,
match p1 in (_ = n) return (n = i1 → Type) with
| eq_refl => λ _ : i1 = i1, True
end eq_refl
| @tcons _ _ i1 _ k0 _ _ => λ _ : k0 = i1, False
end p0
| @tcons _ _ i0 j0 k0 e t =>
λ (j1 : G) (g0 : tlist edges j1 k0) (p0 : i0 = j1),
match
g0 in (tlist _ n n0)
return (∀ i1 j2 : G, edges i1 j2 → tlist edges j2 n0 → i1 = n → Type)
with
| @tnil _ _ i1 =>
λ (i2 j2 : G) (_ : edges i2 j2) (_ : tlist edges j2 i1) (_ : i2 = i1), False
| @tcons _ _ i1 j2 k1 e0 t0 =>
λ (i2 j3 : G) (e1 : edges i2 j3) (t1 : tlist edges j3 k1) (p1 : i2 = i1),
{q : j3 = j2 &
Logic.transport (λ t2 : G, edges i2 t2) q e1 =
Logic.transport_r (λ t2 : G, edges t2 j2) p1 e0 & tlist_quiver_equiv k1 j3 j2 t1 t0 q}
end i0 j0 e t p0
end j g p
: ∀ k i j : G, tlist edges i k → tlist edges j k → i = j → Type
```

and I am trying to understand how this works.

I don't have a question right now I think I still need time to digest this

Well let me ask one question.

```
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k) (g : tlist edges j k) : forall ( p : i = j), Type :=
match f with
| tnil =>
match g with
| tnil => fun _ => True
| _ => fun _ => False
end
| @tcons _ _ i0 i1 k0 fhead ftail =>
( match g in tlist _ j0 k0
return (edges i0 i1) -> (tlist edges i1 k0) -> (i0 = j0) -> Type with
| tnil => fun _ _ _ => False
| @tcons _ _ j0 j1 k1 ghead gtail =>
fun fhead' ftail' =>
fun (p' : i0 = j0) =>
{ q : i1 = j1 &
(Logic.transport (fun t => edges i0 t) q fhead' =
Logic.transport_r (fun t => edges t j1) p' ghead) &
tlist_quiver_equiv k0 i1 j1 ftail' gtail q }
end ) fhead ftail
end.
```

This is the function I was trying to write to solve this problem.

The error I get is ```
The term "ftail'" has type "tlist edges i1 k1" while it is expected to have type
"tlist edges i1 k0".
```

Again I think I understand what's happening here, the problem is that when I pattern match on `g`

it introduces the new variable `k1`

and the system doesn't know to identify `k0`

and `k1`

. I am trying to figure out how to use the convoy pattern here but I have not figured it out yet.

first of all, I think https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/pattern.20matching.20question/near/301987131 should answer "how to use convoy" here — `destruct`

generates the right code

second, the basic answer is Coq is not going to learn that two existing variables are definitionally equal — a match does not modify the context

what it can modify is the return type

since I don't have `Logic.transport_r`

(your "self-contained examples" really aren't), here's a partial version:

```
Axiom TODO : ∀ A, A.
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k)(g : tlist edges j k) (p : i = j): Type.
Proof.
destruct f.
- destruct g.
+ apply True.
+ apply False.
- destruct g.
+ apply False.
+ apply TODO.
Qed.
```

gives

```
tlist_quiver_equiv =
fix tlist_quiver_equiv
(k i j : G) (f : tlist edges i k) (g : tlist edges j k)
(p : i = j) {struct f} : Type :=
match f in (tlist _ y y0) return (tlist edges j y0 → y = j → Type) with
| tnil _ i0 =>
(λ (i1 : G) (g0 : tlist edges j i1) (p0 : i1 = j),
match g0 in (tlist _ y y0) return (y0 = y → Type) with
| tnil _ i2 => (λ (i3 : G) (_ : i3 = i3), True) i2
| tcons _ i2 j0 k0 b t =>
(λ (i3 j1 k1 : G) (_ : edges i3 j1) (_ : tlist edges j1 k1)
(_ : k1 = i3), False) i2 j0 k0 b t
end p0) i0
| tcons _ i0 j0 k0 b t =>
(λ (i1 j1 k1 : G) (_ : edges i1 j1) (f0 : tlist edges j1 k1)
(g0 : tlist edges j k1) (p0 : i1 = j),
match
g0 in (tlist _ y y0) return (tlist edges j1 y0 → i1 = y → Type)
with
| tnil _ i2 =>
(λ (i3 : G) (_ : tlist edges j1 i3) (_ : i1 = i3), False) i2
| tcons _ i2 j2 k2 b0 t0 =>
(λ (i3 j3 k3 : G) (_ : edges i3 j3) (_ : tlist edges j3 k3)
(_ : tlist edges j1 k3) (_ : i1 = i3),
TODO Type) i2 j2 k2 b0 t0
end f0 p0) i0 j0 k0 b t
end g p
: ∀ k i j : G, tlist edges i k → tlist edges j k → i = j → Type
Arguments tlist_quiver_equiv k i j f g p
```

(status: I'm simplifying that by hand to remove unneeded abstractions)

Sorry it's not self contained I thought that function was from the standard library my bad.

This is helpful thank you

I'm still making progress, but let me add one thing I figured: when you match `f : tlist edges i k`

against `tcons`

, this is going to bind a copy of `k`

(because that's an index to `tlist`

) — that already works better if you reabstract over `g`

and similarly, you must reabstract over `ftail`

before matching on `g`

e.g. from the output of

```
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k)(g : tlist edges j k) (p : i = j): Type.
Proof.
destruct f as [|x y z fhead ftail].
- destruct g.
+ apply True.
+ apply False.
- destruct g as [|x' y' z' ghead gtail].
+ apply False.
+ eapply ({ q : y = y' & tlist_quiver_equiv _ _ _ ftail gtail q}).
Qed.
```

I could get down to

```
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k) (g : tlist edges j k) (p : i = j) {struct f} : Type :=
match f in tlist _ y y0 return tlist edges j y0 → y = j → Type with
| tnil _ _ => λ _ _,
match g with
| tnil _ _ => True
| tcons _ _ _ _ _ _ => False
end
| tcons _ x y z fhead ftail =>
λ (g0 : tlist edges j z) (p0 : x = j),
match g0 in tlist _ y0 y1 return tlist edges y y1 → x = y0 → Type with
| tnil _ _ => fun _ _ => False
| tcons _ x' y' z' ghead gtail =>
λ (ftail0 : tlist edges y z') (_ : x = x'),
{q : y = y' & tlist_quiver_equiv z' y y' ftail0 gtail q}
end ftail p0
end g p.
```

but then I can't avoid reabstracting `g`

or `ftail`

Oh by the way that Logic.transport function is from Equations.Prop.

I'm still wrapping my brain around how the convoy pattern works but i'm getting there

here's one example: when you match `f`

against `tcons _ x y z fhead ftail`

, the matching rule makes `y0`

equal to `z`

— this works on `y0`

because it's not bound in context, but only bound by the return annotation, and this modifies the return type...

here `tlist edges j y0 → y = j → Type`

becomes `tlist edges j z -> x = j -> Type`

, which affects the type of `g0`

.

and indeed, replacing `match g0`

with `match g`

gives immediately an error, showing that `g`

kept its type

however, I'm mostly answering "how do you know what must be reabstracted" :sweat_smile:

```
Fixpoint tlist_quiver_equiv (k i j : G)
(f : tlist edges i k) (g : tlist edges j k) ( p : i = j ) : Type :=
match f in (tlist _ i_t k0) return (tlist edges j k0) -> i_t = j -> Type with
| tnil => fun g' _ => match g' with
| tnil => True
| _ => False
end
| @tcons _ _ i0 i1 k1 fhead ftail =>
fun g' : tlist edges j k1 => fun p => True
end g p.
```

So this code type checks and I'm trying to understand why this works. As you said, Coq does not learn two existing variables are definitionally equal. I am trying to understand how `k,k0, k1`

are all "unified" here. I get that since `f`

is of type `tlist edges j k`

, Coq knows to set ``k0 :=k`

, and this is why the body of the match accepts `g`

as an argument to the function. But how does it match up `k0`

with `k1`

so that it knows that the body of the `tcons`

branch is of the right type?

the type of `@tcons _ _ i0 i1 k1 fhead ftail`

is `tlist edges i0 k1`

so the branch must have type `(tlist edges j k0) -> i_t = j -> Type`

substituting `k0 := k1`

and `i_t := i0`

, ie `(tlist edges j k1) -> i0 = j -> Type`

Thank you, this is helpful, and so is Adam Chlipala's *MoreDep* chapter. I don't fully get it yet but I'm getting there.

if this works similarly to Agda, I'd expect the key trick is that Coq unifies pattern type `tlist edges i0 k1`

against the type of the scrutinee `f : tlist edges i_t k0`

, and that's how it deduces `i_t := i0`

and `k0 := k1`

?

Yeah this is something like what Adam Chlipala's book says. I think I understand this definition well enough to move on now.

Patrick Nicodemus has marked this topic as resolved.

Last updated: Jun 17 2024 at 22:01 UTC