Buenas tardes,
tengo dificultades para poder demostrar el siguiente Theorem:
Theorem ej5_1_5 : forall n m k:nat ,
LE n m /\ LE m k -> LE n k.
Intenté por inducción en n, m ó en las hipótesis que se generan al hacer instros. Sin éxito.
¿Alguna pista de cómo sale?
Mi definición de LE la tengo como sigue:
Inductive LE : nat -> nat -> Prop :=
| Le_O : forall n : nat, LE O n
| Le_S : forall n m : nat, LE n m -> LE (S n) (S m).
Aunque entiendo que también podría definirse , cambiando el segundo caso como:
| Le_S : forall n m : nat, LE n m -> LE n (S m).
De todas maneras, la demo que no me sale y tengo curiosidad de cómo se hace es con la primera definición de LE.
Gracias
Hola Camilo.
Abajo copio una solución.
Respecto a tu comentario: "Le_S : forall n m : nat, LE n m -> LE n (S m)." no permite junto con Le_O definir correctamente la relación. Solo podrías construir: LE O ?.
Una opción posible sería:
Inductive LE : nat -> nat -> Prop :=
| Le_O : forall n : nat, LE n n
| Le_S : forall n m : nat, LE n m -> LE n (S m).
Una posible solución de la tranistiva de LE con tu definición:
Theorem ej5_1_5 : forall n m k:nat , LE n m -> LE m k -> LE n k.
Proof.
induction n; simpl; intros; auto.
constructor.
inversion_clear H in H0.
inversion_clear H0.
constructor.
apply (IHn m0); assumption.
Qed.
Saludos, Carlos