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: Dec 05 2023 at 09:01 UTC