Stream: Coq users

Topic: ✔ pattern matching question


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Oct 03 2022 at 01:05):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 01:11):

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.

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 01:14):

@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

view this post on Zulip 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

view this post on Zulip 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 }.

view this post on Zulip Patrick Nicodemus (Oct 03 2022 at 17:00):

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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Oct 03 2022 at 17:02):

Well let me ask one question.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 18:32):

what it can modify is the return type

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 18:48):

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

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Oct 03 2022 at 19:06):

This is helpful thank you

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:14):

and similarly, you must reabstract over ftail before matching on g

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Oct 03 2022 at 19:24):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 03 2022 at 19:48):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Notification Bot (Oct 04 2022 at 05:05):

Patrick Nicodemus has marked this topic as resolved.


Last updated: Jun 17 2024 at 22:01 UTC