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.

Cómo puedo demostrar para todo a y b, que a ≤ b = true -> a ≤ S b = true en Coq.

29 Jul, 2023 Programación

¿Es posible demostrar esto forall (a b : nat), a <=? b = true -> a <=? S b = true en Coq?
Hasta ahora he intentado esto:

Lemma leb0r : forall x, x <=? 0 = true -> x = 0.
  intros. induction x. reflexivity. discriminate H. 
Qed.

Lemma lebS : forall a b, a <=? b = true -> a <=? S b = true.
  intros a b Hab. induction b. apply leb0r in Hab. now rewrite Hab.

Pero aquí me quedé atascado en la hipótesis de inducción:

1 subgoal
a, b : nat
Hab : (a <=? S b) = true
IHb : (a <=? b) = true -> (a <=? S b) = true

========================= (1 / 1)

(a <=? S (S b)) = true

También intenté hacer inducción en "a":

Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
  intros a b Hab. induction a. reflexivity. simpl. destruct b.
  discriminate Hab. simpl in Hab.

1 subgoal
a, b : nat
Hab : (a <=? b) = true
IHa : (a <=? S b) = true -> (a <=? S (S b)) = true

========================= (1 / 1)

(a <=? S b) = true

El problema es que siempre llego a S a <= b o a <= S b y no puedo simplificar eso.

Después de publicar aquí, me di cuenta de que la conclusión de IHa es igual al objetivo del segundo intento y viceversa 🤔

Tags:  

Answer

  1. Avatar for davy.ai
    davy.ai

    Sí, es posible demostrar forall (a b : nat), a <=? b = true -> a <=? S b = true en Coq. Aquí hay una posible demostración:

    Lemma leb_S : forall a b, a <=? b = true -> a <=? S b = true.
Proof.
  intros a b Hab.
  induction a as [|a' IHa'].
  - (* caso base: a = 0 *)
    reflexivity.
  - (* paso de inducción: a = S a' *)
    destruct b as [|b'].
    + (* caso base: b = 0 *)
      discriminate Hab.
    + (* paso de inducción: b = S b' *)
      simpl. apply IHa'. simpl in Hab. apply Hab.
Qed.

    La idea es hacer inducción en a y luego hacer un análisis de casos en b. En el caso base donde a = 0, la conclusión a <=? S b = true se sigue inmediatamente de la reflexividad. En el paso de inducción donde a = S a', asumimos la hipótesis a' <=? b = true (que es la hipótesis de inducción IHa') y necesitamos demostrar que S a' <=? S b = true. Para hacer eso, simplificamos la meta usando simpl y simplificamos la hipótesis Hab usando simpl in Hab. Esto nos permite aplicar IHa' para concluir la prueba. El caso donde b = 0 es descartado por contradicción a partir de Hab, y el caso donde b = S b' se maneja de manera similar al paso de inducción.

Comments are closed.