l1<<l2 & l2<<l1 -> l1=l2
Si bien se dijo que deje aquel axioma, me gustaría saber como resolverlo, me hice de los teóricos del año pasado y sigo sin poder probarlo usando inversion.
Nosotros seguimos sin resolver el 17
En respuesta a German Adolfo Faller Farias
Re: Clase de hoy (30/10)
Hola,
Respecto a la pregunta sobre la clase de hoy, a mí me están quedando sin resolver las últimas dos pruebas del ejercicio 17 (la de la igualdad y la de la transitividad).
Saludos,
Noelia.
Hola.
Sobre la ejercicio de la igualdad, valen todos los comentarios previos. No es un ejercicio nada fácil y no hay problemas si éste lo dejan sin hacer.
La prueba de la transitividad de posfijo no es complicada. Para probar l1 << l2 -> l2 << l3 -> l1 << l3 se sugiere hacer inducción en la hipótesis con l2 << l3 (luego de hacer intros). Notar que << es la relación posfijo, que es inductiva.
Saludos, Carlos
Hola.
Como dije, esta es la prueba más difícil del práctico.
Con el axioma auxiliar que propusiste se demuestra, no obstante no pudiste demostrar la propiedad del axioma. Dado que entiendo que esto puede ser educativo, copio abajo código Coq con un encare para dicha prueba, que traslada en realidad el problema de listas a un problema sobre naturales usando librerías de Coq. Incluyo notación y algunos lemas auxiliares que se usan para que los analicen con calma.
No se asusten, una propiedad tan complicada como esta no la tomaremos en un parcial :). Pueden existir otros encares/pruebas mejores o alternativas, obviamente.
Saludos, Carlos
============
Inductive list (X: Set): Set := nil: list X
| cons: X -> list X -> list X.
Notation "x :: xs" := (cons _ x xs).
Notation "[ ]" := (nil _).
Fixpoint length {X: Set} (xs: list X): nat := match xs with
| nil _ => 0
| cons _ x xs' => 1 + length xs'
end.
Fixpoint append {X: Set} (xs ys: list X) {struct xs}: list X
:= match xs with
| nil _ => ys
| cons _ x xs' => x :: append xs' ys
end.
Notation "xs ++ ys" := (append xs ys).
Theorem L4:
forall (A: Set) (l m: list A),
length (l ++ m) = length l + length m.
Proof.
intros A l m.
induction l; simpl; intros.
reflexivity.
rewrite -> IHl.
reflexivity.
Qed.
Require Import Coq.Arith.Arith.
Inductive Postfix (A: Set): list A -> list A -> Prop
:= idPostfix: forall l: list A, Postfix A l l
| strictPostfix:
forall (x: A) (l1 l2: list A),
Postfix A l1 l2 -> Postfix A l1 (x :: l2).
Notation "l1 << l2" := (Postfix _ l1 l2) (at level 65).
Lemma ConsLength:
forall (A: Set) (l1 l2: list A) (x: A),
l2 = x :: l1 -> length l1 < length l2.
Proof.
intros A l1 l2 x HEq.
rewrite -> HEq; auto.
Qed.
Lemma AppendEq:
forall (A: Set) (l1 l2: list A), l2 = l1 ++ l2 -> l1 = [].
Proof.
intros A l1 l2.
case_eq l1.
reflexivity.
simpl; intros x l0 HCase HAppend.
apply ConsLength in HAppend.
rewrite -> L4 in HAppend.
induction (le_not_lt (length l2) (length l0 + length l2)).
apply le_plus_r.
assumption.
Qed.