Hola estoy intentando probar el ejercicio 9 y en una parte tengo algo así
H : (x <=? e) = false
______________________________________(1/1)
e <= x
estuve leyendo https://coq.inria.fr/library/Coq.Arith.Compare_dec.html
pero no doy con la prueba.
Alguna sugerencia?
Al final pude usando:
elim (leb_complete_conv e x); intros.
omega.
De todas formas sigo sin demostrar el total del lemma.
La idea es demostrar:
forall (l:list nat) (x:nat), sorted nat le l -> sorted nat le (insert_sorted x l).
Alguna sugerencia?
con este lemma como axioma o admitido habría demostrado el Ej 9.
En mi mensaje anterior me equivoqué, ya que el negado de <= es > pero se puede probar >=, ya que en realidad vale el mayor.
Saludos, Carlos
Ja Ja. me llego al correo el otro mensaje, no hay problema.
De todas formas sigo intentando probar el lema que menciono antes.
Reescribí la función Insert Sorted (es la que inserta un elemento en una lista de forma ordenada con pre condición, la lista esta ordenada) donde usa en lugar de leBool para comparar, ahora usa match le_gt_dec a b with ... de esta manera omega resuelve un montón de cosas pero estoy teniendo problemas.
Si hago mas o menos lo que esta en el libro, tengo problemas con R que en el ejemplo esta implícito y no es un parámetro como en el nuestro.
Si hago inversion, me aparece en un subGoal una lista l0 de la cual no se nada.
Así que me queda la opción de Inducción, pero bueno, a estas alturas es mas confusión que claridad en mi cabeza y no se por donde encarar.
El problema es opcional así que en el peor caso lo enviamos como admitido.
