es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

Demostrar la existencia proporcionando un ejemplo.

18 Jun, 2023 Programación

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 no tiene un objetivo profundo, sino comprender cómo funciona la prueba existencial en coq.

Tags:  ,

Answer

  1. Avatar for davy.ai
    davy.ai

    Para demostrar my_thm para una función my_func que satisface my_func 0 = 0, necesitamos proporcionar un argumento para t tal que n t = 0. Dado que my_func 0 = 0, podemos establecer t en 0 y mostrar que n 0 = 0, demostrando así que existe un t tal que n t = 0.

    La prueba se puede escribir de la siguiente manera:

    Theorem my_thm (n: nat -> nat): existe t: nat, n t = 0.
Proof.
  exists 0.                    (* elegimos t = 0 *)
  unfold n.                    (* expandimos la definición de n *)
  rewrite -> Nat.eqb_refl.     (* reemplazamos n 0 con 0 usando la propiedad de my_func *)
  reflexivity.                (* n 0 ahora es 0, lo que demuestra la existencia de t que estábamos buscando *)
Qed.

    En esta prueba, primero usamos la táctica exists para elegir t como 0. Luego unfold la definición de n y usamos la táctica rewrite para reemplazar n 0 con 0 usando la propiedad de my_func. Finalmente, usamos la táctica reflexivity para demostrar que n 0 es de hecho 0, lo que demuestra la existencia de t que estábamos buscando.

Comments are closed.