Agda中的形式化射影几何

可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）61-77www.elsevier.com/locate/entcsAgda中构造射影几何的形式化吉列尔莫·卡尔德龙乌拉圭蒙得维的亚共和国大学摘要我们提出了一个形式化的证明辅助和编程语言Agda的射影几何。我们正式建设性的射影几何已被证明是适当的，以涵盖该地区的最传统的主题，只适用于建设性的有效方法的最新发展。 证明并形式化了它与其它著名的射影几何构造性公理系统的等价性。该实现涵盖了一个基本片段的直观合成射影平面几何，包括公理，对偶原理，Fano和Desargues属性和调和共轭。我们专注于一个说明性的例子，实现了一个复杂的和大的证明，出现部分和含糊地描述在文献中，即调和共轭的唯一性。最重要的细节，我们的实施进行了描述，我们展示了如何利用几个有趣的属性，如模块，依赖记录类型，隐式参数和实例，结果非常有助于减少典型的冗长的正式证明的Agda。保留字：证明助手，数 学 形式化，射影几何，类型论，Agda1介绍射影几何是研究点、线、面的关联性质的数学分支。典型的教科书相对于这一领域（例如[4，23]）涵盖的主题，如：axiomatisation的点和线和发病关系，原则的对偶性，定理的笛沙格和法诺，谐波共轭，projectivities，极性，二次曲线，等等。射影几何构成了一个非常优美的、完备的数学体系。它是由两个基本概念构成的：点和线以及它们之间的关联此外，一些公理决定了整个系统的行为。正因为如此，射影几何成为一个非常有吸引力的学科，在计算机系统中进行形式化。和一个有趣的案例研究，以调查与计算机形式化的数学所涉及的问题1 电子邮件地址：calderon@fing.edu.uyhttps://doi.org/10.1016/j.entcs.2018.10.0051571-0661/© 2018作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。62G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61尽管它的简单，射影几何被认为是一个统一的框架，为所有其他几何。射影几何中的每一个结果都可以应用于一个欧几里得几何，而欧几里得几何又可以归结为欧几里得几何。这个特征隐含在F. Klein [9]，其中射影几何被定义为研究射影下不变的性质另一方面，射影几何在计算机科学的不同领域有许多重要的应用，例如：计算机视觉，密码学，计算机图形学[3，6，2]。射影几何的计算机形式化将有助于解决这些领域的已知问题本文描述了构造性射影平面几何的计算机形式化。在第一个例子中，我们实现了Mandekern的论文[ 15 ]中提出的公理系统我们的形式化2是用Agda[19]编写的，Agda是一种基于直觉类型理论[17]的证明辅助和函数式编程语言特别是，我们关心的是一个编程工具，它可以帮助我们写一个舒适的方式，但不使用自动化的策略，在射影几何的形式证明的建设除其他外，构造方法还意味着完全不使用排中律原则。特别是，基本关系（特别是等式）的可判定性没有被假设。虽然使用构造性方法需要比非构造性方法更多的额外的证明，但我们有一个重要的优势：在构造性数学中，存在命题的证明总是通过给出构造证明的有效方法来进行的;即算法。该算法将与其正确性证明一起提供。总之，构造性射影几何的形式化可以提供正确算法的合成，以解决这一学科应用领域中的问题。另一方面，形式化的射影几何在阿格达可能是有用的，以验证某些证明在文献中给出的构造性。 由于Agda是基于直觉类型论的，我们可以得出结论，这些证明是按照构造性方法建立的。纲要本文的结构如下。在第二节中，我们给出了分离关系和setoid的形式化。第三节描述了投影平面的表示及其公理在Agda。在第四节中，给出了一种方法，证明了含有投影平面交函数和并函数的在第5节中，我们总结了在我们的形式化中开发的一些证明，特别是我们评论了对偶原理的实现。在第6节中，概述了Fano和Desargues属性的实现。在第七节中，我们描述了调和共轭的形式化及其存在唯一性的证明。最后，结论和相关工作2本文中描述的所有代码都可以从git存储库中免费获得：https://github.com/GuillermoCalderon/ProjecteGeometryInAgdaG. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）6163¬≡ ¬≈≈在第8节中讨论。2无隔性与构造性setoid在我们所遵循的射影几何的构造性表述中，需要将等式关系定义为从原始的分离关系（即不等式）导出。这种方法的详细解释见[24]和[15]。在本节中，我们将描述apartness和setoids的实现。集合A上的一个分离关系是A上的一个二元关系，它满足三个性质：不相关性、对称性3和互传递性。它在Agda中被实现为一个依赖记录，它以A和作为参数，其字段假定三个必需的属性：记录IsApartness{a b}{A：Seta}（__：A→A→Setb）：Set（aHb）where field不对称：<${x}→<$（xx）对称：<${x y} →xy→yx共传递性：<${x y}z→xy→zXzy为了得到一个尽可能一般的定义，我们认为A属于一个属类层次a的集合a。在形式化过程中，对所有对象都采用了类似的假设。我们将不会在本文的其余部分详细介绍这些级别。不熟悉Agda中宇宙多态性的读者[20]可以忽略它们而不会失去理解。请注意，有些参数被声明为隐式的（括在花括号中的参数）。隐式参数有一个很好的属性：在大多数情况下，我们可以省略这些参数，Agda将尝试从上下文中推断它们我们在实现中经常使用隐式参数我们将不解释为什么有些参数被声明为隐式的，而另一些则不是。一般来说，它是由实践给出的某种理论决定的平等的 我们定义了平等关系作为分离的否定：xy（x y）。这种方法与大多数射影几何公理化中所采用的方法略有不同（[7，15，24]），其中等式是一个原始概念，等式和分离之间的关系由一个额外的公理（紧密性）给出：如果（x y）则x=y。 紧性的反面来自于非紧性。这样，就在平等与对不平等的否定通过简单，我们得到了这个等价关系，将等式关系定义为非分离性的别名（没有将系统作为一个整体进行分离）正如预期的那样，证明了非分离性是一个等价关系。Setoid。 一个setoid是一个对，其中A是一个集合，上的分离关系[3]实际上，对称性并不是必需的，因为我们可以从另外两个性质中推导出它。然而，对称性通常包含在对分离性的定义64G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61⟨ ⟩→→→≈→≈∀S S答4：记录Setoida b：Set（（aHb））where field{运营商}：设置__：载波→载波→组bisApartness：IsApartness__在Setoid上的关系。为了使用setoids，我们需要在setoids上提升一些基于集合的操作。这个过程包括定义一个记录，它包含一个表示载体水平上的操作的字段，以及另一个断言操作与分离/相等关系相容的字段。在下面的代码中，_表示返回setoid载体的运算符。记录IsRel{a1b1a2b2c}（S1：Setoida1b1）（S2：Setoida2b2）（R：SetoidS1→SetoidS2→Setoidc）：集合（a1Hb1Ha2Hb2Hc），其中场声音：{a b c d}Setoid。S1aBSetoid_S2cdR a c R b d记录Rel{a1b1a2b2}c（S1：Setoida1b1）（S2：Setoida2b2）：Set（a1Hb1Ha2Hb2Hc）），其中，R： S1IsRel：IsRel12R平等与重写在setoids上的二元关系的领域声音，让位于一种构造证明的方法，即用等号替换保留关系的等号（也称为重写）。如果_da_是setoids之间的二元关系，并且我们有a1da b1的证明和a1<$a2和b1<$b2的证明，那么我们得到a2da b2的证明。我们引入了几个运算符，使我们能够模仿一个非常常见的模式，在非正式的数学符号。例如，表达式P=Q∈A=B代表P∈B的证明，只要我们有P=Q的证明，A=B且Q∈A。4我们使用Setoid这个名字来代表一个基于分离的setoid。 标识符Setoid被保留以表示经典的setoid，例如在Agda标准库中定义G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）6165∈/∈我们实现了两个用于重写的操作符，它们对关系的左（_联系我们 <${a1a2b}→a2<$a1→Ra1b→Ra2ba2__：{a1a2b}→Rba1→a1a2→Rba2Rba1a1a2=声音反射a1a2Rba1超载。我们需要同时使用多个setoids。为了重载不同setoids的apartness运算符，我们使用了一个名为instance arguments 5的Agda特性。这个想法相当简单：我们可以用一个特殊的指令打开Setoid模块：openSetoi d{[. ]}。这直接告诉我们访问模块Setoid的所有操作，并且我们可以省略特定的实例参数，该参数将由Agda通过特殊的实例解析算法从上下文中推断出来[5]。3表示射影平面在本节中，我们描述了根据[15]的射影几何公理系统在Agda中的实现。点、线和基本关系 射影平面几何的基本对象是构成setoid的点和线，即它们具有一种分离关系。此外，我们有关联关系（∈）和外部关系（/∈）。这两种关系都被假定为与平等相容。我们开始定义一个记录IsProjectivePlane，它构成了我们的射影几何形式化的主要结构。记录IsProjectivePlane{a b c d e}{Point：Setoida b}{Line：Setoidc d}（外部发生率：Rele点线）：集合（aHbHcHdHe），其中Incidence和Outside这两个名称很快就会被遗忘，因为我们将在载体的级别上使用原始关系。第一步是给出一些方便的定义，使我们能够访问结构的组件。点=点Line=线_∈_：点→线→集合e_∈_=相对R发生率_∈/_：点→线→集合e_∈/_=Rel.R外部5Agda的实例参数可以看作是Haskell类型类的等价物66G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61→/∈∈/∈ ∈→外部关系。在[15]和[7]中，外部关系是从关联关系和点分离性中肯定地（即没有否定）定义的：Pl（Q）（Ql）PQ。我们在形式化中采取了一种不同的方法：我们不给外部关系一个明确的定义。相反，我们添加一个公理（C0），断言Pl（Q）（Ql）PQ。这个蕴涵的逆命题没有被假设，但可以用其他公理证明。3.1射影平面在本节中，我们开始描述射影平面的公理，这些公理表示为记录IsProjectivePlane的场。公理C0在上一节中解释过：C0：n{Pl}→P∈/l→（n{Q}→Q∈l→PQ）第一组公理建立了一条线和它的外部点的存在（曼德尔克恩公理C1）。这些公理排除了射影平面P0：点l0：直线P0∈/l0：P0∈/l0下一组公理（C2和C3）表达了通过两个不同点的直线及其对偶（两条不同直线上的一个点）的存在性和唯一性的条件。在这里，分离的关系成为必不可少的，以确保存在一条线通过两个不同的点。加入：{P Q：Point}→PQ→线加入l：<${P Q} {PQ：PQ}→P∈joinPQ joinr：<${P Q} {PQ：PQ}→Q∈ joinPQ unq-join：<${PQ}（PQ：PQ）→ n{l} →P∈l →Q∈l →l∈连接PQ给出一个函数join，它接收两个点和它们的分离性证明函数joinl和joinr允许证明两点的连接确实通过它们。最后，函数unq-join断言所有通过两个点的直线都等于这两个点的连接注意与传统符号PQ的区别，以表示通过点P和Q的线。在我们的实现中，这条线由表达式（joinPQ）表示，其中PQ是P和Q不同的证明。6然而，在我们的实现中从未使用过相反的方法G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）6167/∈∈/∈∈我们类似地定义函数meet、metl、meetr和unq-meet，它们表示连接操作族的对偶部分为了排除射影平面（C4）的过于简单的模型，提出了一些公理然后假设在任何直线上存在三个不同的点点1点2点3：线→点∈-点1：l→点1l∈l∈-点2：l→点2l∈l∈-点3：l→点3l∈lJ点 ：100l→点1l点2L×点1l点3l×点2l点3l如果我们使用经典推理，很多命题可以从上面的公理推导出来这些结论中有几个在建设上是站不住脚的。因此，为了得到一个有用的系统，同时保持其构造性基础，有必要增加一些其他公理我们保留曼德尔克恩公理C5允许推断两条线是不同的，如果一个点属于其中一条线并且在另一条线之外。反过来，C6在和之间建立了强关系。最后一个公理C7提供了关于两条直线相交唯一性的另一种观点，但涉及而不是。它具有特殊性，其结论是一个析取C5：n{lmP}→P∈l→P∈/m→lmC6：<${Pl}→<$（P∈/l）→P∈lC7：n{lmP}→（lm：lm）→P满足lm→P∈/lP∈/mC6的逆很容易证明。3.2与其他公理系统的自从Heyting [7]的开创性工作以来，人们给出了几个不同的系统来以可接受的构造性方式定义射影几何。在这里，我们研究了我们的形式化（主要基于[15]，这反过来又类似于海廷的公式）与von Plato [ 24 ]和van Dalen [ 22 ]给出的形式化之间冯·柏拉图体系为所有的几何定义了一个核心，这就是所谓的分离几何。在这种方法中，所有通常的消极关系都被认为是原始的和积极的。然后，（点和线的）分离关系和外部关系被认为是给定的，而相等关系和关联关系被定义为这些原始关系的相应否定。公理的集合是非常简单和对称的。其中有几个有分离的结论。我们给出了一个形式证明，证明我们在第3节中定义的每一个射影平面构成了柏拉图意义上的无偶射影几何反之则需要在von Plato系统中加入一些假设非简并条件的公理（如Mandelkern的公理C1和C4有了这个补充，我们正式68G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61/∈≈≈柏拉图式的射影几何与曼德尔克恩射影平面的对应另一方面，范达伦描述了一个公理系统的射影几何，其中唯一的原始关系是外部关系（）。系统的所有其他二元我们实现了与我们的范达伦的系统的等价性证明我们认为这些等价非常重要和有用，因为它们允许我们自由地处理不同的公理集合。我们对每个公理系统的实现在Agda中被表示为一个依赖记录。因此，我们可以通过导入相应的模块来提供任何系统4用join和meet进行函数join和meet允许构造表示点的复杂表达式。通常，我们会发现不同的表达式（join和meet的组合）表示同一个对象（点或线）。这一事实的原因依赖于由函数unq-join和unq-meet表示的唯一性属性。下面，我们给出一些代数规则，表达用join和meet构造的表达式之间的等式。我们使用一个简化的符号：ABq表示形式为（joinA B q）的表达式，其中q是A B的证明。子索引q在不相关时被省略。公司简介ABp ABq AB BAA1A2B1B2A1B1A2B2琼公A1A2B1B2A1B1B2A2联系我们图1.一、等式推理规则我们有两个见面的规则。我们实现简单的功能，允许证明这些代数方程在一个相当直接的方式。这个实现的一个有趣的特性是，这些函数的所有参数都是隐式的。因此，我们可以以一种非常直接的方式组合函数，由规则的简单直觉指导此外，这些运算符可以与Agda的EqReasoning库（[18]，[1]）的运算符一起工作，提供了一个很好的语法来编写一些相等的证明。玩弄这个系统，人们很快就会发现，大多数证明都遵循在某些几何对象之间建立关系的模式（任何基本关系，分离，平等，关联和外部）。因此，所需的公理被调用，并且通常我们需要应用重写以获得涉及正确对象的关系。重写的重载运算符和第4节中描述的等式的组合子被广泛用于我们系统中的证明构造。G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61695命题与对偶一旦我们用投影平面的定义和setoids和方程推理的库实现了前面的模块，我们就可以构建命题的证明，例如[15]第2节和大多数传统书籍中出现的证明。我们还提供了一个正式的证明的原则，对偶被认为是最典型的结果之一的射影几何。这一原则的经典表述是：对于每一个有效命题，是从第一个将单词“线”换成“点”，“通过”换成“谎言”得到的。这个非正式的陈述与其说是一个几何命题，不如说是一个元定理。然而，它可以以一种非常简洁的方式形式化，就像投影平面之间的函数一样。二元性：{a b c d e}{点：Setoida b}{线： Setoidc d}{∈∈/：RelePointLine}→IsProjectivePlane∈∈/→IsProjectivePlane（ip∈）（ip∈/）这个函数的作用是交换setoids上二元关系的参数顺序。对偶原理的证明表明如何从一个给定的射影平面构造一个对偶射影平面6法诺和笛沙格在平面射影几何中，经典的Fano定理和Desargues定理是无法证明的。因此，我们假设它们是新的公理。更确切地说，我们通过添加代表这些公理的场来定义先前定义的射影平面的扩展。法诺公理是关于四边形的，而笛沙格是关于三角形的。四边形和三角形是一种称为完全n点的图形的实例。我们在实现中定义了这些概念，为模块提供了必要的工具，使它们能够轻松地工作我们定义了一个结构FanoProjectivePlane作为结构ProjectivePlane的扩展，通过添加一个代表Fano公理的新字段。反过来，另一种结构Desargues的获得作为FanoProjectivePlane 的 扩 展 ， 其 具 有 对 应 于Desargues 公 理 的 场 。 通 过 证 明Fano 和Desargues公理的对偶形式，将在射影平面上证明的对偶原理推广到新定义的结构上虽然概念上很简单，但这些证明是相当广泛和冗长的（大约有一千行Agda代码）。在这些模块中实现了一些有趣的数学机制，以便适当地处理所涉及的那种数字的对称性和圆形性。我们没有提供对这部分实现的详细解释，感兴趣的读者可以在存储库中查阅。70G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61图二. C关于A和B的7调和共轭调和共轭可以在欧几里得几何中用度量概念（交比）来定义。von Staudt [25]是第一个提出基于四边形的综合定义的人。我们遵循[15]中给出的定义，它更好地实现了所需的构造性，因为定义在基线的所有点上都是一致的。7.1调和共轭假设两个不同的点A和B。设C是直线AB上的任意点。 C关于A和B的调和构形由一条经过C且与AB不同的直线l和一个在l和AB之外的点R决定。从直线l和点R，我们可以构造一个点D，它被称为C关于A，B的调和共轭。求C的共轭的方法如下：设Q是l和AR的交集。 设P是l和BR的交集。 设S是AP和BQ的交集，那么， C关于A和B的调和共轭（相对于构型（l，R））是点D=RSAB。为了有一个有效的定义，我们必须证明所有的步骤都是明确定义的，即所有的连接和相交都应用于不同的点和线。在我们的形式化中，这是由Agda类型检查器强制执行的，因为函数join和meet需要作为所涉及对象的独立性的证明例如，要引用直线AR，我们需要证明AR，要考虑l和AR的交集，我们需要证明l AR，等等。谐波配置。给定A和B两个不同的点，C是AB上的一个点，C的调和构形是从l和R的特定选择中构造的（遵循上述方法）直线和点的集合，以获得点D（C关于A和B的调和共轭）。我们将谐波配置表示为记录：记录HarmonicConf{A B} {AB：AB}{C}（C∈AB：C∈joinAB）：集合（aHbHcHdHe），其中G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）6171∈∈→∈→∀∈∈菲尔德l：线C l：Cll AB： l加入ABR：点R∈/l：R∈/lR∈/AB：R∈/joinAB上面的代码显示了记录HarmonicConf的字段，即线l和点R以及它们必须满足的条件在同一个模块HarmonicConf中，我们定义了构造调和共轭所需的点和线，以及调用的每个连接和相交的不相容性的必要证明。特别是，四边形的点（见下文）是这样定义P Q S D：点P=满足RB 1 Q=满足RA 1S=符合AP BQ D=符合RS AB表示谐波共轭。根据前面的发展，调和共轭被定义为从给定配置返回一个点的函数：H共轭：{A B C：点}{AB：AB}{C AB：CjoinAB}HarmonicConfCABPointH共轭HC=HarmonicConf.DHC注意，唯一明确的参数是对应于调和配置的结构（记录）。在这个记录中，我们给出了点D的构造，它是为构形选择的场所有其他参数都是隐式的，它们将从参数HC推断出来。四边形和调和共轭。通常用四边形来定义调和共轭。在这样的定义中，四边形PQRS以这样的方式构造，即线QR和PS在A中相遇，线PR和QS在B中相遇，并且线PQ通过C。 然后，C关于到A和B的距离是线RS和AB的交点。这种结构只有在C既不与A也不与B重合时才是可能的。由于这个原因，我们遵循[15]中给出的定义，其中我们不需要确定C是否等于A或B来定义调和共轭。7.2调和共轭的存在性调和共轭的存在性在标准文献中没有任何证明而被普遍承认。根据我们的建设性做法，我们必须72G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61¬⊥提供了一种方法，从任何给定的点A、B和C构造至少一个谐波配置。简体中文{A B C：点}{AB：AB}→（C∈AB：C∈joinAB）→HarmonicConfC∈AB通过公理C4对偶，我们可以得到两条不同的直线经过C。通过共输性，这些线中至少有一条不同于AB。然后，我们有所需的线l经过C，与AB不同。在AB和l之外的点R的存在性更难证明。它还遵循公理C4和共传递性的适当组合。7.3调和共轭根据上面的定义，给定点关于A和B的共轭将取决于所选的线l和点R（即所考虑的构型）。射影几何中的一个主要结果是调和共轭不依赖于所选择的构形。换句话说，如果我们考虑两个构型HC和HCJ，则分别使用HC和HC'获得的共轭D和DJ唯一性：（A B C：点）→（AB：AB）→（C∈AB：C∈joinAB）→（HC HC→HConjugateHC→HConjugateHC构造这个证明是本文的主要目标。我们将为了解释构造这个形式证明所使用的一般方案，并更详细地说明某些部分7.3.1案例的建设性证明在经典数学中，利用排中律的某些变体来构造证明是很常见的。如果我们从假设证明一个命题φ，我们也从假设证明φ，那么我们有一个证明φ（在没有假设的情况下）。如果我们正在建设性地工作，并且不接受LEM作为一般有效原则，则此方法无效。然而，在我们想要证明一个矛盾（）的特殊情况下，我们可以如下进行：从假设φ，证明一个矛盾，从假设φ，证明一个矛盾。我们有一个证据（没有假设）。第一个矛盾给出了<$φ的证明，并取消了假设φ。 第二个矛盾接受了<$φ的这个证明，并给出了荒谬性（）的证明。这种方法可以推广到任意数量k个前提，这些前提在序列中被矛盾抵消。设φ1，...，φk是假设的集合。G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）6173⊥⊥图3.第三章。两个谐波配置。完全不相交四边形的情形我们必须依次提供（k+ 1）个证明。在每一步中，我们用否定来取消一个前提。最后，我们得到了一个独立于假设φ1，…， φk。在下一节中，我们将解释如何将这种推理模式应用于构造调和共轭唯一性的证明7.3.2唯一性的证明在这一节中，我们将解释唯一性证明是如何在Agda中构造和这是一个相当广泛的证明，它考虑了许多不同的情况，以涵盖所有的可能性7。该证明采用如上定义的点A、B和C以及两个谐波配置HC和HC '作为输入。设D和DJ分别是关于HC和HC'的调和共轭我们想构造一个DDJ的证明，它被定义为D DJ的否定。换句话说，D<$DJ的证明是通过假设D DJ并从这个假设导出一个矛盾而得到的。除了D DJ的全局假设之外，我们还加入了几个额外的假设，这些假设使我们能够通过前面一节中解释的案例来证明矛盾。该等假设与HC及HC'的配置有多明显有关例如，我们将描述两个配置完全不相交的情况的证明我们需要11个假设来确定这个情况：C素八早午晚餐lJ，RRJ，RJ/∈RB，RJ/∈RA，SPSJPJ，SQSJQJ，O/∈RS，O/∈RJSJ，SSJ.注意，所有的前提都是分离（__）或外部（_/∈_）关系的情况这一点很重要，因为从A B的否定中我们可以推出A∈B（通过定义），而A/∈r的否定必然导致A∈r（通过公理C6）。7证明的完整代码包括大约5000行，分布在大约15个 文件中。74G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61≈∩联系我们联系我们第一个和第二个假设确保了两种配置的四边形的存在。条件l lJ允许推出P PJ和QQJ。 从RJRB和RJ我们可以证明三角形PQR和PJQJRJ是从AB轴的透视图。相反，通过Desargues，PQR和PJQJRJ是从中心透视的。设O=PPJ<$QQJ这个透视中心。三角形PQS和PJQJSJ也是从AB轴透视的（使用假设SP SJPJ和SQ SJQJ）。根据笛沙格的逆命题，这些三角形是由一个中心透视的。可以直接看出这个中心等于O。我们可以得出结论，三角形PRS和PJRJSJ是从中心O透视的（需要假设O RS，ORJSJ和S SJ）现在应用Desargues，这些三角形也是从轴透视的。我们可以很容易地确定这个轴是AB线，因此DDJ=RSRJSJ。 从一般的假设D DJ，我们得到了这种情况下的矛盾在大多数的射影几何书籍中，这种情况通常被作为调和共轭唯一性的完整证明。此外，一些必要的前提（如涉及点O的前提）被省略了。Veblen和Young [23]提出了一个类似上述的证明。他们认为，对于HC的顶点或边与HCJ的顶点或边重合的情况，我们可以考虑第三种构型HCJ J，其顶点和边与HC和HCJ的顶点和边不同。因此，我们可以将前面的证明应用于配置HC和HCJJ，然后应用于配置HCJ和HCJJ。利用传递性，导出了D与DJ如果我们想形式化这个论证，我们必须给出一个构造第三种配置的方法。此外，我们应该为前面的假设之一失败的几种情况中的每一种就建设性办法而言，这项任务似乎相当复杂8。反过来，Coxeter关于构造性方法，Heyting [7]在空间的射影几何的背景下给出了基于四边形的调和共轭定义，提供了一种仅适用于与基点（A和B）不同的点的构造同时，Mandelkern [15]的证明在构造矛盾序列时不够严密，[16]也有不准确之处。除了基于11个假设的证明之外，在我们的实现中，我们还考虑了更多的情况，一次一个地依次否定假设。对于每一种情况，我们必须得到一个矛盾。在某些情况下，矛盾是相当明显的，而在另一些情况下，则需要相当大的努力才能推导出它。大多数情况下，我们通过Desargues的一些应用获得所需的结果，就像我们对不相交构形所做的那样在许多情况下，可以利用构形的对称性，并重新使用已经为类似情况给出的证明[8]请注意，如果我们考虑一个嵌入射影空间的平面，那么获得第三种构形所需的方法就变得微不足道了。G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61758结论和相关工作我们已经描述了一个形式化的基本片段建设性的射影平面几何，其中包括：基本对象和关系的表示，射影平面的定义及其公理，关联的基本命题，对偶原理，完全n点的定义，Fano和Desargues公理的表示及其对偶公式的证明，调和共轭的定义及其存在唯一性的证明。该实现仅限于使用来自构造性数学的有效方法。我们实现了[15]中描述的公理系统，并有一些小的变体。此外，还证明了它与其他公知的构造性公理系统的等价性。调和共轭唯一性的证明，如果仅仅用构造性有效的方法来证明，是一个相当复杂的问题。事实上，我们无法在文献中找到完整而严格的证明。因此，一个正式的和机器检查的建设这样的证明构成了本文的主要贡献。我们的开发基于Agda的编程语言功能特别是，我们没有通过策略来构造证明。我们利用了该语言的一些重要特性。模块和依赖记录类型扮演了重要的角色，允许我们将setoids实现为抽象数据类型，并将线和点视为此ADT的实例。此外，隐式实例的机制提供了重载该ADT的运算符的能力。我们几乎不需要任何额外的数据类型：只使用自然数和无穷集合来定义完整的n点。关于实现中涉及的逻辑：我们使用了一阶直觉主义逻辑的标准连接词，即蕴涵、否定、析取、合取和量化器。归纳和递归在我们的实现中很少使用这对于类型论中的形式化来说是相当不寻常的，但是在主要对象是ADT而不是归纳定义的数据类型的情况下，这是合理的因此，模式匹配很少使用（仅用于处理析取和有限集合）。我们工作的目标之一是实现一个框架，在这个框架中，人们可以很容易地构造射影几何的证明，而不需要使用自动策略。我们所说的换句话说，我们希望与纸质证明相比，减少形式证明的复杂性。我们已经得到了非常优雅和简单的证明，结合了我们的实现提供的运算符（例如，重写、连接-满足规则、等式推理、配置的循环）。然而，一些证明（即：Desargues一个法诺定理和调和共轭的唯一性）是过于冗长相比，他们的教科书版本。需要一些额外的工作来降低这种复杂性。我们推测，对我们实现的一些基本模块进行适当的重新设计将有助于实现这一目标。此外，某种自动化将有助于避免样板76G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）61代码（例如线和点的相等性证明）。相关工作。据我们所知，在Agda中没有其他形式化的几何（任何形式）在Alf（Agda的祖先）[13]中，存在由von Plato [24]编写的早期形式化。这是一个非常简单的形式化的冯柏拉图公理系统。一个更高级的实现是[8]，它在Coq中形式化了von Plato构造性几何。这些工作只是射影几何的一小部分，没有涉及到诸如Desargues定理和调和共轭等高级概念然而，它们对线/点的存在性和唯一性使用相同的表示：函数join和meet的定义与我们的实现相同。分离关系的定义也非常相似。如果我们把自己限制在类型论中的射影几何形式化，我们应该提到Magaud，Narboux和Schreck的工作[11，12]。他们描述了合成射影几何的基本概念的Coq实现，使用基于策略的方法来构造证明。它们涵盖了一些复杂的定理，如笛沙格和对偶原理。有一些共同点与我们的形式化，即表示的投影平面作为一个记录和证明的对偶性进行了记录之间提供一个功能。主要的和资本的区别是，他们的形式化不遵循一个纯粹的建设性的方法，因为发病率和平等关系被假定为可判定的。最后，我们注意到，我们不知道任何形式化的射影几何覆盖的调和共轭领域。未来的工作。这项工作是一个更雄心勃勃的项目的一部分，包括在一个完整的正式建设性射影几何。未来的主题将涵盖：射影和二次曲线。此外，还有许多有趣的相关问题需要研究，例如：射影几何与一个射影几何的关系，即扩张问题（[21]，[14]）;射影平面坐标化的实现;与射影几何的代数模型如Grassman-Cayley代数，几何代数等的关系[10 ]第10段。确认我要感谢阿尔贝托·帕尔多和匿名裁判的有益评论。我也感谢M。曼德尔克恩对他的工作有益的意见建设性射影几何。引用[1] Agda developers，Agda标准库，http://wiki.portal.chalmers.se/agda/pmwiki.php/Libraries/StandardLibrary，[发布日期：2017-04-05].[2] Beutelspacher，A.和联合罗森鲍姆，“射影几何-从基础到应用。剑桥大学出版社，1998年，I-X，1-258页。[3] Birch field，S.，An Introduction to Projective Geometry（for Computer Vision），http：//robotics. stanford.edu/~birch/projective/（1998），访问日期：2017年。G. Calderón/Electronic Notes in Theoretical Computer Science 338（2018）6177[4] Coxeter，H.S. M.，[5] Devriese，D.和F. Piessens，On the bright side of type classes：instance arguments in Agda，in：Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming，ICFP 2011，Tokyo，Japan，September 19-21，2011，pp.143-155[6] 赫 尔 曼 岛 “The use of projective geometry in computer graphics,” Springer-Verlag Berlin ; New York,1992, ：pp.[7] Heyting，A.， 投影几何的直观公理，数学年鉴98（1928），pp. 491-538.[8] Kahn，G.，根据扬·冯·柏拉图，科克贡献的构造几何。Coq5（1995），p.10.[9] 克莱因，F.，[10] Li，H.，[11] Magaud ， N. ， J. Narboux 和 P.Schreck， Formalizing projective plane geometry in Coq ， in ：Automated Deduction in Geometry-7th International Workshop，ADG 2008，Shanghai，China，September 22-24，2008. 2008年修订，pp。141-162.[12] Magaud，N.，J. Narboux和P. Schreck，Coq中形式化射影几何的案例研究：Desargues定理，Comput。45（2012），pp. 406-424[13] 马 格 努 松 湖 和 B. Nords