Pattern matching not specialising types

Question

I'm playing around in Coq, trying to create a sorted list. I just wanted a function that takes a list [1,2,3,2,4] and would return something like Sorted [1,2,3,4] - i.e. taking out the bad parts, but not actually sorting the entire list.

I thought I would start by defining a function lesseq of type (m n : nat) -> option (m <= n), and then I could pattern match on that pretty easily. Maybe that's is a bad idea.

The crux of the issue I'm having right now is that (snippet, whole function at bottom)

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
        | 0 => match n with
            | 0 => Some (le_n 0)
            ...

is not typechecking; it says that it's expecting an option (m <= n), but that Some (le_n 0) has type option (0 <= 0). I don't understand, because obviously both m and n are zero in that context, but I've no idea how to tell Coq that.

The entire function is:

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
    | 0 => match n with
        | 0 => Some (le_n 0)
        | S n_  => None
        end
    | S m_  => match n with
        | 0 => None
        | S _   => match lesseq m_ n with
                | Some x=> le_S m n x
                | None  => None
                end
            end
    end.

Perhaps I'm getting ahead of myself and just need to keep reading before I tackle this.

Answer 1

You probably want to define the following function (even if you annotate it properly you [le_S m n x] does not have the type you want) :

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n with
     | 0 =>
         match m with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

But as you've noticed, the typechecker is not clever enough to guess the new context when you destruct a variable appearing in the type of the result. You have to annotate the match in the following way :

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n return (option (m <= n)) with
     | 0 =>
         match m return (option (m <= 0)) with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

See the reference manual if you really want to understand how pattern matching works with dependent types. If you don't feel brave enough for that, you'd rather use tactics mechanisms to build your proof (the "refine" tactic is a great tool for that).

     Definition lesseq m n : option (m <= n).
     refine (fix lesseq (m : nat) (n : nat) {struct n} := _).

     destruct n.
     destruct m.
     apply Some; apply le_n.
     apply None.

     destruct (lesseq m n).
     apply Some.
     apply le_S.
     assumption.
     apply None.
     Defined.

By the way, I don't think your function will be really helpfull (even if it is a good idea), because you will need to prove the following lemma : Lemma lesseq_complete: forall m n, lesseq m n <> None -> m > n.

This is why people use Coq.Arith.Compare_dec. Have fun.

Answer 2

Do you want to write this function as an exercise or only to accomplish your bigger goal? In the latter case you should take a look at the standard library, which is full of decision functions that would do the job here, Coq.Arith.Compare_dec; see for instance le_gt_dec.

Also note that the function you propose would only give you information whether m <= n. For pattern matching the sum type { ... } + { ... } is much more useful, giving you two possible cases to deal with.