Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.
Tengo un sub objetivo que tiene la siguiente forma: ~ (Mi_termino1) < (Mi_termino2) donde Mi_termino1 y Mi_termino2 son ambos números reales. ¿Hay alguna manera de reescribirlo como (Mi_termino1) >= (Mi_termino2)? Intenté usar varias tácticas (especialmente simplificar), pero no puedo encontrar la forma correcta de lograrlo. ¿Alguien tiene alguna idea?
Estoy tratando de aprender cómo demostrar la corrección y optimalidad de los algoritmos. Para ello, estoy tratando de hacerlo para el problema: La entrada es una lista de intervalos ([l1,r1],[l2,r2],…,[ln,rn]) Encuentra la cobertura de intervalos mínima, es decir, la cobertura con la menor cantidad de intervalos que contienen todos los . . . Read more
Si tengo un Teorema de la forma: Teorema my_thm (n: nat -> nat): existe t: nat, n t = 0. Admitido. Si quiero demostrar que para una función tal que my_func 0 = 0, ¿cómo puedo decirle a coq que efectivamente existe dicho t porque mi_func 0 = 0? Esto . . . Read more
Tengo una lista 20 :: 75 :: 123 :: 12 :: nil y me gustaría demostrar que todos los elementos de la lista son mayores o iguales a 10. Entonces lo que hice es crear un Fixpoint para extraer el mínimo de la lista, que es 12, y luego me . . . Read more
Actualmente estoy teniendo dificultades para demostrar este lema: “` Fixpoint select (x: nat) (l: list nat) : nat * list nat := match l with | [] => (x, []) | h :: t => if x <=? h then let (j, l') := select x t in (j, h . . . Read more