Patrick Nicodemus (Oct 03 2022 at 00:36): Patrick Nicodemus (Oct 03 2022 at 00:36):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.
Paolo Giarrusso (Oct 03 2022 at 01:03):First, have you considered using Coq-Equations rather than writing dependent pattern matches by hand? Coq-Equations would understand that x = i automatically.
Patrick Nicodemus (Oct 03 2022 at 01:05):That is a great place for me to start, I think
Paolo Giarrusso (Oct 03 2022 at 01:08):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
Patrick Nicodemus (Oct 03 2022 at 01:10):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
Paolo Giarrusso (Oct 03 2022 at 01:15):hence the match f in (tlist _ a y) return (tlist edges j y → a = j → Type) with ... end g p part
Patrick Nicodemus (Oct 03 2022 at 16:59):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.
Patrick Nicodemus (Oct 03 2022 at 17:00):I don't have a question right now I think I still need time to digest this
Patrick Nicodemus (Oct 03 2022 at 17:02):Well let me ask one question.
Patrick Nicodemus (Oct 03 2022 at 17:03): 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.
Patrick Nicodemus (Oct 03 2022 at 17:04):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".
Patrick Nicodemus (Oct 03 2022 at 17:07):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.
Paolo Giarrusso (Oct 03 2022 at 18:31):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
Paolo Giarrusso (Oct 03 2022 at 18:31):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
Paolo Giarrusso (Oct 03 2022 at 18:32):what it can modify is the return type
Paolo Giarrusso (Oct 03 2022 at 18:40):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)
Patrick Nicodemus (Oct 03 2022 at 19:06):Sorry it's not self contained I thought that function was from the standard library my bad.
Patrick Nicodemus (Oct 03 2022 at 19:06):This is helpful thank you
Paolo Giarrusso (Oct 03 2022 at 19:10):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
Paolo Giarrusso (Oct 03 2022 at 19:14):and similarly, you must reabstract over ftail before matching on g
Paolo Giarrusso (Oct 03 2022 at 19:17):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
Patrick Nicodemus (Oct 03 2022 at 19:24):Oh by the way that Logic.transport function is from Equations.Prop.
Patrick Nicodemus (Oct 03 2022 at 19:39):I'm still wrapping my brain around how the convoy pattern works but i'm getting there
Paolo Giarrusso (Oct 03 2022 at 19:47):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.
Paolo Giarrusso (Oct 03 2022 at 19:47):and indeed, replacing match g0 with match g gives immediately an error, showing that g kept its type
Paolo Giarrusso (Oct 03 2022 at 19:48):however, I'm mostly answering "how do you know what must be reabstracted" :sweat_smile:
Patrick Nicodemus (Oct 03 2022 at 20:45): 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?
Gaëtan Gilbert (Oct 03 2022 at 20:52):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
Patrick Nicodemus (Oct 03 2022 at 21:25):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.
Paolo Giarrusso (Oct 03 2022 at 21:43):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?
Patrick Nicodemus (Oct 04 2022 at 05:04):Yeah this is something like what Adam Chlipala's book says. I think I understand this definition well enough to move on now.
Notification Bot (Oct 04 2022 at 05:05):Patrick Nicodemus has marked this topic as resolved.
Last updated: Apr 20 2024 at 13:01 UTC