Elementos de matemáticas formalizados en Isabelle/HOL

Elementos de matem´aticas formalizados en Isabelle/HOL Facultad de Matem´ aticas Departamento de Ciencias de la Computaci´ on e Inteligencia Artificial Trabajo Fin de Grado Carlos N´u˜nez Fern´andez 2 El presente Trabajo Fin de Grado se ha realizado en el Departamento de Ciencias de la Computaci´ on e Inteligencia Artificial de la Universidad de Sevilla y ha sido supervisado por Jos´ e Antonio Alonso Jim´ enez y Mar´ ıa Jos´ e Hidalgo Doblado. ´ Indice Sumario 7 Introducci´on 9 1 Teor´ıa de n´umeros 13 1.1 Suma de los primeros n´ umeros impares .................... 13 1.1.1 Demostraci´ on en lenguaje natural ................... 13 1.1.2 Especificaci´ on en Isabelle/HOL .................... 14 1.1.3 Demostraci´ on autom´ atica ........................ 14 1.1.4 Demostraci´ on estructurada ....................... 15 1.1.5 Demostraci´ on con patrones ....................... 16 1.2 Propiedad de los conjuntos finitos de n´ umero naturales ........... 17 1.2.1 Demostraci´ on en lenguaje natural ................... 17 1.2.2 Especificaci´ on en Isabelle/HOL .................... 18 1.2.3 Demostraci´ on autom´ atica ........................ 19 1.2.4 Demostraci´ on detallada ......................... 20 2 Teor´ıa de funciones 23 2.1 Cancelaci´ on de funciones inyectivas ...................... 23 2.1.1 Demostraci´ on en lenguaje natural ................... 23 2.1.2 Especificaci´ on en Isabelle/Hol ..................... 26 2.1.3 Demostraci´ on estructurada de los lemas ................ 26 2.1.4 Demostraci´ on del teorema en Isabelle/Hol .............. 29 2.2 Cancelaci´ on de las funciones sobreyectivas .................. 29 3 4´ Indice 2.2.1 Demostraci´ on en lenguaje natural ................... 29 2.2.2 Especificaci´ on en Isabelle/Hol ..................... 32 2.2.3 Demostraci´ on estructurada ....................... 32 2.2.4 Demostraci´ on teorema .......................... 35 2.2.5 Demostraci´ on autom´ atica del teorema ................. 36 3 Teor´ıa de conjuntos 37 3.1 Teorema de Cantor ................................ 37 3.1.1 Demostraci´ on en lenguaje natural ................... 37 3.1.2 Especificaci´ on en Isabelle/HOL .................... 38 3.1.3 Demostraci´ on detallada ......................... 38 3.1.4 Demostraci´ on autom´ atica ........................ 40 4 Teor´ıa de ret´ıculos 41 4.1 Teorema de Knaster Tarski ............................ 41 4.1.1 Demostraci´ on en lenguaje natural ................... 41 4.1.2 Especificaci´ on en Isabelle/HOL .................... 43 4.1.3 Demostraci´ on detallada ......................... 44 4.1.4 Demostraci´ on autom´ atica ........................ 45 5 Teor´ıa de geometr´ıa 47 5.1 Introducci´ on a la geometr´ ıa ........................... 47 5.2 Geometr´ ıa simple ................................. 48 5.2.1 Entorno local ............................... 48 5.2.2 Proposiciones de geometr´ ıa simple ................... 48 5.2.3 Interpretaci´ on m´ ınimo modelo geometr´ ıa simple .......... 55 5.3 Geometr´ ıa no proyectiva ............................. 55 5.3.1 Entorno local ............................... 55 5.3.2 Proposiciones de geometr´ ıa no proyectiva .............. 56 5.3.3 Interpretacion modelo geometr´ ıa no proyectiva ........... 57 5.4 Geometr´ ıa proyectiva ............................... 57 5.4.1 Entorno local ............................... 57 ´ Indice 5 5.4.2 Proposiciones de geometr´ ıa proyectiva ................ 58 5.4.3 Interpretaci´ on modelo geometr´ ıa proyectiva ............. 70 A Lemas de HOL usados 73 A.1 Las bases de l´ ogica de orden superior (2) ................... 73 A.1.1 L´ ogica primitiva (2.1) .......................... 73 A.1.2 Reglas fundamentales (2.2) ....................... 74 A.2 ´ Ordenes abstractos (4) .............................. 75 A.2.1 Monotonicidad (4.9) ........................... 75 A.2.2 Nombres duplicados (4.17) ....................... 75 A.3 Grupos (5) ..................................... 76 A.3.1 Soporte para razonar sobre signos (5.7) ................ 76 A.4 Ret´ ıculos abstractos (6) .............................. 76 A.4.1 Ret´ ıculos concretos (6.3) ......................... 76 A.5 Teor´ ıa de conjuntos para l´ ogica de orden superior(7) ............. 76 A.5.1 Conjuntos como prediados ....................... 76 A.5.2 Operaciones b´ asicas (7.3) ........................ 76 A.6 Nociones sobre funciones (9) .......................... 77 A.6.1 El operador composici´ on (9.2) ...................... 77 A.6.2 Inyectividad y biyectividad (9.5) .................... 77 A.6.3 Actualizaci´ on de funciones (9.6) .................... 77 A.7 Ret´ ıculos completos (10) ............................. 77 A.7.1 Ret´ ıculos completos abstractos (10.3) .................. 77 A.8 N´ umeros naturales (16) .............................. 78 A.8.1 Operaciones aritm´ eticas (16.3) ..................... 78 A.9 Conjuntos finitos(18) ............................... 78 A.9.1 Predicados para conjuntos finitos .................... 78 A.10 M´ etodo de prueba Meson (37) .......................... 78 A.10.1 Forma de negaci´ on normal (37.1) .................... 78 Bibliograf´ıa 79 6´ Indice Sumario La finalidad de este trabajo es la formalizaci´ on de teoremas de diferentes teor´ ıas de las matem´ aticas. Para ello, se han elegido una serie de teoremas de la teor´ ıa de n´ umeros, teor´ ıa de conjuntos, teor´ ıa de funciones, teor´ ıa de ret´ ıculos y teor´ ıa de geometr´ ıa. Una vez formalizados los mismos en el sistema de pruebas autom´ aticas Isabelle/HOL, se han utilizado teor´ ıas ya predefinidas en ´ el y comprobado la similitud existente entre la demostraci´ on en lenguaje natural y la demostraci´ on formal. The purpose of this project is the formalization of theorems from differents mathematic’s theories. For it, some theorems have been choosen from number theory, set theory, function theory, lattice theory and geometry theory. Once they have been formalized by the automatic proof system Isabelle/HOl, theories have already been used predefined in it and checking the existing similarity between proof in natural language and formal proof. 7 8´ Indice Introducci´on Actualmente el gran inter´ es de la formalizaci´ on matem´ atica reside en la capacidad de la verificaci´ on de demostraciones mediante un ordenador. Para ello, se hace preciso poder expresar las definiciones, teoremas y pruebas en un lenguaje generado por una gram´ atica que permita verificar de forma mec´ anica las pruebas. Tambi´ en hay que dotar al ordenador de una informaci´ on previa al teorema de forma que junto con una orientaci´ on humana, se pueda llegar a validar la demostraci´ on de los teoremas. La importancia que se le atribuye a la formalizaci´ on es la capacidad de c´ alculos y razonamientos que puede realizar un ordenador a la vez, incluso demostrando teoremas muy dif´ ıciles como el teorema de los Knaster–Tarski como se expondr´ a en el Cap´ ıtulo 5. En [6] pueden encontrarse una lista de 100 teoremas formalizados junto con el programa usado. Dentro de los sistemas de pruebas autom´ aticas los m´ as usados, como se aprecia en [7] son HOL, Mizar, PVS, Coq, Isabelle/Isar entre otros. Isabelle suministra una estructura gen´ erica para construir sistemas deductivos con un especial foco en la prueba de teoremas de l´ ogica de orden superior. Sin embargo, Isar proporciona un entorno de lenguaje propio, dise˜ nado espec´ ıficamente para el desarrollo de pruebas y teorias. En su conjunto Isabelle/Isar es un marco de referencia para el desarrollo formal de documentos matem´ aticos, incluida una comprobaci´ on completa de pruebas, en el que las definiciones y pruebas se organizan como teorias. En el presente an´ alisis, el sistema de pruebas autom´ atico utilizado es Isabelle/HOL que es una especializaci´ on de Isabelle/Isar con l´ ogica de orden superior(HOL). El objetivo general de este trabajo es mostrar como se elaboran demostraciones formales y estructuradas en Isabelle/HOL, manifestando la capacidad que tiene este sistema de pruebas autom´ aticas en los diferentes aspectos de las matem´ aticas. El objetivo espec´ ıfico es estudiar la similitud que hallada entre las demostraciones en lenguaje natural y las de lenguaje formal en Isabelle/HOL de aspectos b´ asicos de las diferentes teor´ ıas de las matem´ aticas. La metodolog´ ıa utilizada para este trabajo ha sido seleccionar y probar formalmente teoremas en las distintas ´ areas de las matem´ aticas, de forma que se muestre la capacidad de Isabelle/HOl en los diferentes ´ ambitos. Una vez escogido el teorema para 9 16 Cap´ ıtulo 1. Teor´ ıa de n´ umeros by simp qed 1.1.5 Demostraci´on con patrones La demostraci´ on anterior se puede simplificar usando patrones. lemma suma-impares n =n∗n(is ?P n =?Q n) proof (induct n) show ?P 0 =?Q 0 by simp next fix n assume HI:?P n =?Q n have ?P (Suc n)=(2∗(Suc n)−1) + suma-impares n by simp also have . . . = (2∗(Suc n)−1) + n∗nusing HI by simp also have . . . =?Q (Suc n)by simp finally show ?P (Suc n) = ?Q (Suc n)by simp qed La demostraci´ on usando otro patr´ on es lemma suma-impares n =n∗n(is ?P n) proof (induct n) show ?P 0 by simp next fix n assume ?P n then show ?P (Suc n)by simp qed 1.2. Propiedad de los conjuntos finitos de n´ umero naturales 17 1.2 Propiedad de los conjuntos finitos de n´umero naturales 1.2.1 Demostraci´on en lenguaje natural El siguiente teorema es una propiedad que verifican todos los conjuntos finitos de n´ umeros naturales. Se ha estudiado en el tema 10 de la asignatura de LMF de tercer curso del grado en Matem´ aticas. Su enunciado es el siguiente: Teorema 1.2.1 Sea S un conjunto finito de n´umeros naturales. Entonces todos los elementos de S son menores o iguales que la suma de los elementos de S; es decir, ∀m∈S=⇒m≤∑S donde ∑S denota la suma de todos los elementos de S. Primero se debe notar que podemos dar una definici´ on inductiva de conjunto finito, lo que conlleva un esquema de inducci´ on asociado. Definici´on 1.2.2 La definici´on inductiva de un conjunto finito es: •∅es finito. • Si A es un conjunto finito y x un elemento entonces A ∪ {x}es un conjunto finito. De esta construcci´ on se obtiene un esquema de inducci´ on. Para ello sea ϕuna propiedad sobre conjuntos finitos. El esquema de inducci´ on viene dado por: Si se verifica: 1. ϕ(∅). 2. ∀Afinito tal que ϕ(A)y∀xentonces ϕ(A∪ {x}). Entonces ∀Afinito se verifica ϕ(A). Demostraci´on: La demostraci´ on del teorema la haremos por inducci´ on sobre conjuntos finitos. (Base de la inducci´ on) El caso S=∅es trivial. (Paso de la inducci´ on) Supongamos que se verifica el teorema para un conjunto finito de n´ umeros naturales, que se denotar´ a por Sy sea aun elemento. Vamos a demostrarlo para S∪ {a}. 18 Cap´ ıtulo 1. Teor´ ıa de n´ umeros Sea a∈Ntal que a/∈S, ya que si a∈Sse tendr´ ıa probado el teorema. Luego hay que probar que: ∀n∈S∪ {a}=⇒n≤∑(S∪ {a}) Distingamos dos casos ahora: Caso 1: n=a. Si n=a, se tiene que: n=a≤a+∑S=∑(S∪ {a}). Caso 2: n6=a. Si n6=a, tenemos que n∈S, luego usando la hip´ otesis de inducci´ on: n≤∑S≤∑S+a=∑(S∪ {a}).  En la demostraci´ on del teorema hemos usado un resultado, que vamos a probar en Isabelle despu´ es de la especificaci´ on del teorema; el resultado es ∑S+a=∑(S∪ {a}). 1.2.2 Especificaci´on en Isabelle/HOL Para la especificaci´ on del teorema en Isabelle, primero consideremos la definici´ on de conjunto finito ya definida en Isabelle. inductive finite :: ”’a set ⇒bool” where emptyI [simp, intro!]: ”finite {}” |insertI [simp, intro!]: ”finite A =⇒finite (insert a A)” Esta definici´ on de conjunto finito es una definici´ on inductiva en Isabelle, equivalente a la Definici´ on 1.2.2 en lenguaje natural. Esta definici´ on genera autom´ aticamente el siguiente esquema de inducci´ on en Isabelle: [[finite x;P∅;VA a.finite A ∧P A =⇒P({a} ∪ A)]] =⇒P x (finite.induct) Tambi´ en se debe notar que finite S indica que un conjunto Ses finito y definir la funci´ on sumaConj tal que sumaConj n es la suma de todos los elementos de S. definition sumaConj :: nat set ⇒nat where 1.2. Propiedad de los conjuntos finitos de n´ umero naturales 19 sumaConj S ≡∑S Donde ∑ya se encuentra definido en Isabelle, pero se renombra de la siguiente forma: abbreviation Sum (”∑”) where ”∑≡sum (λx.x)” El enunciado del teorema es el siguiente : lemma finite S =⇒ ∀ x∈S.x≤sumaConj S oops Vamos a demostrar primero el lema enunciado anteriormente lemma aux-propiedad-conjuntos-finitos: assumes finite S x/∈S shows x+sumaConj S =sumaConj (insert x S) proof − have x+sumaConj S =x+∑S by (simp only:sumaConj-def ) also have . . . =sum (λx.x) (insert x S) using assms by (rule sum.insert[THEN sym]) also have . . . =sumaConj (insert x S) by (simp only:sumaConj-def ) finally show ?thesis by this qed En la demostraci´ on del lema anterior se ha usado sumConj-def, que hace referencia a la definici´ on sumaConj que hemos hecho anteriormente. Vamos a presentar diferentes formas de demostraci´ on: 1.2.3 Demostraci´on autom´atica La demostraci´ on autom´ atica es: lemma finite S =⇒ ∀ x∈S.x≤sumaConj S by (induct rule:finite-induct) (auto simp add:sumaConj-def ) 20 Cap´ ıtulo 1. Teor´ ıa de n´ umeros 1.2.4 Demostraci´on detallada La demostraci´ on declarativa es: lemma sumaConj-acota: finite S =⇒ ∀ x∈S.x≤sumaConj S proof (induct rule:finite-induct) show ∀x∈ {}.x≤sumaConj {} by (simp only:ball-empty) next fix xand F assume fF:finite F and xF:x/∈F and HI:∀x∈F.x≤sumaConj F show ∀y∈insert x F.y≤sumaConj (insert x F) proof fix y assume y∈insert x F then have y=x∨y∈F by (simp only:insert-iff ) then show y≤sumaConj (insert x F) proof assume y=x then have y≤x+ (sumaConj F) by (simp only:le-add-same-cancel1) also have . . . =sumaConj (insert x F) using fF xF by (rule aux-propiedad-conjuntos-finitos) finally show ?thesis by this next assume y∈F then have y≤sumaConj F using HI by (simp only:HI) also have . . . ≤x+ (sumaConj F) by (simp only:le-add-same-cancel2) also have . . . =sumaConj (insert x F) using fF xF by (rule aux-propiedad-conjuntos-finitos) finally show ?thesis 1.2. Propiedad de los conjuntos finitos de n´ umero naturales 21 by this qed qed qed 22 Cap´ ıtulo 1. Teor´ ıa de n´ umeros Cap´ıtulo 2 Teor´ıa de funciones Este cap´ ıtulo muestra dos resultados de la teor´ ıa de funciones. Estos resultado son la caracterizaci´ on de funciones inyectivas y sobreyectivas respectivamente. Estos teoremas muestran la capacidad de Isabelle/HOL de trabajar con tipos, debido a que, en la demostraci´ on de ambos teoremas es necesario especificar los dominios y codominios de las funciones. 2.1 Cancelaci´on de funciones inyectivas 2.1.1 Demostraci´on en lenguaje natural El siguiente teorema que se va a probar es una caracterizaci´ on de las funciones inyectivas. Primero se definir´ a el significado de inyectividad de una funci´ on y la propiedad de ser cancelativa por la izquierda. Definici´on 2.1.1 Una funci´on f :A−→ B es inyectiva si ∀x,y∈A:f(x) = f(y) =⇒x=y. Antes de definir la propiedad de ser cancelativa por la izquierda se va a probar la siguiente propiedad. Lema 2.1.2 Sea f una funci´on f :A−→ B. Las siguientes condiciones son equivalentes: 1. ∀C:(∀g,h:C−→ A):f◦g=f◦h=⇒g=h. 23 24 Cap´ ıtulo 2. Teor´ ıa de funciones 2. ∀g,h:{0, 1} −→ A:f◦g=f◦h=⇒g=h. Demostraci´on: 1=⇒2 Trivial, ya que tomando en particular el conjunto C={0, 1}se tiene probado. 2=⇒1 La prueba se va a realizar por reducci´ on al absurdo, es decir, supongamos que ∃C:∃g,h:C−→ A:f◦g=f◦hyg6=h. Como g6=hesto implica que ∃c∈Ctal que g(c)6=h(c). Consideremos ahora r:{0, 1} −→ Atal que r(x) = c si x =0 c si x =1 Definamos entonces g0=g◦ryh0=h◦r. Luego se tiene que (f◦g0)(x) = (f◦g◦r)(x) = (( f◦g)◦r))(x) = (( f◦h)◦r)(x)(Hip´otesis inducci´on) = (f◦h◦r)(x) = (f◦h0)(x) Entonces f◦g0=f◦h0. Luego, usando la hip´ otesis g0=h0. Por otra parte g0(0) = (g◦r)(0) =g(r(0)) =g(c) h0(0) = (h◦r)(0) =h(r(0)) =h(c) Luego g0(0)6=h0(0)por lo que hemos llegado a un absurdo.  Puesto que tenemos esta equivalencia, la definici´ on de la propiedad de ser cancelativa por la izquierda ser´ a: Definici´on 2.1.3 (Cancelativa izquierda) Una funci´on f :A−→ B es cancelativa por la izquierda si ∀g,h:{0, 1} −→ A:f◦g=f◦h=⇒g=h. Nota 2.1.4 Es adecuado usar esta definici´on, ya que a la hora de especificar la definici´on en Isabelle no se puede cuantificar tipos y esta definici´on no lo requiere. Sin embargo, la otra s´ı. 2.1. Cancelaci´ on de funciones inyectivas 25 El teorema es el siguiente: Teorema 2.1.5 Una funci´on f es inyectiva si y solo si es cancelativa por la izquierda. Vamos a hacer dos lemas previos, ya que se descompone la doble implicaci´ on en dos implicaciones y se va a demostrar cada una de ellos por separado. Lema 2.1.6 (Condici´on necesaria) Si f es una funci´on inyectiva, entonces f es cancelativa por la izquierda. Demostraci´on: Hay que probar que ∀g,h:{0, 1} −→ A:f◦g=f◦hesto implica que g=h. Luego, sean g,htales que f◦g=f◦h, veamos que ∀x.g(x) = h(x). Se tiene que: f◦g=f◦h=⇒(f◦g)(x) = ( f◦h)(x)de f . =⇒f(g(x)) = f(h(x)) f inyect. =⇒g(x) = h(x)  Lema 2.1.7 (Condici´on suficiente) Si f es cancelativa por la izquierda, entonces f es inyectiva. Demostraci´on: Sea f:A−→ B. Si el dominio de la funci´ on ffuese vac´ ıo, f es inyectiva. Supongamos que el dominio de la funci´ on fes distinto del vac´ ıo y que f verifica la propiedad de ser cancelativa por la izquierda. Hay que demostrar que ∀a,btales que f(a) = f(b), esto implica que a=b. Sean a,btales que f(a) = f(b). Consideremos las funciones constantes g:{0, 1} −→ Atal que g(x) = a,∀xy h:{0, 1} −→ Atal que h(x) = b,∀x. Veamos que f◦g=f◦h. En efecto, ∀x (f◦g)(x) =f(g(x)) =f(a) (f◦h)(x) =f(h(x)) =f(b) Por hip´ otesis se tiene que f(a) = f(b)luego f◦g=f◦h. Por hip´ otesis se tiene que fes cancelativa por la izquierda, por lo tanto, esto implica que g=h. Es decir, que ∀x,g(x) = h(x). Y, por tanto, a=b.  32 Cap´ ıtulo 2. Teor´ ıa de funciones Por lo que g(y) = h(y), con lo que hemos llegado a una contradicci´ on.  2.2.2 Especificaci´on en Isabelle/Hol Su especificaci´ on es la siguiente, que se dividir´ a en dos al igual que en la demostraci´ on a mano: definition cancelativaDerecha :: (0a⇒0b)⇒bool where cancelativaDerecha f = (∀(g:: 0b⇒bool)h.(g◦f=h◦f−→ g=h)) theorem caracterizacion-funciones-sobreyectivas: surj f ←→ cancelativaDerecha f oops lemma condicion-suficiente: surj f =⇒cancelativaDerecha f oops lemma condicion-necesaria: cancelativaDerecha f =⇒surj f oops En la especificaci´ on anterior, surj f es una abreviatura de range f =UNIV, donde range f es el rango o imagen de la funci´ on f y UNIV es el conjunto universal definido en la teor´ ıa Set.thy como una abreviatura de top que, a su vez est´ a definido en la teor´ ıa Orderings.thy mediante la siguiente propiedad ordering-top less-eq less top less-eq a top (ordering-top.extremum) Adem´ as queda a˜ nadir que la teor´ ıa donde se encuentra definido surj f es en Fun.thy. Esta teor´ ıa contiene la definicion surj-def. surj f = (∀y.∃x.y=f x)(surj--def) 2.2.3 Demostraci´on estructurada Presentaremos distintas demostraciones de los lemas. Las primeras son las detalladas: 2.2. Cancelaci´ on de las funciones sobreyectivas 33 lemma condicion-suficiente-detallada: assumes surj f shows cancelativaDerecha f proof − have ∀(g:: 0a⇒bool)h.(g◦f=h◦f−→ g=h) proof (intro allI impI) fix g h :: 0a⇒bool assume g◦f=h◦f show g=h proof (rule ext) fix x have ∃y.x=f y using assms by (simp only:surjD) then obtain ywhere x=f y by (rule exE) then have g x =g(f y) by (simp only:hx=f yi) also have . . . = (g◦f)y by (simp only:comp-apply) also have . . . = (h◦f)y by (simp only:hg◦f=h◦fi) also have . . . =h(f y) by (simp only:comp-apply) also have . . . =h x by (simp only:hx=f yi) finally show g x =h x by this qed qed then show cancelativaDerecha f by (simp only:cancelativaDerecha-def) qed lemma condicion-necesaria-detallada-l1: assumes @x.y=f x shows g◦f=g(y:=z)◦f proof (rule ext) fix a show (g◦f)a= (g(y:=z)◦f)a 34 Cap´ ıtulo 2. Teor´ ıa de funciones proof − have ∀x.y6=f x using assms by (rule Meson.not-exD) then have y6=f a by (rule allE) then have f a 6=y by (rule not-sym) have (g◦f)a=g(f a) by (simp only:o-apply) also have . . . = (g(y:=z)) (f a) using hf a 6=yi by (rule fun-upd-other [THEN sym]) also have . . . = (g(y:=z)◦f)a by (simp only:o-apply) finally show ?thesis by this qed qed lemma condicion-necesaria-detallada-l2: assumes (λx.a)=(λx.a)(y:=b) shows a=b proof − have a= ((λx.a)(y:=b)) y using assms by (rule fun-cong) also have . . . =b by (rule fun-upd-same) finally show a=b by this qed lemma condicion-necesaria-detallada: assumes cancelativaDerecha f shows surj f proof − have ∀y.∃x.y=f x proof (rule ccontr) assume ¬(∀y.∃x.y=f x) 2.2. Cancelaci´ on de las funciones sobreyectivas 35 then have ∃[email protected]=f x by (rule Meson.not-allD) then obtain y0 where @x.y0 =f x by (rule exE) then have ∀x.y0 6=f x by (rule Meson.not-exD) let ?g = (λx.True):: 0b⇒bool let ?h =?g(y0 :=False) have ∀(g:: 0b⇒bool)h.g◦f=h◦f−→ g=h using assms by (simp only:cancelativaDerecha-def) then have ∀h.(?g ◦f=h◦f)−→ (?g =h) by (rule allE) then have (?g ◦f=?h ◦f)−→ (?g =?h) by (rule allE) moreover have (?g ◦f=?h ◦f) using [email protected] =f xi by (rule condicion-necesaria-detallada-l1) ultimately have (?g =?h) by (rule mp) then have True =False by (rule condicion-necesaria-detallada-l2) with True-not-False show False by (rule notE) qed then show surj f using surj-def by (rule rev-iffD2) qed 2.2.4 Demostraci´on teorema En consecuencia, la demostraci´ on del teorema es theorem caracterizacion-funciones-sobreyectivas: surj f ←→ cancelativaDerecha f proof (rule iffI) show surj f =⇒cancelativaDerecha f by (rule condicion-suficiente-detallada) next show cancelativaDerecha f =⇒surj f 36 Cap´ ıtulo 2. Teor´ ıa de funciones by (rule condicion-necesaria-detallada) qed 2.2.5 Demostraci´on autom´atica del teorema theorem surj f ←→ cancelativaDerecha f by (auto simp add:condicion-suficiente-detallada condicion-necesaria-detallada) Cap´ıtulo 3 Teor´ıa de conjuntos En este cap´ ıtulo se analiza un teorema importante de la teor´ ıa de conjuntos, el teorema de Cantor; en el que la demostraci´ on formal y en lenguaje natural es pr´ acticamente id´ entica. 3.1 Teorema de Cantor 3.1.1 Demostraci´on en lenguaje natural El siguiente teorema, denominado teorema de Cantor por el matem´ atico Georg Cantor, es un resultado importante de la teor´ ıa de conjuntos. Para la exposici´ on del teorema vamos a definir una serie de conceptos: Definici´on 3.1.1 (Conjunto Potencia) El conjunto potencia de un conjunto A (P(A)) es el conjunto formado por todos los subconjuntos de A. Definici´on 3.1.2 (Cardinal) El cardinal de un conjunto A (denotado #A) es el n´umero de elementos del propio conjunto. El enunciado original del teorema es el siguiente : Teorema 3.1.3 El cardinal del conjunto potencia de cualquier conjunto A es estrictamente mayor que el cardinal de A, o lo que es lo mismo, #P(A)>#A. El enunciado del teorema lo podemos reformular como sigue: 37 38 Cap´ ıtulo 3. Teor´ ıa de conjuntos Teorema 3.1.4 Dado un conjunto A, @f:A−→ P(A)sobreyectiva. Demostraci´on: La prueba se va a realizar por reducci´ on al absurdo. Supongamos que ∃f:A−→ P(A)sobreyectiva, es decir, ∀B∈ P(A),∃x∈Atal que B=f(x). En particular, tomemos el conjunto B={x∈A:x/∈f(x)} y supongamos que ∃a∈A:B=f(a), ya que Bes un subconjunto de A. Luego podemos distinguir dos casos : 1. Si a∈B. Entonces por definici´ on del conjunto Bse tiene que a/∈B, luego se llega a una contradicci´ on. 2. Si a/∈B. Entonces por definici´ on de B se tiene que a∈B, luego se ha llegado a otra contradicci´ on. En los dos casos se ha llegado a una contradicci´ on, por lo que no existe ayfno es sobreyectiva.  3.1.2 Especificaci´on en Isabelle/HOL Para la especificaci´ on del teorema en Isabelle, primero debemos notar que f:: 0a⇒0a set significa que es una funci´ on de tipos, donde 0asignifica un tipo y para poder denotar el conjunto potencia tenemos que poner 0a set que significa que es de un tipo formado por conjuntos del tipo 0a. El enunciado del teorema es el siguiente : theorem Cantor:@f:: 0a⇒0a set.∀A.∃x.A=f x oops A continuaci´ on presentaremos diferentes formas de demostraci´ on del teorema. 3.1.3 Demostraci´on detallada La primera es la demostraci´ on detallada del teorema: theorem 3.1. Teorema de Cantor 39 @f:: 0a⇒0a set.∀B.∃x.B=f x proof (rule notI) assume ∃f:: 0a⇒0a set.∀A.∃x.A=f x then obtain f:: 0a⇒0a set where Hf :∀A.∃x.A=f x by (rule exE) let ?B ={x.x/∈f x} from Hf obtain ∃x.?B =f x by (rule allE) then obtain awhere Ha:?B =f a by (rule exE) show False proof (cases a ∈?B) assume a∈?B then have a/∈f a by (rule CollectD) moreover have a∈f a using ha∈?Bi by (simp only:Ha) ultimately show False by (rule notE) next assume a/∈?B with Ha have a/∈f a by (rule subst) moreover have a∈f a proof (rule ccontr) assume a/∈f a then have a∈?B by (rule CollectI) with ha/∈?Bishow False by (rule notE) qed ultimately show False by (rule notE) qed qed 40 Cap´ ıtulo 3. Teor´ ıa de conjuntos 3.1.4 Demostraci´on autom´atica La demostraci´ on autom´ atica del teorema es: theorem Cantor: @f:: 0a⇒0a set.∀B.∃x.B=f x by best Cap´ıtulo 4 Teor´ıa de ret´ıculos En este cap´ ıtulo se muestra un teorema de la teor´ ıa de ret´ ıculos, el teorema de Knaster- Tarski. En Isabelle/HOL la teor´ ıa de ret´ ıculos ya se encuentra predefinida y tanto los ret´ ıculos como los ret´ ıculos completos se definen como clases. 4.1 Teorema de Knaster Tarski 4.1.1 Demostraci´on en lenguaje natural El siguiente teorema, denominado teorema de Knaster-Tarski del punto fijo, es un teorema de la teor´ ıa de ret´ ıculos y lleva el nombre de los matem´ aticos Bronislaw Knaster y Alfred Tarski. Para la exposici´ on y demostraci´ on del teorema es necesario definir una serie de conceptos previos. Definici´on 4.1.1 Sea L un conjunto. Un orden parcial sobre L es una relaci´on binaria ≤sobre L, tal que ∀x,y,z∈L se verifica: 1. x ≤x (Propiedad reflexiva). 2. Si x ≤y e y ≤x entonces x =y (Propiedad antisim´etrica). 3. Si x ≤y e y ≤z entonces que x ≤z (Propiedad transitiva). Definici´on 4.1.2 Un conjunto L con un relaci´on de orden (≤)se denomina conjunto parcialmente ordenado y se denota (L,≤). 41 48 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa 5.2 Geometr´ıa simple 5.2.1 Entorno local La geometr´ ıa simple, como ya se ha dicho anteriormente, posee tres elementos fundamentales. Los puntos, el plano, que es el conjunto de todos ellos, y las rectas, que son conjuntos de puntos. Esta geometr´ ıa posee 5 axiomas: 1. El plano es no vac´ ıo. 2. Toda l´ ınea es un subconjunto no vac´ ıo del plano. 3. Para cualquier par de puntos en el plano, existe una l´ ınea que contiene a ambos. 4. Dos l´ ıneas diferentes se cortan en no m´ as de un punto. 5. Para cada l´ ınea, existe un punto del plano que no pertenece a ella. Se ha declarado un entorno local, denotado Simple−Geometry, con un par de constantes (lines yplane) junto con los 5 axiomas anteriores. locale Simple-Geometry = fixes plane :: 0a set fixes lines :: (0a set)set assumes A1:plane 6={} and A2:∀l∈lines.l⊆plane ∧l6={} and A3:∀p∈plane.∀q∈plane.∃l∈lines.{p,q} ⊆ l and A4:∀l∈lines.∀r∈lines. l6=r−→ l∩r={} ∨ (∃q∈plane.l∩r={q}) and A5:∀l∈lines.∃q∈plane.q/∈l A pesar de la definici´ on del anterior entorno local con 5 axiomas, no en todas las demostraciones, se van a usar todos ellos. Sin embargo, al haber definido tanto las l´ ıneas como el plano como conjuntos tenemos todas las funciones definidas en Isabelle/HOL de la teor´ ıa de conjuntos Set.thy. 5.2.2 Proposiciones de geometr´ıa simple A continuaci´ on vamos a presentar una serie de lemas que vamos a demostrar dentro del entorno de la geometr´ ıa simple. El primer lema es el siguiente: 5.2. Geometr´ ıa simple 49 Lema 5.2.1 Existe al menos una l´ınea. Demostraci´on: Vamos a demostrar que el conjunto de l´ ıneas es no vac´ ıo. Para ello, supongamos en primer lugar, por el axioma A1, que qes un punto del plano. Entonces, por el axioma A3, tenemos que existe una l´ ınea ltal que {q,q} ⊆ l. Luego, ya hemos probado que existe una l´ ınea.  La formalizaci´ on del lema y su demostraci´ on en Isabelle/HOl es la siguiente: lemma (in Simple-Geometry)one-line-exists: ∃l.l∈lines proof − have ∃q.q∈plane using A1 by auto then obtain q1 where q1 ∈plane by (rule exE) then obtain ∃l∈lines.{q1,q1} ⊆ lusing A3 by auto then show ?thesis by auto qed El segundo lema es el siguiente Lema 5.2.2 Existen al menos dos puntos que son diferentes en el plano Demostraci´on: Para la demostraci´ on del lema, usando el lema anterior, tenemos que existe una l´ ınea l. Adem´ as, por el axioma A2, sabemos que l6=∅lo que implica que existe un punto qen l. Por otro lado, por el axioma A5, sabemos que existe un punto p que no est´ a en l. Luego ya tenemos probada la existencia de dos puntos. A parte, como p/∈lyq∈ltienen que ser distintos.  La especificaci´ on y demostraci´ on del lema en Isabelle/HOL es la siguiente: lemma (in Simple-Geometry)two-points-exist: ∃p1 p2.p1 6=p2 ∧ {p1,p2} ⊆ plane proof − obtain l1 where l1 ∈lines using one-line-exists by (rule exE) then obtain l1 ⊆plane ∧l1 6={} using A2 by auto then have ∃q.q∈l1 ∧q∈plane by auto then obtain p1 where p1 ∈l1 ∧p1 ∈plane by (rule exE) moreover obtain p2 where p2 ∈plane ∧p2 /∈l1 50 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa using hl1 ∈linesiA5 by auto ultimately show ?thesis by force qed El siguiente lema es el siguiente: Lema 5.2.3 Existen al menos tres puntos diferentes en el plano. Demostraci´on: Para la demostraci´ on del lema vamos a usar el lema anterior; es decir, tenemos que existen dos puntos distintos pyq. Por el axioma A3, se tiene que existe una l´ ınea lque pasa por esos dos puntos. Usando el axioma A5, sabemos que existe un punto rque no pertenece a l. Veamos que son diferentes; es decir, como hemos tomado p6=qsimplemente tenemos que probar que r6=qyr6=p. Como r/∈lya se tiene la prueba.  La especificaci´ on y demostraci´ on del lema en Isabelle/HOL es la siguiente: lemma (in Simple-Geometry)three-points-exist: ∃p1 p2 p3.distinct [p1,p2,p3]∧ {p1,p2,p3} ⊆ plane proof − obtain p1 p2 where p1 6=p2 ∧ {p1,p2} ⊆ plane using two-points-exist by auto moreover then obtain l1 where l1 ∈lines ∧ {p1,p2} ⊆ l1 using A3 by auto moreover then obtain p3 where p3 ∈plane ∧p3 /∈l1 using A5 by auto ultimately have distinct [p1,p2,p3]∧ {p1,p2,p3} ⊆ plane by auto then show ?thesis by (intro exI) qed El siguiente lema es una consecuencia inmediata del lema anterior. Lema 5.2.4 Si el plano es finito, entonces la cardinalidad del plano es mayor o igual que 3. La especificaci´ on y demostraci´ on del lema en Isabelle/HOL es la siguiente: lemma (in Simple-Geometry)card-of-plane-greater: assumes finite plane shows card plane ≥3 5.2. Geometr´ ıa simple 51 proof − obtain p1 p2 p3 where distinct [p1,p2,p3]∧ {p1,p2,p3} ⊆ plane using three-points-exist by auto moreover then have {p1,p2,p3} ⊆ plane by (rule conjE) then have card {p1,p2,p3} ≤ card plane using assms by (simp add:card-mono) ultimately show ?thesis by auto qed Lema 5.2.5 Sean a y b dos puntos distintos, l una l´ınea que pasa por ellos y p un punto fuera de l. Sea n una l´ınea que pasa por a y p y m una l´ınea que pasa b y p. Entonces, m 6=n. Demostraci´on: La demostraci´ on se har´ a por reducci´ on al absurdo; es decir, supongamos que m=ny se llegar´ a a un absurdo. Primero notemos que m6=lya que p/∈lpero p∈m, luego podemos aplicar el axioma A4 a las l´ ıneas myl. Al aplicarlo resulta que tenemos que l∩m=∅o existe un punto qtal que l∩m={q}. Primero supongamos que l∩m=∅, sin embargo b∈lyb∈mluego hemos llegado a n absurdo. Segundo supongamos que sea qel punto tal que l∩m=q, sin embargo al principio se ha supuesto que m=n. Por lo tanto, se tiene que {a,b} ⊆ {q}con lo que se ha llegado a un absurdo ya que a6=b. Por los dos casos se ha llegado a un absurdo luego, m6=n.  Para tener una visi´ on geom´ etrica de la demostraci´ on incluimos la figura 5.4.6. 52 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa Figura 5.1: Visi´ on geom´ etrica de la demostraci´ on de l´ ıneas diferentes La especificaci´ on y demostraci´ on del lema en Isabelle/HOL es la siguiente: lemma (in Simple-Geometry)how-to-produce-different-lines: assumes l∈lines {a,b} ⊆ l a 6=b p/∈l n∈lines {a,p} ⊆ n m∈lines {b,p} ⊆ m shows m6=n proof (rule notI) assume m=n show False proof − have m6=l using assms(4,8)by auto moreover have l6=m−→ l∩m={} ∨ (∃q∈plane.l∩m={q}) using assms(1,7)A4 by auto ultimately have l∩m={} ∨ (∃q∈plane.l∩m={q}) by auto then show False proof (rule disjE) assume l∩m={} then show False using assms(2,6)hm=niby auto next assume ∃q∈plane.l∩m={q} 5.2. Geometr´ ıa simple 53 then obtain qwhere q∈plane ∧l∩m={q} by auto then have l∩m={q} by (rule conjE) then have {a,b} ⊆ {q} using assms(2,6,8)hm=niby auto then show False using assms(3)by auto qed qed qed Lema 5.2.6 Sea l una l´ınea tal que existen dos puntos {a,b} ⊆ l con a 6=b,un punto p tal que p /∈l.Sea n una l´ınea tal que {a,p} ⊆ n y m otra l´ınea tal que {b,p} ⊆ m.Supongamos adem´as que existen otros dos puntos c,d tales que pertenecen a n y m respectivamente y c 6=p. Entonces c 6=d. Demostraci´on: La demostraci´ on se har´ a por reducci´ on al absurdo, es decir, supongamos que c=dy llegaremos a una contradicci´ on. Tenemos todas las hip´ otesis del lema anterior, luego m6=n, por lo que podemos aplicar el axioma A4 a las l´ ıneas myn. Se tiene por lo tanto que m∩n=∅o existe un punto qtal que m∩n={q}. Primero supongamos que m∩n=∅, sin embargo por hip´ otesis se tiene que p∈m yp∈nluego hemos llegado a una contradicci´ on. Segundo sea qel punto tal que m∩n={q}. Como se ha supuesto que c=dse tiene que c,p⊆ {q}, pero por hip´ otesis se tiene que c6=pluego se ha llegado a una contradicci´ on. En los dos caso se ha llegado a una contradicci´ on, por lo que c6=d.  Para entender mejor la demostraci´ on se puede ver geom´ etricamente en la siguiente figura 5.4.8 54 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa Figura 5.2: Visi´ on geom´ etrica de la demostraci´ on de puntos diferentes La especificaci´ on y demostraci´ on del lema en Isabelle/HOL es la siguiente: lemma (in Simple-Geometry)how-to-produce-different-points: assumes l∈lines {a,b} ⊆ l a 6=b p/∈l n∈lines {a,p,c} ⊆ n m∈lines {b,p,d} ⊆ m p6=c shows c6=d proof assume c=d show False proof − have m6=n using assms how-to-produce-different-lines by simp moreover have n6=m−→ m∩n={} ∨ (∃q∈plane.m∩n={q}) using assms(5,7)A4 by auto ultimately have m∩n={} ∨ (∃q∈plane.m∩n={q}) by auto then show False proof (rule disjE) assume m∩n={} then show False using assms(6,8)by auto next 5.3. Geometr´ ıa no proyectiva 55 assume ∃q∈plane.m∩n={q} then obtain qwhere q∈plane ∧m∩n={q} by auto then have {p,d} ⊆ {q} using hc=diassms by auto then show False using hc=diassms(9)by auto qed qed qed 5.2.3 Interpretaci´on m´ınimo modelo geometr´ıa simple El m´ ınimo modelo que tiene la geometr´ ıa simple es considerar el plano como el conjunto formado por tres n´ umeros {a,b,c}, ya pueden ser enteros,naturales etc y con ellos formar ´ unicamente 3 l´ ıneas. En este caso ser´ ıan las combinaciones que se pueden hacer de 2 elementos de un conjunto de 2, es decir, 3. Para ello se va a dar el la definicion del planes-3 que es el plano de 3 elementos y lines-3 que es el conjunto formado por 3 l´ ıneas. definition plane-3 ≡ {1::nat,2,3} definition lines-3 ≡ {{1,2},{2,3},{1,3}} interpretation Simple-Geometry-smallest-model: Simple-Geometry plane-3 lines-3 apply standard apply (simp add:plane-3-def lines-3-def )+ done 5.3 Geometr´ıa no proyectiva 5.3.1 Entorno local La geometr´ ıa no proyectiva es un tipo de geometr´ ıa en el que asumimos paralelismo, en nuestro caso entre rectas. Definici´on 5.3.1 El paralelismo es una relaci´on que se establece entre dos rectas cualesquiera del plano, esta relaci´on dice que dos rectas son paralelas si bien son la misma recta o no comparten ning´un punto, es decir, su intersecci´on es vac´ıa. 56 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa Gracias a esta relaci´ on entre rectas, podemos definir un nuevo entorno local a˜ nadiendo al ya definido Simple-Geometry un nuevo axioma, el axioma de la existencia del paralelismo. Parallels-Ex: sea pun punto del plano y luna l´ ınea. Si p/∈lentonces debe existir una l´ ınea mtal que p∈myl∩m=∅. Al nuevo entorno local lo denotaremos como Non-Projective-Geometry. locale Non-Projective-Geometry = Simple-Geometry + assumes parallels-Ex: ∀p∈plane.∀l∈lines.p/∈l−→ (∃m∈lines.p∈m∧m∩l={} ) 5.3.2 Proposiciones de geometr´ıa no proyectiva A continuaci´ on vamos a presentar un lema sobre geometr´ ıa no proyectiva: Lema 5.3.2 Es falso que todo par de l´ıneas se cortan. Demostraci´on: La demostraci´ on se har´ a por reducci´ on al absurso. Es decir, supongamos que todo par de l´ ıneas se cortan. Sea ahora l1 una l´ ınea obtenida por el el lema 5.2.1. Porr el axioma A5 obtenemos un punto q1 tal que q1 /∈l1. Usando el axioma Parallels-Ex aplicado al punto q1ya la l´ ınea l1 obtenemos que existe una l´ ınea mtal que q1∈mym∩l=∅. Por lo tanto, hemos llegado a una contradicci´ on ya que se ha demostrado que existen dos l´ ıneas cuya intersecci´ on es vac´ ıa.  La formalizaci´ on y demostraci´ on en Isabelle/Hol es la siguiente: lemma (in Non-Projective-Geometry)non-projective: ¬(∀r∈lines.∀s∈lines.r∩s6={}) proof assume 4:∀r∈lines.∀s∈lines.r∩s6={} show False proof − obtain l1 where 1:l1 ∈lines using one-line-exists by auto then obtain q1 where 2:q1 ∈plane ∧q1 /∈l1 using A5 by auto then have q1 /∈l1 −→ (∃m∈lines.q1 ∈m∧m∩l1 ={} ) using 1 parallels-Ex by simp 5.4. Geometr´ ıa proyectiva 57 then obtain m1 where 3:m1 ∈lines ∧q1 ∈m1 ∧m1 ∩l1 ={} using 2by auto then obtain m1 ∩l1 6={} using 1 4 by auto then show ?thesis using 3by auto qed qed 5.3.3 Interpretacion modelo geometr´ıa no proyectiva El m´ ınimo modelo de la geometr´ ıa no proyectiva es considerar que el plano tiene 4 elementos; es decir, considerar el plano como {a,b,c,d}siendo estos n´ umeros enteros,naturales etc. Con estos 4 elementos para que sea un modelo de la geometr´ ıa no proyectiva hay que formar como m´ ınimo 6 rectas. Para ello vamos a dar la definicion plane-4 que es el plano formado por 4 elementos ylines-4 que son las l´ ıneas asociadas a estos elementos. definition plane-4 ≡ {1::nat,2,3,4} definition lines-4 ≡ {{1,2},{2,3},{1,3},{1,4},{2,4},{3,4}} interpretation Non-projective-geometry-card-4: Non-Projective-Geometry plane-4 lines-4 apply standard apply (simp add:plane-4-def lines-4-def )+ done 5.4 Geometr´ıa proyectiva 5.4.1 Entorno local La geometr´ ıa proyectiva es un tipo de geometr´ ıa que se basa en que dado cualquier par de rectas su intersecci´ on siempre es un punto. Para ello vamos a definir un nuevo entorno local Projective-Geometry tal que se basa en el entorno local ya definido Simple-Geometry a˜ nadi´ endole dos axiomas m´ as. Estos axiomas son los siguientes: 1. Cualquier par de l´ ıneas se cortan. 2. Toda l´ ınea tiene al menos 3 puntos. 64 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa shows l1 6=l2 proof assume 1:l1 =l2 have l∩l1 ={} ∨ (∃q∈plane.l∩l1 ={q}) using A4 assms(1,2,4)by auto then show False proof assume l∩l1 ={} then show False using assms(1,2)by auto next assume ∃q∈plane.l∩l1 ={q} then obtain twhere l∩l1 ={t} by auto then have {p,r} ⊆ {t} using assms(1,2,3)1by auto then show False using assms(5)by auto qed qed Lema 5.4.7 Para todo punto p en el plano, existen al menos tres l´ıneas que pasan por p. Demostraci´on: Sea pun punto del plano, usando el lema 5.4.5 se obitene que una l´ ınea htal que p/∈h. Usando la definici´ on equivalente del axioma A7 (lema 5.4.1) se obtienen tres puntos a,b,cdistintos entre s´ ı y tales que {a,b,c} ⊆ h. Por lo tanto, usando el axioma A3 obtenemos de forma equivalente tres l´ ıneas l,m,ntales que {a,p} ⊆ l,{b,p} ⊆ m,{c,p} ⊆ n. Ya hemos probado que existen 3 l´ ıneas que verifican las condiciones, lo ´ unico que queda por probar es que sean diferente. Usando el lema auxiliar 5.4.6 se concluye la prueba.  La siguiente figura 5.3 muestra una visi´ on geom´ etrica de la demostraci´ on anterior. 5.4. Geometr´ ıa proyectiva 65 Figura 5.3: Visi´ on geom´ etrica de la demostraci´ on del lema 5.3 La formalizaci´ on y demostraci´ on en Isabelle/HOL es la siguiente: lemma (in Projective-Geometry)three-lines-per-point: ∀p∈plane.∃lmn. distinct [l,m,n]∧ {l,m,n} ⊆ lines ∧p∈l∩m∩n proof fix p assume 1:p∈plane show ∃lmn.distinct [l,m,n]∧ {l,m,n} ⊆ lines ∧p∈l∩m∩n proof − obtain hwhere 2:h∈lines ∧p/∈h using 1 external-line by auto then obtain abc where 3:{a,b,c} ⊆ plane ∧distinct [a,b,c]∧ {a,b,c} ⊆ h using A7a by auto then obtain lwhere 4:l∈lines ∧ {a,p} ⊆ l using 1 A3 by auto obtain mwhere 5:m∈lines ∧ {b,p} ⊆ m using 1 3 A3 by auto obtain nwhere 6:n∈lines ∧ {c,p} ⊆ n using 1 3 A3 by auto have 7:h6=l using 4 2 by auto have a6=b using 3by auto then have 9:m6=l using 3 4 5 2 7 lineas-diferentes [ofhablpm]by simp 66 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa have 8:h6=m using 5 2 by auto have b6=c using 3by auto then have 10:m6=n using 6 5 3 2 8 lineas-diferentes [ofhbcmpn]by simp have a6=c using 3by auto then have 11:l6=n using 2 3 4 6 7 lineas-diferentes [ofhaclpn]by simp show ?thesis using 45691011by auto qed qed Para el siguiente lema se va a usar el siguiente lema auxiliar: Lema 5.4.8 Sea l y l1l´ıneas tales que l 6=l1y existen puntos p,q,c tales que {p,c} ⊆ l y {q,c} ⊆ l1con c 6=p. Entonces p 6=q Demostraci´on: La demostraci´ on se har´ a por reducci´ on al absurdo, es decir, supongamos que p=qy se llegar´ a a un absurdo. Supongamos que p=q. Entonces usando la hip´ otesis l6=l1 y el axioma A4 se obtiene que l∩l1=∅o existe un punto tal que l∩l1={q}. Veamos los dos casos por separado. 1. Supongamos que l∩l1=∅. Como por hip´ otesis se tiene que c∈lyc∈l1 entonces se llega a un contradicci´ on. 2. Supongamos que existe ttal que l∩l1={t}. Sin embargo, como hemos supuesto que p=q, se tiene que {p,c} ⊆ {t}. Pero como p6=cse llega a una contradicci´ on. En los dos casos se ha llegado a una contradicci´ on luego se tiene que p6=q.  La formalizaci´ on y demostraci´ on en Isabelle/HOL es la siguiente: lemma (in Projective-Geometry)puntos-diferentes: assumes l∈lines l1 ∈lines {p,c} ⊆ l {q,c} ⊆ l1 5.4. Geometr´ ıa proyectiva 67 l6=l1 c6=p shows p6=q proof assume 1:p=q have l∩l1 ={} ∨ (∃q∈plane.l∩l1 ={q}) using assms(1,2,5)A4 by auto then show False proof assume l∩l1 ={} then show False using assms(3,4)by auto next assume ∃q∈plane.l∩l1 ={q} then obtain twhere l∩l1 ={t} by auto then have {p,c} ⊆ {t} using assms(3,4)1by auto then show False using assms(6)by auto qed qed Lema 5.4.9 Existen al menos 7 puntos diferenetes en el plano. Demostraci´on: Primero sea luna l´ ınea que se obtiene usando el lema 5.2.1, usando el lema equivalente al axioma A7 (lema 5.4.1 ) se obtienen 3 puntos p1, p2, p3 distintos entre s´ ı tales que {p1, p2, p3} ⊆ l. Ahora usando el axioma A5 se obtiene que existe q tal que q/∈l, luego ya se tienen probado que existen 4 puntos diferentes, ya que qes diferente del resto porque q/∈l. Consideremos ahora tres l´ ıneas l1, l2, l3 obtenidas por el axioma A3 tales que {p1, q} ⊆ l1, {p2, q} ⊆ l2, {p3, q} ⊆ l3. Ahora vamos a obtener los tres puntos restantes, usando que l6=l16=l26=l3 gracias al lema auxiliar 5.4.6: 1. Obtenemos p4 tal que p4∈l1 y p4 /∈ {p1, q}usando el lema equivalente al axioma A7 (lema 5.4.2). Entonces veamos que p4 es diferente al resto de los puntos. Se tiene que p4 /∈ {p1, q}, luego veamos que p46=p2 y p46=p3. Usando el lema auxiliar 5.4.8 se tiene probado. Luego hemos probado que p4 es diferente al resto de los puntos. 2. Obtenemos p5 tal que p5∈l2 y p5 /∈ {p2, q}usando el lema equivalente al axioma A7 (lema 5.4.2). Entonces veamos que p5 es diferente al resto de los puntos, ya se 68 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa tiene que p5 /∈ {p2, q}luego falta por probar que p5 /∈ {p1, p3, p4}. Sin embargo es inmediato comprobar que se verifica usando el lema auxiliar ??, luego ya hemos probado que p5 es diferente al resto de los puntos. 3. Obtenemos p6 tal que p6∈l3 y p6 /∈ {p3, q}usando el lema equivalente al axioma A7 (lema 5.4.2). Entonces veamos que p6 es diferente al resto de los puntos, ya se tiene que p6 /∈ {p3, q}luego falta por probar que p6 /∈ {p1, p2, p4, p5}. Sin embargo es inmediato comprobar que se verifica usando el lema auxiliar ??, luego ya hemos probado que p6 es diferente al resto de los puntos. Por lo tanto, ya tenemos probado la existencia y la disparidad de 7 puntos: {p1, p2, p3, p4, p5, p6, p7}.  La siguiente figura 5.4 muestra una intuici´ on geom´ etrica de la demostraci´ on del lema 5.4.9. Figura 5.4: Visi´ on geom´ etrica de la demostraci´ on del lema 5.4.9 La formalizaci´ on y demostraci´ on del lema en Isabelle/HOL es la siguiente: lemma (in Projective-Geometry)at-least-seven-points: ∃p1 p2 p3 p4 p5 p6 p7. distinct [p1,p2,p3,p4,p5,p6,p7]∧ {p1,p2,p3,p4,p5,p6,p7} ⊆ plane proof − obtain lwhere 1:l∈lines using one-line-exists by auto then obtain xwhere 2:card x =3∧x⊆l using A7 by auto then have card x =3 by (rule conjE) 5.4. Geometr´ ıa proyectiva 69 then obtain p1 p2 p3 where 3:distinct [p1,p2,p3]∧x={p1,p2,p3} using construct-set-of-card3 [of x]by auto then have 4:{p1,p2,p3} ⊆ l using 2by auto then have 5:{p1,p2,p3} ⊆ plane using A2 1 by auto obtain qwhere 6:q∈plane ∧q/∈l using A5 1 by auto then have 7:distinct [p1,p2,p3,q] using 3 4 by auto obtain l1 where 8:l1 ∈lines ∧ {p1,q} ⊆ l1 using 5 6 A3 by auto then have 9:l1 6=l using 6by auto obtain p4 where 10:p4 /∈ {p1,q} ∧ p4 ∈l1 using A7b [of l1 p1 q]8by auto have 11:p4 6=p2 using 3 4 1 6 2 10 8 puntos-diferentes [of l1 l p4 p1 p2]by auto have 12:p4 6=p3 using 7 1 9 4 10 8 puntos-diferentes [of l1 l p4 p1 p3]by auto obtain l2 where 13:l2 ∈lines ∧ {p2,q} ⊆ l2 using 5 6 A3 by auto then obtain p5 where 14:p5 /∈ {p2,q} ∧ p5 ∈l2 using A7b [of l2 p2 q]7by auto have 15:l2 6=l using 6 13 by auto have 16:p5 6=p1 using 1 13 14 4 15 puntos-diferentes [of l l2 p1 p2 p5] by auto have 17:p5 6=p3 using 1 13 14 4 15 puntos-diferentes [of l l2 p3 p2 p5] by auto have 20:l1 6=l2 using 1 9 13 4 8 7 lineas-diferentes [of l p1 p2 l1 q l2 ] by simp have 21:p4 6=p5 using 13 8 14 4 10 20 puntos-diferentes [of l1 l2 p4 q p5] by auto obtain l3 where 22:l3 ∈lines ∧ {p3,q} ⊆ l3 70 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa using A3 5 6 by auto then obtain p6 where 23:p6 /∈ {p3,q} ∧ p6 ∈l3 using A7b by metis have 25:p6 6=p1 using 1 22 6 4 23 puntos-diferentes [of l3 l p1 p3 p6] by auto have 26:p6 6=p2 using 1 22 6 23 4 puntos-diferentes [of l3 l p2 p3 p6] by auto have 29:l1 6=l3 using 1 4 9 22 8 7 lineas-diferentes [of l p1 p3 l1 q l3] by simp have 31:p6 6=p4 using 22 8 10 23 29 puntos-diferentes [of l1 l3 p4 q p6] by auto have 34:l2 6=l3 using 1 4 13 22 15 7 lineas-diferentes [of l p2 p3 l2 q l3] by simp have 35:p6 6=p5 using 22 13 23 14 34 puntos-diferentes [of l2 l3 p5 q p6] by auto moreover have distinct [p1,p2,p3,p4,p5,p6,q] using 7 10 11 12 14 16 17 21 23 25 26 31 7 35 by auto moreover have {p1,p2,p3,p4,p5,p6,q} ⊆ plane using 6 5 A2 10 8 14 13 22 23 by auto ultimately show ?thesis by blast qed 5.4.3 Interpretaci´on modelo geometr´ıa proyectiva El m´ ınimo modelo que presenta la Geometria Proyectiva es considerar que el plano tiene 7 puntos y con ellos formar como m´ ınimo 7 l´ ıneas. Este modelo se conoce como el plano de Fano que es el plano proyectivo con el menor n´ umero de puntos y l´ ıneas necesarios para que se verifiquen todos los axiomas. Para ello vamos a dar la definici´ on en Isabelle del plano de 7 elementos plane-7 y la definici´ on lines-7 asociado a sus 7 l´ ıneas. La siguiente figura 5.5 muestra una visi´ on del plano de Fano: 5.4. Geometr´ ıa proyectiva 71 Figura 5.5: Visi´ on geom´ etrica del plano de Fano definition plane-7 ≡ {1::nat,2,3,4,5,6,7} definition lines-7 ≡ {{1,2,3},{1,6,5},{3,4,5},{5,7,2},{3,7,6}, {1,4,7},{2,4,6}} Para poder demostrar la existencia de este modelo m´ ınimo con el comando interpretation es necesario definir los siguientes lemas auxiliares: lemma aux1a:card {Suc 0,2,3}=3 by auto lemma aux1:∃x.card x =3∧x⊆ {Suc 0,2,3} using aux1a by blast lemma aux2a:card {Suc 0,6,5}=3 by auto lemma aux2:∃x.card x =3∧x⊆ {Suc 0,6,5} using aux2a by blast lemma aux3a:card {3::nat,4,5}=3 by auto lemma aux3:∃x.card x =3∧x⊆ {3::nat,4,5} using aux3a by blast lemma aux4a:card {5::nat,7,2}=3 72 Cap´ ıtulo 5. Teor´ ıa de geometr´ ıa by auto lemma aux4:∃x.card x =3∧x⊆ {5::nat,7,2} using aux4a by blast lemma aux5a:card {3::nat,7,6}=3 by auto lemma aux5:∃x.card x =3∧x⊆ {3::nat,7,6} using aux5a by blast lemma aux6a:card {Suc 0,4,7}=3 by auto lemma aux6:∃x.card x =3∧x⊆ {Suc 0,4,7} using aux6a by blast lemma aux7a:card {2::nat,4,6}=3 by auto lemma aux7:∃x.card x =3∧x⊆ {2::nat,4,6} using aux7a by blast interpretation Projective-Geometry-smallest-model: Projective-Geometry plane-7 lines-7 apply standard apply (simp add:plane-7-def lines-7-def )+ apply (intro conjI) apply (rule aux1) apply (rule aux2) apply (rule aux3) apply (rule aux4) apply (rule aux5) apply (rule aux6) apply (rule aux7) done end Ap´endice A Lemas de HOL usados En este ap´ endice se recogen la lista de los lemas usados en el trabajo indicando la p´ agina del libro de HOL donde se encuentra. A.1 Las bases de l´ogica de orden superior (2) A.1.1 L´ogica primitiva (2.1) A.1.1.1 Axiomas y definiciones b´asicas (2.1.4) • (p. 36) (P−→ Q)∧P Q(mp) • (p. 36) P Q P−→ Q(impI) • (p. 36) ^x.f x =g x f=g(ext) • (p. 36) s=t∧P s P t (subst) 73 80 Bibliograf´ ıa [13] Steven Roman. Lattices and Ordered Sets. Springer Science [14] Makarius Wenzel. The Isabelle/Isar Reference Manual. 2020. En http://isabelle.in. tum/doc/isar-ref.pdf. [15] Harold E. Wolfe. Introduction to Non-Euclidean Geometry. Courier Corporation, 2013.