Pattern match error

Using Coq
1

I’m implementing an algorithm that translates the lambda calculus to combinators (from the paper “Lambda to ski semantically” by Oleg Kiselyov). I’m still a beginner at Coq, but I have a lot of experience with Haskell where I’ve already implemented the same algorithm with GADTs. Here is the code that is relevant for my issue:

Inductive ski : Type -> Type :=
  si : forall {a}, ski (a -> a)
| sk : forall {b} {a}, ski (a -> b -> a)
| ss : forall {b} {c} {a}, ski ((a -> b -> c) -> (a -> b) -> a -> c)
| sapp : forall {b} {a}, ski (a -> b) -> ski a -> ski b.

Inductive conv : Type -> Type -> Type :=
  cc : forall {ctx} {a}, ski a -> conv ctx a
| cn : forall {b} {ctx} {a}, conv ctx (b -> a) -> conv (ctx * b) a.

Definition amalg {ctx} {a} {b}
   : conv ctx (a -> b) -> conv ctx a -> conv ctx b :=
  fun x y =>
    match x, y with
    | cc d1, cc d2 => cc (sapp d1 d2) (* The error is here *)
    | _, _ => _ (* TODO *)
    end.

This gives the following error message:

In environment
ctx : Type
a : Type
b : Type
x : conv ctx (a -> b)
y : conv ctx a
T : Type
T0 : Type
d1 : ski T0
y0 : conv T a
T1 : Type
T2 : Type
d2 : ski T2
The term "d1" has type "ski T0" while it is expected to have type "ski (?a0@{y0:=y; y:=y0} -> ?b@{y0:=y; y:=y0})".

I would think T0 has to be equal to the function type (a -> b), because we know that cc d1 is a match of x : conv ctx (a -> b) and cc : ski a -> conv ctx a. Why does Coq give this error and how can I fix it?

General advice for improvement of this code is also appreciated.

2

Long story short, when you do a match over an indexed data type that has a partially-concrete index (e.g. a -> b in the type of x), this type gets generalized (notice the T0 : Type that comes out of nowhere), forgetting the knowledge we had.

In order to retain this information, you have to use a dependent pattern-matching, and force the information to be retained using something sometimes referred to as the “convoy pattern”. Here is how it’d look to remember the index of x:

match x in     conv ctx ab
        return (ab = a -> b) -> conv ctx b
with
| cc d1 => fun EQab => (* ... *)
| _     => (* TODO *)
end (Logic.eq_refl (a -> b))

Now, in the cc d1 branch, you’d need to build a conv ctx b, which you’d want to do using sapp, but you’ll find out that in this branch, d1 : conv ctx T0 once again. However, thanks to our convoy, we have access to a proof EQab : T0 = a -> b that will let us use d1 as if it had the right type, again, by convoying it in a dependent pattern-matching over EQab (at this point you can use the induction principle on equality to not write this match yourself).

This is the “hard” way: you will need to start understanding dependent pattern-matching, and this convoy pattern business, which are invaluable, but hard for the beginner!

The “easy” way would be to use the Program library offered by Coq, which does most of this hard work for you. The caveats are: it uses an extra axiom (which is not too much of a worry in most use cases), and it forces you, as far as I know, to write your definition in “proof mode” rather than in “term mode”. In this setting, your proof would start like this:

From Coq Require Import Program.

Definition amalg {ctx} {a} {b}
  : conv ctx (a -> b) -> conv ctx a -> conv ctx b.
  intros x y.
  dependent destruction x.
  dependent destruction y.
  exact (cc (sapp s s0)).

A final downside of this is that it makes your proofs more brittle, because, again AFAIK, you have no control over the names introduced by dependent destruction. So on my computer it’s s and s0, but maybe it’ll be different for you…

Anyway, this s corresponds to your original d1, but you’ll notice that s : ski (a -> b), which is the proper index we wanted, had it not been generalized away! When you finish building the term, you can Print amalg. to see what hacks the library came up with to make this happen: it is not pretty by any means! But it was easy, and worked.

There might be better techniques that I am not aware of. In particular, you might be interested by the Equations library, which tries to help dealing with such annoying pattern matches.

1 Like
3

