How to reason with complex pattern-matchings?

Question

Coq allows to write complex pattern-matchings, but then it decomposes them so that its kernel can handle them.

For instance, let us consider the following code.

Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Definition f (l : list bar) :=
  match l with
  | _ :: A :: _ => 1
  | _ => 2
  end.

We pattern-match both on the list and on the second element. Printing f shows that Coq stores a more complex version of it.

Print f.
(* f = fun l : list bar => match l with
                        | [] => 2
                        | [_] => 2
                        | _ :: A :: _ => 1
                        | _ :: B :: _ => 2
                        | _ :: C :: _ => 2
                        end
     : list bar -> nat
*)

The problem is that, in the proofs manipulating f, I have to deal with 5 cases instead of only 2, and 4 of them are redundant.

What is the best way to deal with this? Is there a way to reason with the pattern-matching as if it were exactly as defined?

Answer 1

You are correct in that Coq actually simplifies pattern-matching making a lot of redundancies appear. There are however some ways to reason on the case analysis you meant opposed to what Coq understands.

• Using Function and function induction is a way.
• More recently, Equations also allows you to define pattern-matching for which it derives induction principles automatically (that you can invoke using funelim). In order to convince coq cases can be factorised you have to use the notion of view. They are described in the context of Equations in the examples. I'll detail how to adapt your example to it.

From Equations Require Import Equations.
Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Equations discr (b : list bar) : Prop :=
  discr (_ :: A :: _) := False ;
  discr _ := True.

Inductive view : list bar -> Set :=
| view_foo : forall x y, view (x :: A :: y)
| view_other : forall l, discr l -> view l.

Equations viewc l : view l :=
    viewc (x :: A :: y) := view_foo x y ;
    viewc l := view_other l I.

Equations f (l : list bar) : nat :=
    f l with viewc l := {
    | view_foo _ _ => 1 ;
    | view_other _ _ => 2
    }.

Goal forall l, f l < 3.
Proof.
    intro l.
    funelim (f l).
    - repeat constructor.
    - repeat constructor.
Qed.

As you can see, funelim only generates two subgoals.

It can be a bit heavy so if you don't want to use Equations of Function, you might have to prove your own induction principles by hand:

Require Import List. Import ListNotations.

Inductive bar := A | B | C.

Definition f (l : list bar) :=
  match l with
  | _ :: A :: _ => 1
  | _ => 2
  end.

Definition discr (l : list bar) : Prop :=
    match l with
    | _ :: A :: _ => False
    | _ => True
    end.

Lemma f_ind :
    forall (P : list bar -> nat -> Prop),
        (forall x y, P (x :: A :: y) 1) ->
        (forall l, discr l -> P l 2) ->
        forall l, P l (f l).
Proof.
    intros P h1 h2 l.
    destruct l as [| x [|[] l]].
    3: eapply h1.
    all: eapply h2.
    all: exact I.
Qed.

Goal forall l, f l < 3.
Proof.
    intro l.
    eapply f_ind.
    - intros. repeat constructor.
    - intros. repeat constructor.
Qed.