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.

Answer 1

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.

Answer 2

Another, slightly less involved, alternative is to use nat and fail's induction combinators.

Print nat_rect.
Print fail_rect.

Definition failhard : forall fl, fail_hard_omat fl = 0.
Proof.
refine (fail_rect _ _). (* Performs induction (projection) on fl. *)
refine (nat_rect _ _ _). (* Performs induction on fl's first component. *)
Show Proof.