It does not seem necessary to call Program for the `proof mode’ approach:

Definition amalg {ctx} {a} {b}
   : conv ctx (a -> b) -> conv ctx a -> conv ctx b.
Proof.
intros x y.
inversion_clear x as [c1 ctx1 d1 | c1 ctx1 d1];
inversion_clear y as [c2 ctx2 d2 | c2 ctx2 d2].
- exact (cc (sapp d1 d2)).
[...]
Defined.
4

Thank you for the detailed replies.

Can you explain how to do this or point to some documentation about this. I’ve tried looking at https://coq.inria.fr/library/Coq.Init.Logic.html, but most of those functions seem to deal with value equality and not type equality (e.g. f_equal and eq_rec). I have also tried to manually write the dependent pattern match:

Definition amalg {ctx} {a} {b}
   : conv ctx (a -> b) -> conv ctx a -> conv ctx b :=
  fun x y =>
    match x : conv ctx (a -> b) in conv ctx ab, y : conv ctx a in conv ctx a
        return (ab = (a -> b)) -> conv ctx b
    with
    | cc d1, cc d2 => fun EQab => match EQab with
        eq_refl => cc (sapp d1 d2)
      end
    | _, _     => _ (* TODO *)
    end (Logic.eq_refl (a -> b)).

But that does not work. By the way, is there a syntactic difference between dependent pattern matching and normal pattern matching? Also, what does the in keyword mean? Searching for it in the documentation is very difficult because it is such a common word.

For the proof mode approaches: I am more comfortable with term mode, because Haskell only has term mode. Applying those approaches works for the first case, but the other cases recursively depend on the amalg function itself. So the second case would be: exact (amalg (cc (sapp (sapp (sapp ss (sapp sk ss)) sk) d1) d2) (or something like that, the point is that it uses amalg).

5

Something like this works:

Definition amalg {ctx} {a} {b}
   : conv ctx (a -> b) -> conv ctx a -> conv ctx b :=
  fun x y =>
    match
      x in conv _ ab,
      y in conv _ a'
      return ((a -> b) = ab) -> (a = a') -> conv ctx b
    with
    | cc d1, cc d2 =>
      fun EQab EQaa =>
        match
          EQab in eq _ ab,
          EQaa in eq _ a'
          return ski ab -> ski a' -> conv ctx b with
        | eq_refl, eq_refl => fun d1 d2 => cc (sapp d1 d2)
        end d1 d2
    | _, _     => _ (* TODO *)
    end (Logic.eq_refl (a -> b)) (Logic.eq_refl a).

Of note:

  1. When you case on y, it also loses the fact that its index was a. So I convoyed it too.

  2. I switched the equalities around, from (ab = (a -> b)) to ((a -> b) = ab), so that in the inner match they are in the “nice” order for dependent pattern-matching. If you leave them the other way around, to get the proper elimination, you’d need to match on Logic.eq_sym EQab and Logic.eq_sym EQaa instead. This is due to the fact that the left argument to equality is a type parameter, whereas the right argument is a type index. If you need more info on this, check out my StackOverflow answer on the subject.

  3. In the outer match, I removed ctx from the in clause, so as to not change it in the return type. Speaking of, to answer your question, yes, dependent pattern-matching has a special form, which is an extension of regular pattern matching, and looks like:

match <discriminee>
  as <alias>           (* optional *)
  in <family>          (* optional *)
  return <return type> (* optional *)
with ... end

If you omit the three optional clauses, you end up with a plain old non-dependent pattern-matching (caveat: recent versions of Coq infer some simple dependent pattern matches for you, so it might add them for you!). Usually you’d have the return type, and for it to be interesting, you’d need to bind some variables in either the as clause, the in clause, or both.

The details of dependent pattern matching are available here, though it mentions figures that are nowhere to be found on that page.

And what I meant by using the induction principle on the equality type was to use one of Logic.eq_{rec,rect,ind}, but I ended up writing it up there as a parallel pattern match on both EQab and EQaa.

1 Like
6

Oh, very nice, I assumed wrongly it would not handle this, thanks!

7

Program also lets you use term mode with Program Definition/Program Fixpoint/…
But for what a GADT user wants, I’d honestly recommend installing the Equations plugin.
Or trying out Agda with its agda-mode (in Emacs or Atom at present), since it’s very helpful to write programs interactively and it has good support for dependent pattern matching; OTOH, Agda has other disadvantages compared to Coq.

8

IIRC, a problem with inversion is for recursive functions: you cannot recurse on the terms introduced by inversion, because they’re not recognized as subterms of the input.

Replace Definition by Fixpoint to enable recursive calls (on subterms of the input).
It also works in proof mode, tho tactics will let you perform non-structural recursive calls.

9

I am writing this code as part of a course on Coq and I also would like to learn more about Coq, so I don’t mind doing things the hard way.

I tried this like so:

Fixpoint amalg {ctx} {a} {b}
   : conv ctx (a -> b) -> conv ctx a -> conv ctx b.
Proof.
  ...

But that gives the following error:

Cannot do a fixpoint on a non inductive type.
10

You should provide Fixpoint with a decreasing argument:

Fixpoint amalg {ctx} {a} {b}
   (x : conv ctx (a -> b)) : conv ctx a -> conv ctx b.
Proof.
intros y.
inversion_clear x as [c1 ctx1 d1 | c1 ctx1 ? e1];
inversion_clear y as [c2 ctx2 d2 | c2 ctx2 ? e2].
- exact (cc (sapp d1 d2)).
[...]
Defined.
11

So now I have this:

Fixpoint amalg {ctx} {a} {b}
   (x : conv ctx (a -> b)) (y : conv ctx a) : conv ctx b.
Proof.
inversion x as [c1 ctx1 d1 | c1 ctx1 ? e1];
inversion y as [c2 ctx2 d2 | c2 ctx2 ? e2].
- exact (cc (sapp d1 d2)).
- exact (cn (amalg _ _ _ (cc (sapp sb d1)) e2)).
- exact (cn (amalg _ _ _ (cc (sapp (sapp sc sc) d2)) e1)). 
- exact (cn (amalg _ _ _ (amalg _ _ _ (cc ss) e1) e2)). (* the error is here *)
Defined.

But this gives the following error:

In environment
amalg : forall ctx a b : Type, conv ctx (a -> b) -> conv ctx a -> conv ctx b
ctx : Type
a : Type
b : Type
x : conv ctx (a -> b)
y : conv ctx a
c1 : Type
ctx1 : Type
a0 : Type
e1 : conv ctx1 (c1 -> a -> b)
H : (ctx1 * c1)%type = ctx
H0 : a0 = (a -> b)
c2 : Type
ctx2 : Type
a1 : Type
e2 : conv ctx2 (c2 -> a)
H1 : (ctx2 * c2)%type = ctx
H2 : a1 = a
The term "e2" has type "conv ctx2 (c2 -> a)" while it is expected to have type "conv ctx1 (c1 -> a)".

So I see that H and H1 can be used to prove (ctx1 * c1)%type = (ctx2 * c2)%type, but I don’t know how to prove that this implies that ctx1 = ctx2 and c1 = c2. It looks a lot like pair_equal_spec, but then on the type level. Unfortunately, there seems to be no prod_equal_spec.