Arbitrary types in Dependent Pattern Matching

Using Coq
1

Consider the following example of length indexed list, taken from CPDT

Section ilist.
  Variable A : Set.

  Inductive ilist : nat -> Set :=
  | Nil : ilist O
  | Cons : forall n, A -> ilist n -> ilist (S n).

  Definition hd n (ls: ilist (S n)): A :=
    match ls in (ilist n') return match n' with
                                  | O => unit
                                  | S n'' => A
                                  end with
      | Nil => tt
      | Cons h hs => h
    end.

In the case for hd Nil it’s type is unit, and unit is not A, so why does Coq accept this definition? I know Nil is unreachable in this case, but what exactly is going under the hood for Coq to allow a branch to have an arbitrary type?

1 Like
2

So you know that ls: ilist (S n) and the in (ilist n') annotation just binds S n to the identifier n'. This means that

return match n' with
| O => unit
| S n'' => A
end

is the same as

return match S n with
| O => unit
| S n'' => A
end

which in its turn is the same as just return A. Hence the type A we required as the output type of hd is still A.

Then why go through all that trouble of expanding the return type? This is needed because Coq will substitute the index n' with O and S n0 in the Nil and Cons branches of the match ls ...-expression. And in the case of Nil branch n' is O, so the return type inside the Nil branch is going to be

return match O with
| O => unit
| S n'' => A
end

i.e. unit.

Had we not mentioned n' anywhere in the return type, the substitution would be vacuous and the return type would stay the same in both branches, leading to impossible to solve Nil branch.

1 Like
3

So basically if we are type checking Definition t x : A := match x return T with ... it first normalize T and then check if it matches A?

4

More precisely, Coq first substitutes the parameters of the inductive type of x into T. Then, it checks if types A and T are convertible. Normalization is one way of checking convertibility, but it is kind of a last resort, if all the other heuristics failed.

2 Likes
5

Can you give me a list of heuristics applied in this case?

6

Since A is an atomic term, no heuristic applies in this case. So, Coq just computes the weak head normal form of match S n' with ... end, which is A.

Heuristics matter when Coq is comparing definitions or applications. For example, if Coq is comparing the applications a b and c d, it will first check whether a and c (resp. b and d) are convertible. If they are, no need to normalize anything.

1 Like
7

What about when T is a product forall foo: bar, T'? Does it first perform a beta reduction on any application after the match?

For example:

Definition hd' n (ls: ilist (S n)): A :=
    match ls in (ilist n') return (n' = S n) -> A with
      | Nil => fun eq => False_rect A (PeanoNat.Nat.neq_succ_0 n (eq_sym eq))
      | Cons h hs => fun _ => h
    end eq_refl.
8

Never mind, I just noticed that in this case the type checker will consider the whole body of the function, and in this case it is an application.

9

Just my personal opinion, but; on complicated cases of dependent pattern matching, i think it’s simpler to understand what’s going on with eliminators instead. Don’t get me wrong, i like “match” as a construct, but dependent matching mixes too much stuff, i feel. For example, an earlier reply was talking about how “Coq first substitutes the parameters of the inductive type of x into T”: using an eliminator makes it clear this isn’t some sort of specific mechanism to pattern matching, it’s just regular function application.

Take the " hd’ " function you posted, for instance. With an eliminator, its definition looks like :

  Definition hd'_alt (n:nat) (ls : ilist (S n)) : A := 
  @ilist_rec (fun n' _ => n' = S n -> A)
   (fun eq => False_rect A (PeanoNat.Nat.neq_succ_0 n (eq_sym eq)))
   (fun m h hs _ => (fun _ => h))
   (S n) ls eq_refl.

At first glance, this is a mouthful no one would be advised to write, but: you can define it partially. For example, you can check that

Definition hd'_start (n:nat) :
((0 = S n) -> A) ->
(forall m (h:A) hs, ((m = S n) -> A) -> (S m = S n) -> A) ->
forall i, ilist i -> i = S n -> A
:= @ilist_rec (fun n' _ => n' = S n -> A).

…and from there it’s a matter of filling holes. Proof mode makes this task simpler, of course.

10

I agree, dependent pattern matching is still something I don’t think we got quite right yet. This makes me excited about the Equations plugin, for example. My only complaint is that I believe match expressions are superior to equations because they live in the expression level, meaning that you have a much higher freedom to make a case analysis anywhere in your code.