Antecedentes
Estoy aprendiendo asistencia, Coq, por mi cuenta. Hasta ahora, he terminado de leer Coq de Yves Bertot a toda prisa . Ahora, mi objetivo es probar algunos resultados básicos con respecto a los números naturales, que culminan con el llamado algoritmo de división. Sin embargo, he encontrado algunos contratiempos en mi camino hacia ese objetivo. En particular, los dos resultados siguientes han demostrado (juego de palabras) ser más difíciles de probar en Coq de lo que inicialmente imaginé. De hecho, después de muchos intentos infructuosos, he recurrido a probarlos a mano (como se muestra a continuación). Claramente, esto no me ayuda a ser más competente en el manejo de Coq; Por eso me dirijo a este foro. Mi esperanza es que alguien en este sitio pueda y quierapara ayudarme a traducir mis pruebas a continuación en una prueba que Coq acepta. Toda ayuda es sinceramente apreciada!
Teorema A
Para todo x < S ( y ) ⊂ x < y ∨ I ( N , x , y ) Prueba:
Supongamos que . Por lo tanto, hay una z ∈ N con I ( N , x + S ( z ) , S ( y ) ) Por lo tanto, por (Peano 1b y 3) I ( N , x + z , y )
Definir un predicado
Es suficiente mostrar . Probamos esto por inducción en z . Para ver Q ( 0 ) , no ethat si I ( N , x + 0 , y ) se cumple, entonces I ( N , x , y ) es cierto para Peano 1a. Por lo tanto, x < y ∨ I ( n , x , y ) . Ahora, demostramos Q ( S ( v ) : Suponga que I ( N , x + S ( v ) , y ) . De esta definición tenemos x < y y por lo tanto x < y ∨ I ( N , x , y ) también en este caso. Finalmente, el quinto axioma de Peano da Q ( z ) y por ( ∗ ) obtenemos x < y ∨ I ( N , x , y .
Teorema B
Para todo x < y ∨ I ( N , x , y ) ∨ y < x Prueba:
Si entonces ¬ I ( N , x , y ) por definición, y si x > y entonces ¬ I ( N , x , y ) también por definición. Si x > y e y > x entonces por transitividad y reflexividad, tenemos I ( N , x , y ) , lo cual es una contradicción. En consecuencia, no más de una de las declaraciones es verdadera.
Mantenemos fijo e inducimos en x . Cuando I ( N , 0 , y ) tenemos 0 < y ∨ I ( N , 0 , y ) para todo y , lo que demuestra el caso base. Luego, suponga que el teorema se cumple para x ; ahora queremos probar el teorema de S ( x ) . De la tricotomía para x , hay tres casos: x < y , I ( N , x y x > y . Si x > y , entonces claramente S ( x ) > y . Si I ( N , x , y ) , entonces S ( x ) > y (como S ( x ) > x para todo x ∈ N ). Finalmente, supongamos que x < y Luego, por el teorema A tenemos S ( x ) o I ( N , S ( x ) , y ) , y en cualquier caso hemos terminado.
Los teoremas que deseo probar se pueden expresar de la siguiente manera en Coq.
Lema less_lem (xy: N): menos x (succ y) -> o (less xy) (IN xy).
Teorema Ntricotomía: (para xy: N, o (menos xy) (o (IN xy) (menos yx))).
Resultados útiles
Aquí, he reunido algunos de los resultados que he definido, y probé hasta este punto. Estos son los que menciono anteriormente. * Este es el código que he logrado escribir hasta ahora, tenga en cuenta que la mayoría consiste en definiciones. * *
(* Sigma types *)
Inductive Sigma (A:Set)(B:A -> Set) :Set :=
Spair: forall a:A, forall b : B a,Sigma A B.
Definition E (A:Set)(B:A -> Set)
(C: Sigma A B -> Set)
(c: Sigma A B)
(d: (forall x:A, forall y:B x,
C (Spair A B x y))): C c :=
match c as c0 return (C c0) with
| Spair a b => d a b
end.
(* Binary sum type *)
Inductive sum' (A B:Set):Set :=
inl': A -> sum' A B | inr': B -> sum' A B.
Print sum'_rect.
Definition D (A B : Set)(C: sum' A B -> Set)
(c: sum' A B)
(d: (forall x:A, C (inl' A B x)))
(e: (forall y:B, C (inr' A B y))): C c :=
match c as c0 return C c0 with
| inl' x => d x
| inr' y => e y
end.
(* Three useful finite sets *)
Inductive N_0: Set :=.
Definition R_0
(C:N_0 -> Set)
(c: N_0): C c :=
match c as c0 return (C c0) with
end.
Inductive N_1: Set := zero_1:N_1.
Definition R_1
(C:N_1 -> Set)
(c: N_1)
(d_zero: C zero_1): C c :=
match c as c0 return (C c0) with
| zero_1 => d_zero
end.
Inductive N_2: Set := zero_2:N_2 | one_2:N_2.
Definition R_2
(C:N_2 -> Set)
(c: N_2)
(d_zero: C zero_2)
(d_one: C one_2): C c :=
match c as c0 return (C c0) with
| zero_2 => d_zero
| one_2 => d_one
end.
(* Natural numbers *)
Inductive N:Set :=
zero: N | succ : N -> N.
Print N.
Print N_rect.
Definition R
(C:N -> Set)
(d: C zero)
(e: (forall x:N, C x -> C (succ x))):
(forall n:N, C n) :=
fix F (n: N): C n :=
match n as n0 return (C n0) with
| zero => d
| succ n0 => e n0 (F n0)
end.
(* Boolean to truth-value converter *)
Definition Tr (c:N_2) : Set :=
match c as c0 with
| zero_2 => N_0
| one_2 => N_1
end.
(* Identity type *)
Inductive I (A: Set)(x: A) : A -> Set :=
r : I A x x.
Print I_rect.
Theorem J
(A:Set)
(C: (forall x y:A,
forall z: I A x y, Set))
(d: (forall x:A, C x x (r A x)))
(a:A)(b:A)(c:I A a b): C a b c.
induction c.
apply d.
Defined.
(* functions are extensional wrt
identity types *)
Theorem I_I_extensionality (A B: Set)(f: A -> B):
(forall x y:A, I A x y -> I B (f x) (f y)).
Proof.
intros x y P.
induction P.
apply r.
Defined.
(* addition *)
Definition add (m n:N) : N
:= R (fun z=> N) m (fun x y => succ y) n.
(* multiplication *)
Definition mul (m n:N) : N
:= R (fun z=> N) zero (fun x y => add y m) n.
(* Axioms of Peano verified *)
Theorem P1a: (forall x: N, I N (add x zero) x).
intro x.
(* force use of definitional equality
by applying reflexivity *)
apply r.
Defined.
Theorem P1b: (forall x y: N,
I N (add x (succ y)) (succ (add x y))).
intros.
apply r.
Defined.
Theorem P2a: (forall x: N, I N (mul x zero) zero).
intros.
apply r.
Defined.
Theorem P2b: (forall x y: N,
I N (mul x (succ y)) (add (mul x y) x)).
intros.
apply r.
Defined.
Definition pd (n: N): N :=
R (fun _=> N) zero (fun x y=> x) n.
(* alternatively
Definition pd (x: N): N :=
match x as x0 with
| zero => zero
| succ n0 => n0
end.
*)
Theorem P3: (forall x y:N,
I N (succ x) (succ y) -> I N x y).
intros x y p.
apply (I_I_extensionality N N pd (succ x) (succ y)).
apply p.
Defined.
Definition not (A:Set): Set:= (A -> N_0).
Definition isnonzero (n: N): N_2:=
R (fun _ => N_2) zero_2 (fun x y => one_2) n.
Theorem P4 : (forall x:N,
not (I N (succ x) zero)).
intro x.
intro p.
apply (J N (fun x y z =>
Tr (isnonzero x) -> Tr (isnonzero y))
(fun x => (fun t => t)) (succ x) zero)
.
apply p.
simpl.
apply zero_1.
Defined.
Theorem P5 (P:N -> Set):
P zero -> (forall x:N, P x -> P (succ x))
-> (forall x:N, P x).
intros base step n.
apply R.
apply base.
apply step.
Defined.
(* I(A,-,-) is an equivalence relation *)
Lemma Ireflexive (A:Set): (forall x:A, I A x x).
intro x.
apply r.
Defined.
Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).
intros x y P.
induction P.
apply r.
Defined.
Lemma Itransitive (A:Set):
(forall x y z:A, I A x y -> I A y z -> I A x z).
intros x y z P Q.
induction P.
assumption.
Defined.
Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)).
intros m n H.
induction H.
apply r.
Defined.
Lemma zeroadd: (forall n:N, I N (add zero n) n).
intro n.
induction n.
simpl.
apply r.
apply succ_cong.
auto.
Defined.
Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))).
intros.
induction n.
simpl.
apply r.
simpl.
apply succ_cong.
auto.
Defined.
Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)).
intros n m; elim n.
apply zeroadd.
intros y H; elim (succadd m y).
simpl.
rewrite succadd.
apply succ_cong.
assumption.
Defined.
Lemma associative_add: (forall m n k:N,
I N (add (add m n) k) (add m (add n k))).
intros m n k.
induction k.
simpl.
apply Ireflexive.
simpl.
apply succ_cong.
assumption.
Defined.
Definition or (A B : Set):= sum' A B.
Definition less (m n: N) :=
Sigma N (fun z => I N (add m (succ z)) n).
Lemma less_lem (x y:N) :
less x (succ y) -> or (less x y) (I N x y).
intro.
destruct H.
right.
(* Here is where I'm working right now *)
Defined.
Theorem Ntrichotomy: (forall x y:N,
or (less x y) (or (I N x y) (less y x))).
Respuestas:
Coq es un poco más cruel que las pruebas en papel: cuando escribe "y terminamos" o "claramente" en una prueba en papel, a menudo hay mucho más que hacer para convencer a Coq.
Ahora hice una pequeña limpieza de su código, mientras trataba de mantenerlo en el mismo espíritu. Lo puedes encontrar aquí .
Varios comentarios:
Usé tipos de datos y definiciones incorporados donde pensé que no dañaría tu intención. Tenga en cuenta que si hubiera utilizado la igualdad incorporada en lugar de
identity
la relación "menor que", las pruebas habrían sido mucho más fáciles, ya que muchos de sus lemas están en la base de datos de teoremas conocidos, que se verifican en cada llamada deUsé algunas tácticas que probablemente no conozcas, pero un superusuario "real" de Coq tendría tácticas mucho más poderosas a mano y escribiría sus propias tácticas para simplificar el trabajo. Siempre recomiendo CPDT como el lugar para aprender sobre el uso de tácticas de una manera poderosa.
induction
less
Si bien puede obtener respuestas a este tipo de preguntas aquí, le recomiendo que envíe su trabajo a Coq-Club, que fue creado con el propósito expreso de responder a este tipo de preguntas.
fuente
La respuesta de Cody es excelente y cumple con su pregunta sobre la traducción de su prueba a Coq. Como complemento a eso, quería agregar los mismos resultados, pero probé usando una ruta diferente, principalmente como una ilustración de algunos bits de Coq y para demostrar lo que puede probar sintácticamente con muy poco trabajo adicional. Sin embargo, esto no es una afirmación de que esta es la ruta más corta, solo una diferente. Las pruebas solo incluyen un lema auxiliar adicional, y se basan solo en definiciones básicas, no introduzco la suma, la multiplicación o ninguna de sus propiedades, o la extensionalidad funcional, y los únicos axiomas de Peano son una forma simple de a <= b -> a + c <= b + c en el lema auxiliar (solo para c = 1) y la inducción estructural, que de todos modos viene con tipos inductivos gratis.
Al igual que Cody, donde pensé que no había diferencia, usé tipos predefinidos, etc., así que antes de la prueba, describiré esos:
y
Lo que sigue ahora son mis pruebas, en principio, si el marcado no se interpone en el camino, debería ser capaz de cortar y pegar esto en un archivo Coq .v y funcionará. He incluido comentarios para notar partes interesantes, pero están en delimitadores (* *), por lo que no debería tener que eliminarlos.
fuente