Match patterns of non-specialized types

Question

I play Coq trying to create a sorted list. I just need a function that takes a list of [1,2,3,2,4] and returns something like Sorted [1,2,3,4] - that is, it takes out the bad parts, but does not actually sort the whole list.

I thought I would start by defining a lesseq function like (mn : nat) -> option (m <= n) , and then I could easily combine the template with this. Maybe this is a bad idea.

The essence of the problem that I have right now is that (snippet, the whole function below)

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

typecheck is not checked; he says that he expects option (m <= n) , but that Some (le_n 0) is of type option (0 <= 0) . I do not understand, because it is obvious that both m and n are equal to zero in this context, but I do not know how to tell Coq that.

The whole function:

 Fixpoint lesseq (mn : 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 mnx | None => None end end end. 

Perhaps I am getting ahead of myself and just want to keep reading before doing this.

Answer 1

You probably want to define the following function (even if you annotate it correctly, you [le_S mnx] do not have the type you need):

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

But, as you noticed, typechecker is not smart enough to guess the new context when you destroy the variable that appears in the type of result. You must annotate the match as follows:

  Fixpoint lesseq (mn : 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 mp with | Some l => Some (le_S mpl) | None => None end end. 

See the reference guide if you really want to understand how pattern matching works with dependent types. If you don’t feel brave enough to do this, you will prefer to use tactical mechanisms to create your evidence (refinement tactics are a great tool for this).

  Definition lesseq mn : 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 mn). apply Some. apply le_S. assumption. apply None. Defined. 

By the way, I do not think that your function will be really useful (even if it is a good idea), because you will need to prove the following lemma: Lemma lesseq_complete: forall mn, lesseq mn <> None → m> n.

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

Answer 2

Do you want to write this function as an exercise or just to achieve your larger goal? In the latter case, you should take a look at the standard library, which is full of decision-making functions that would do the work here, Coq.Arith.Compare_dec ; see for example le_gt_dec .

Also note that the function you offer will only give you information m <= n . For pattern matching, the sum type { ... } + { ... } much more useful, which gives you two possible cases.