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.

友情链接