Coincidencia de patrones no especializados

Question

Estoy jugando en Coq, tratando de crear una lista ordenada. Solo quería una función que tomara una lista [1,2,3,2,4] y devolviera algo como Sorted [1,2,3,4] - es decir, eliminar las partes defectuosas, pero no ordenar realmente la lista completa.

Pensé que comenzaría definiendo una función lesseq de tipo , y luego podría hacer coincidir el patrón fácilmente. Tal vez esa es una mala idea.

El quid de la cuestión que estoy teniendo ahora mismo es que (fragmento, toda la función en la parte inferior)

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

no está verificación de tipos; dice que está esperando un option (m <= n), pero que Some (le_n 0) tiene el tipo option (0 <= 0). No entiendo, porque obviamente ambos m y n son cero en ese contexto, pero no tengo idea de cómo decirle eso a Coq.

La función entera es:

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. 

Tal vez me estoy adelantando a mí mismo y sólo hay que seguir leyendo antes de hacer frente a este.

Answer 1

Es posible que desee para definir la siguiente función (incluso si anotarla correctamente [le_S mnx] no tiene el tipo que desee):

 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. 

Pero como se ha notado, la typechecker es no es lo suficientemente inteligente como para adivinar el nuevo contexto cuando destruye una variable que aparece en el tipo del resultado . Usted tiene que realizar anotaciones en el partido de la siguiente manera:

 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. 

Consulte el manual de referencia si realmente quiere entender cómo el patrón coincidente trabaja con tipos dependientes. Si no te sientes lo suficientemente valiente para eso, preferirías usar mecanismos tácticos para construir tu prueba (la táctica de "refinar" es una gran herramienta para eso).

 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. 

Por cierto, no creo que su función será muy servicial (incluso si es una buena idea), ya que necesitará para probar la siguiente lema: Lema lesseq_complete: forall mn, lesseq mn <> Ninguno -> m> n.

Es por esto que las personas usan Coq.Arith.Compare_dec. Diviértete.

Answer 2

¿Desea escribir esta función como un ejercicio o solo para lograr su objetivo más grande? En este último caso, debería echar un vistazo a la biblioteca estándar, que está llena de funciones de decisión que harían el trabajo aquí, Coq.Arith.Compare_dec; ver por ejemplo le_gt_dec.

También tenga en cuenta que la función que propone solo le proporcionará información ya sea . Para la coincidencia de patrones, el tipo de suma { ... } + { ... } es mucho más útil, lo que le da dos posibles casos para tratar.