Dependent pattern matching in coq

Question

The following code (which is of course not a complete proof) tries to do pattern matching on a dependent product:

Record fail : Set :=
  mkFail {
      i : nat ;
      f : forall x, x < i -> nat
    }.

Definition failomat : forall (m : nat) (f : forall x, x < m -> nat), nat.
Proof.
  intros.
  apply 0.
Qed.

Function fail_hard_omat fl : nat := failomat (i fl) (f fl).

Definition failhard fl : fail_hard_omat fl = 0.
refine ((fun fl =>
          match fl with
            | mkFail 0 _ => _
            | mkFail (S n) _ => _
          end) fl).

The error I get when trying to execute this is

Toplevel input, characters 0-125:
Error: Illegal application (Type Error): 
The term "mkFail" of type
 "forall i : nat, (forall x : nat, x < i -> nat) -> fail"
cannot be applied to the terms
 "i" : "nat"
 "f0" : "forall x : nat, x < i0 -> nat"
The 2nd term has type "forall x : nat, x < i0 -> nat"
which should be coercible to "forall x : nat, x < i -> nat".

It seems that the substitution somehow does not reach the inner type parameters.

Indeed the match foo with bar construction is not easy to use with dependent type. You will have to explain Coq how the substitution goes with the more complex match foo as bar return bli with blo construction. I'm not sure how to do it correctly right now, I'll give it a try. — Vinz

Vinz Vinz · Accepted Answer · 2014-04-23T07:38:33

After playing with the Program command I managed to build a refine that might suites you, but I don't understand everything I did. The main idea is to help Coq with the substitution by introducing intermediate equalities that will serve as brige within the substitution

    refine ((fun fl =>

    match fl as fl0 return (fl0 = fl -> fail_hard_omat fl0 = 0) with
      | mkFail n bar =>
        match n as n0 return (forall foo: (forall x:nat, x < n0 -> nat), 
           mkFail n0 foo = fl -> fail_hard_omat (mkFail n0 foo) = 0) with 
       | O => _
       | S p => _
       end bar
    end (eq_refl fl) ) fl).

Anyway, I don't know what your purpose here is, but I advise never write dependent match "by hand" and rely on Coq's tactics. In your case, if you define your Definition failomat with Defined. instead of Qed, you will be able to unfold it and you won't need dependent matching.

Hope it helps, V.

Note: both occurences of bar can be replaced by an underscore.

Dependent pattern matching in coq

2 Answers