Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Mathematik » Logik, Mengen & Beweistechnik » LEAN und Reiterationsregel
Autor
Universität/Hochschule LEAN und Reiterationsregel
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Themenstart: 2021-10-05

Hallo allerseits, tactac hat die folgende Doku empfohlen: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf Darin kommt auch das Kalkül des natürlichen Schliessens vor. (und eine kleine Einführung in LEAN). Warum fehlt unter den Regeln des natürlichen Schliessens die Reiterationsregel? Diese wird doch (zumindest implizit) in den Beispielen verwendet? Mir ist auch nicht klar, wie die Fitchschreibweise mit den Beispielen (in dem o.g. Skript) korrespondiert. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.1, eingetragen 2021-10-05

\quoteon(2021-10-05 13:12 - carlox im Themenstart) Hallo allerseits, tactac hat die folgende Doku empfohlen: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf Darin kommt auch das Kalkül des natürlichen Schliessens vor. (und eine kleine Einführung in LEAN). Warum fehlt unter den Regeln des natürlichen Schliessens die Reiterationsregel? \quoteoff Man braucht sie eigentlich nicht. \quoteon Diese wird doch (zumindest implizit) in den Beispielen verwendet? \quoteoff Wo wird sie denn implizit verwendet? \quoteon Mir ist auch nicht klar, wie die Fitchschreibweise mit den Beispielen (in dem o.g. Skript) korrespondiert. \quoteoff "3.1 Derivations in Natural Deduction" beschreibt die Mechanik ja eigentlich recht gut. Sehr direkt und einfach beschreibbar ist die Korrespondenz zur Fitch-Schreibweise nicht. Eine solche zu finden ist aber für Lean unnötig. In Lean braucht man eine Entsprechung der Reiterationsregel ebenfalls nicht.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.2, vom Themenstarter, eingetragen 2021-10-06

\quoteon(2021-10-05 20:37 - tactac in Beitrag No. 1) "3.1 Derivations in Natural Deduction" beschreibt die Mechanik ja eigentlich recht gut. Sehr direkt und einfach beschreibbar ist die Korrespondenz zur Fitch-Schreibweise nicht. Eine solche zu finden ist aber für Lean unnötig. In Lean braucht man eine Entsprechung der Reiterationsregel ebenfalls nicht. \quoteoff Ich kannte bisher nur einen Kalkül, den ich wie folgt informal beschreibe: Ein Beweis ist eine Folge von Formeln, an dessen Ende die zu beweisende Formel steht. Jedes Folgenglied ist entweder ein Axiom oder geht mittels einer der Regeln aus früheren Folgendgliedern hervor. Im Kalkül des natürlichen Schliessens geht das anders: Es gibt keine Axiome und es geht nicht notwendig jedes Folgenglied aus früheren Folgengliedern durch Anwendung einer Regel hervor. Beispiel mit der Regel or.elim(A or B) Folge1: A,...,C beweist C Folge2: B,...,C beweist C Man kann daraus _eine_ Folge machen: A,...,C, B,...,C aber man darf in der Teilfolge B,...,C nicht mittels einer Regel aus früheren Folgengliedern (aus A,...,C) neue Folgenglieder in der Teilfolge B,...,C konstruieren. Ist das korrekt? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.3, eingetragen 2021-10-06

\quoteon(2021-10-06 11:27 - carlox in Beitrag No. 2) \quoteon(2021-10-05 20:37 - tactac in Beitrag No. 1) "3.1 Derivations in Natural Deduction" beschreibt die Mechanik ja eigentlich recht gut. Sehr direkt und einfach beschreibbar ist die Korrespondenz zur Fitch-Schreibweise nicht. Eine solche zu finden ist aber für Lean unnötig. In Lean braucht man eine Entsprechung der Reiterationsregel ebenfalls nicht. \quoteoff Ich kannte bisher nur einen Kalkül, den ich wie folgt informal beschreibe: Ein Beweis ist eine Folge von Formeln, an dessen Ende die zu beweisende Formel steht. Jedes Folgenglied ist entweder ein Axiom oder geht mittels einer der Regeln aus früheren Folgendgliedern hervor. Im Kalkül des natürlichen Schliessens geht das anders: Es gibt keine Axiome und es geht nicht notwendig jedes Folgenglied aus früheren Folgengliedern durch Anwendung einer Regel hervor. Beispiel mit der Regel or.elim(A or B) Folge1: A,...,C beweist C Folge2: B,...,C beweist C Man kann daraus _eine_ Folge machen: A,...,C, B,...,C aber man darf in der Teilfolge B,...,C nicht mittels einer Regel aus früheren Folgengliedern (aus A,...,C) neue Folgenglieder in der Teilfolge B,...,C konstruieren. Ist das korrekt? mfg cx \quoteoff Im Fitch-Stil ist das ungefähr so (was "Man kann daraus _eine_ Folge machen:" soll, ist mir schleierhaft). Bei der Oder-Elimination ist es aber so, dass man einen neues Folgenglied mit der Aussage C anfügen darf mit der Begründung: Oder-Elimination mit Folge1, Folge2 und Nummer k, wobei an Nummer k die Aussage (A or B) steht, und k an einer zugreifbaren Stelle steht, also u.a. nicht in einer der beiden Folgen Folge1 und Folge2, oder anderen "eingerückteren". Manchmal malt man um soetwas wie Folge1: A,...,C auch ein Kästchen, und die Regel ist dann eben: man darf Zeilen daraus nicht von außen referenzieren, wohl aber den Block als ganzes (bei oder-Elimination und Implikationseinführung zum Beispiel.) Wenn die Ableitungen als Bäume geschrieben werden, kann man statt Zeilenreferenzierungen etwas anderes verwenden -- eben die Form der Bäume. Eine Ableitung von C per Oder-Elimination hätte an der Wurzel die Aussage C, und 3 Teilbäume: einer ist eine Ableitung von (A oder B), einer eine Ableitung von C unter der temporären Annahme von A, und einer eine Ableitung von C unter der temporären Annahme von B.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.4, vom Themenstarter, eingetragen 2021-10-07

\quoteon Im Fitch-Stil ist das ungefähr so (was "Man kann daraus _eine_ Folge machen:" soll, ist mir schleierhaft). \quoteoff In dem man Folge1 an Folge2 anfügt: Folge1: A,...,C beweist C Folge2: B,...,C beweist C also Gesamtfolge: A,...,C, B,...,C \quoteon Wenn die Ableitungen als Bäume geschrieben werden, kann man statt Zeilenreferenzierungen etwas anderes verwenden -- eben die Form der Bäume. Eine Ableitung von C per Oder-Elimination hätte an der Wurzel die Aussage C, und 3 Teilbäume: einer ist eine Ableitung von (A oder B), einer eine Ableitung von C unter der temporären Annahme von A, und einer eine Ableitung von C unter der temporären Annahme von B. \quoteoff Ok, ich verwende also Bäume. \quoteon In Lean braucht man eine Entsprechung der Reiterationsregel ebenfalls nicht. \quoteoff Wie kannst du aber folgendes Beispiel als Baum darstellen, ohne die Reiterationsregel zu verwenden? theorem myTheorem_1 (A B C : Prop) : A→((B→(A∧B)) ∧ (C→(A∧C))) := (assume h : A, and.intro (assume : B, -- show A∧B, from and.intro (‹A› ‹B›) -- show A∧B, from and.intro (h ‹B›) show A∧B, from and.intro h ‹B› ) (assume : C, -- show A∧C, from and.intro ‹A› ‹C› -- show A∧C, from and.intro (h ‹C›) show A∧C, from (and.intro h ‹C›) ) ) Der Baum müsste also so aussehen: (Bem: H_... bedeutet Hypothese) Hier kommt also H_A zwei Mal vor, weil die Reiterationsregel verwendet wurde. Wo ist mein Denkfehler? H_A H_A H_B H_C A and B A and C B -> A and B C -> A and C (B -> A and B) and (C -> A and C) A -> (B -> A and B) and (C -> A and C) Eine Frage noch: Mit der And-Einführungsregel kann man folgende Beweisfolge konstruieren: A,B,A and B Wie kann man aber ohne Reiterationsfolge die folgende Beweisfolge konstruieren: A,A mfg cx mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.5, eingetragen 2021-10-07

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-07 20:12 - carlox in Beitrag No. 4) \quoteon Im Fitch-Stil ist das ungefähr so (was "Man kann daraus _eine_ Folge machen:" soll, ist mir schleierhaft). \quoteoff In dem man Folge1 an Folge2 anfügt: Folge1: A,...,C beweist C Folge2: B,...,C beweist C also Gesamtfolge: A,...,C, B,...,C \quoteoff Wichtig ist, dass das zwei Teilfolgen sind, die miteinander und dem darumherum nicht viel zu tun haben. \quoteon \quoteon Wenn die Ableitungen als Bäume geschrieben werden, kann man statt Zeilenreferenzierungen etwas anderes verwenden -- eben die Form der Bäume. Eine Ableitung von C per Oder-Elimination hätte an der Wurzel die Aussage C, und 3 Teilbäume: einer ist eine Ableitung von (A oder B), einer eine Ableitung von C unter der temporären Annahme von A, und einer eine Ableitung von C unter der temporären Annahme von B. \quoteoff Ok, ich verwende also Bäume. \quoteon In Lean braucht man eine Entsprechung der Reiterationsregel ebenfalls nicht. \quoteoff Wie kannst du aber folgendes Beispiel als Baum darstellen, ohne die Reiterationsregel zu verwenden? theorem myTheorem_1 (A B C : Prop) : A→((B→(A∧B)) ∧ (C→(A∧C))) := (assume h : A, and.intro (assume : B, -- show A∧B, from and.intro (‹A› ‹B›) -- show A∧B, from and.intro (h ‹B›) show A∧B, from and.intro h ‹B› ) (assume : C, -- show A∧C, from and.intro ‹A› ‹C› -- show A∧C, from and.intro (h ‹C›) show A∧C, from (and.intro h ‹C›) ) ) Der Baum müsste also so aussehen: (Bem: H_... bedeutet Hypothese) Hier kommt also H_A zwei Mal vor, weil die Reiterationsregel verwendet wurde. Wo ist mein Denkfehler? H_A H_A H_B H_C A and B A and C B -> A and B C -> A and C (B -> A and B) and (C -> A and C) A -> (B -> A and B) and (C -> A and C) \quoteoff Ja. Dass man Hypothesen mehrfach angibt, ist normal. Mit einer Syntax näher an der im Skript: \sourceon ASCII-Art [A]^1 [B]^2 [A]^1 [C]^3 ------------- ------------- A∧B A∧C ------- 2 ------- 3 B→(A∧B) C→(A∧C) ------------------------ (B→(A∧B)) ∧ (C→(A∧C)) ------------------------- 1 A→((B→(A∧B)) ∧ (C→(A∧C))) \sourceoff Bei der Implikationseinführung darf man beliebig viele temporäre Annahmen der Voraussetzung in den Unterbäumen "entwerten" (in obiger Notation mit den Nummern und eckigen Klammern markiert). Sind nicht alle Annahmen entwertet, hat man etwas mit globalen Annahmen hergeleitet. Im Beispiel, wenn wir die letzte Implikationseinführung weglassen, haben wir nicht $\vdash A→((B→(A∧B)) ∧ (C→(A∧C)))$ bewiesen, sondern nur $A\vdash (B→(A∧B)) ∧ (C→(A∧C))$, und der Baum sähe am Ende so aus (man bemerke, dass die $A$ noch als globale Annahmen übrigbleiben). \sourceon ASCII-Art A [B]^2 A [C]^3 ------------- ------------- A∧B A∧C ------- 2 ------- 3 B→(A∧B) C→(A∧C) ------------------------ (B→(A∧B)) ∧ (C→(A∧C)) \sourceoff \quoteon Eine Frage noch: Mit der And-Einführungsregel kann man folgende Beweisfolge konstruieren: A,B,A and B Wie kann man aber ohne Reiterationsfolge die folgende Beweisfolge konstruieren: A,A \quoteoff Wenn wir mit Bäumen arbeiten statt mit Folgen (und andere Kleinigkeiten des im Skript verwendeten KdnS), ergibt sich die Notwendigkeit der Reiteration seltener. Man kann natürlich auch immer Teilbeweise wiederholen. Wenn eine Folge zu $A$ führt, führt dieselbe nochmal auch zu $A$. Syntaktisch verboten werden muss das jedenfalls nicht. \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.6, vom Themenstarter, eingetragen 2021-10-09

\quoteon(2021-10-09 12:40 - carlox in Beitrag No. 6) \quoteon Wenn wir mit Bäumen arbeiten statt mit Folgen (und andere Kleinigkeiten des im Skript verwendeten KdnS), ergibt sich die Notwendigkeit der Reiteration seltener. Man kann natürlich auch immer Teilbeweise wiederholen. Wenn eine Folge zu $A$ führt, führt dieselbe nochmal auch zu $A$. Syntaktisch verboten werden muss das jedenfalls nicht. \quoteoff Ok. Danke für deine Infos. 1) Ich habe jetzt im Browser mit "try it" ein paar Aussagen der Aussagenlogik bewiesen. Dieses ganzen Quellcode habe ich kopiert und in einer Word-Datei gespeichert. Wie kann man das im Browser in einer Lean-Datei speichern ? 2) Ich würde diesen Quellcode gerne hier mal zeigen. Wie kann man das machen, ohne dass mir die Formatierung um die Ohren fliegt? (Das was mir bei "try it" schön formatiert angezeigt wird - also auch meine Kommentare im Quellcode - wird mir im MP anders dargestellt) 3) Ich habe deshalb meinen Quellcode hier als pdf reingestellt: hier Frage: Habe ich im Quellcode alles richtig eingerückt bzw. wie machen das die Profis? 4) Gibt es eine Website, wo man über seine Lean-Programm diskutieren kann, bzw. diese dort vorstellen kann ? mfg cx \quoteoff


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.7, eingetragen 2021-10-09

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-09 12:40 - carlox in Beitrag No. 6) 1) Ich habe jetzt im Browser mit "try it" ein paar Aussagen der Aussagenlogik bewiesen. Dieses ganzen Quellcode habe ich kopiert und in einer Word-Datei gespeichert. Wie kann man das im Browser in einer Lean-Datei speichern ? \quoteoff Ich denke nicht. Anstelle einer Word-Datei kannst du aber natürlich auch eine ganz normale Textdatei nehmen. \quoteon 2) Ich würde diesen Quellcode gerne hier mal zeigen. Wie kann man das machen, ohne dass mir die Formatierung um die Ohren fliegt? (Das was mir bei "try it" schön formatiert angezeigt wird - also auch meine Kommentare im Quellcode - wird mir im MP anders dargestellt) \quoteoff \sourceon MP-Nachricht /sourceon lean -- wotsit dooda theorem test(x : ℕ): 0 ∣ x → x = 0 := begin intro h, unfold has_dvd.dvd at h, cases h with y i, simp [i, nat.zero_mul] end /sourceoff \sourceoff ergibt, wenn man anstelle der / Backslashs scheibt: \sourceon lean -- wotsit dooda theorem test(x : ℕ): 0 ∣ x → x = 0 := begin intro h, unfold has_dvd.dvd at h, cases h with y i, simp [i, nat.zero_mul] end \sourceoff \quoteon 3) Ich habe deshalb meinen Quellcode hier als pdf reingestellt: hier Frage: Habe ich im Quellcode alles richtig eingerückt bzw. wie machen das die Profis? \quoteoff Sieht in Ordnung aus. Einige Klammerpaare kann man weglassen, und die entsprechende weitere Einrückung würde ich dann auch nicht vornehmen. Nämlich in Konstruktionen wie assume h, (assume i, bla). Ich würde das mit Zeilenumbrüchen so schreiben: \sourceon lean assume h, assume i, bla \sourceoff (bla vielleicht noch einrücken, wenn es größer ist) Und naja. Profis verwenden eigentlich selten assume und schreiben stattdessen direkt $\lambda$, oder sie verwenden den Taktik-Modus, also begin end. \quoteon 4) Gibt es eine Website, wo man über seine Lean-Programm diskutieren kann, bzw. diese dort vorstellen kann ? \quoteoff Ja. https://matheplanet.de. 😄 Und https://leanprover.zulipchat.com/ zum Beispiel. Ist zwar näher an 'nem Chat als 'nem Forum, aber scheint benutzbar.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.8, vom Themenstarter, eingetragen 2021-10-11

\quoteon Und naja. Profis verwenden eigentlich selten assume und schreiben stattdessen direkt $\lambda$, oder sie verwenden den Taktik-Modus, also begin end. \quoteoff Danke für deine wertvollen Tipps. 1) Bis jetzt habe ich mich in LEAN mit den Beweisen in der Aussagenlogik beschäftigt. Ich mache jetzt mit den Allquantoren weiter und will einige Beweise in der Prädikatenlogik machen. Dazu arbeite ich an der von dir genannten Quelle weiter: http://leanprover.github.io/logic_and_proof/ 2) Ich dachte bis jetzt, dass LEAN auch Beweise generieren kann. Stimmt das ? Wie macht man das ? Kannst du mir dazu eine Quelle angeben ? 3) Was sind Taktiken ? Kannst du mir dazu eine Quelle angeben ? 4) Wozu braucht man die Lambda-Schreibweise? Kannst du mir dazu eine Quelle angeben ? Nachklapp: Habe mit PL1 (Prädiktenlogik 1. Stufe) experimentiert: \sourceon lean theorem t1 (U:Type) (A B : U → Prop) (x : Type) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, (assume h2 : ∀ x, A x, (assume y, --(assume hy : y, have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff Als Anfänger wäre es mir recht, auch die Variable y als "variable" mit ihrem Typ "Type" innerhalb des Theorems zu deklarieren. Wie geht das möglichst einach ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.9, eingetragen 2021-10-11

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-11 10:52 - carlox in Beitrag No. 8) 2) Ich dachte bis jetzt, dass LEAN auch Beweise generieren kann. Stimmt das ? Wie macht man das ? Kannst du mir dazu eine Quelle angeben ? \quoteoff Ja. Taktiken sind genau dazu da. Hier kannst du dir diesen Code in Aktion ansehen: \sourceon lean import tactic theorem t1(m n : ℕ) : (m+n)^3 = m^3 + 3*m^2*n + 3*m*n^2 + n^3 := begin ring end #print t1 -- hier sieht man den generierten Beweisterm. \sourceoff Die ring-Taktik etwa, ist eine ganz allgemeine, die Anwendungen der Axiome von kommutativen (Halb-)Ringen zusammensetzt, um Gleichungen wie die angegebene zu beweisen. Irgendwo in der Standardbibliothek ist angegeben, auf welche Weise $\IN$ ein kommutativer Halbring ist, die ring-Taktik funktioniert aber für alle Halbring-Instanzen. \quoteon 3) Was sind Taktiken ? Kannst du mir dazu eine Quelle angeben ? \quoteoff Taktiken sind Metaprogramme zur Erzeugung von Termen (die nicht unbedingt einen Typ haben müssen, der eine Aussage ist). Man kann auch selber Taktiken programmieren -- das ist aber eher für fortgeschrittene. Hier grundsätzliche Information zur Benutzung. Hier ist eine Dokumentation der in mathlib vorhandenen Taktiken. Hier ein Text, der das Taktiken-selber-Schreiben erläutern soll. \quoteon 4) Wozu braucht man die Lambda-Schreibweise? Kannst du mir dazu eine Quelle angeben ? \quoteoff Es ist eben eine übersichtliche Möglichkeit, Funktionen (bzw. Beweise von Implikationen oder $\forall$-Aussagen) zu definieren. Bezüglich Beweisen steht hier 'was. \quoteon Nachklapp: Habe mit PL1 (Prädiktenlogik 1. Stufe) experimentiert: \sourceon lean theorem t1 (U:Type) (A B : U → Prop) (x : Type) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, (assume h2 : ∀ x, A x, (assume y, --(assume hy : y, have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff Als Anfänger wäre es mir recht, auch die Variable y als "variable" mit ihrem Typ "Type" innerhalb des Theorems zu deklarieren. Wie geht das möglichst einach ? mfg cx \quoteoff y hat doch den Typ U (das wird aus der Verwendung von B : U → Prop im hinteren (∀ x, B x) geschlossen). Jedenfalls kannst du im Beweis dann assume y:U, schreiben. Und (x : Type) im Theorem-Statement ist fehl am Platz.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.10, vom Themenstarter, eingetragen 2021-10-12

\quoteon \quoteon Nachklapp: Habe mit PL1 (Prädiktenlogik 1. Stufe) experimentiert: \sourceon lean theorem t1 (U:Type) (A B : U → Prop) (x : Type) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, (assume h2 : ∀ x, A x, (assume y, --(assume hy : y, have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff Als Anfänger wäre es mir recht, auch die Variable y als "variable" mit ihrem Typ "Type" innerhalb des Theorems zu deklarieren. Wie geht das möglichst einach ? mfg cx \quoteoff y hat doch den Typ U (das wird aus der Verwendung von B : U → Prop im hinteren (∀ x, B x) geschlossen). Jedenfalls kannst du im Beweis dann assume y:U, schreiben. Und (x : Type) im Theorem-Statement ist fehl am Platz. \quoteoff \quoteoff Also so: \sourceon lean theorem t1 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, (assume h2 : ∀ x, A x, (assume y : U, have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff Danke für die Hilfe. 1) Warum ist (x : Type) im Theorem-Statement fehl am Platz? (Funktionieren würde es ja, d.h. es gibt keine Fehlermeldung). 2) Bei einem der obigen assumes ist noch die Angabe der Variable (also h2) dabei: assume h2 : ∀ x, A x, Wie könnte man das auch noch bei assume y : U, hinzufügen ? 3) Habe deinen Link zu tactics noch nicht gelesen. Trotzdem die Frage: Mit welcher Taktik kann man Beweise für aussagenlogische Sätze (die ich in meinem Beitrag Nr. 6 angegeben habe) generieren lassen ? (damit ich damit experimentieren kann) mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.11, eingetragen 2021-10-12

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-12 14:11 - carlox in Beitrag No. 10) 1) Warum ist (x : Type) im Theorem-Statement fehl am Platz? (Funktionieren würde es ja, d.h. es gibt keine Fehlermeldung). \quoteoff Es ist ein überflüssiger zusätzlicher Parameter, der nicht benutzt wird. \quoteon 2) Bei einem der obigen assumes ist noch die Angabe der Variable (also h2) dabei: assume h2 : ∀ x, A x, Wie könnte man das auch noch bei assume y : U, hinzufügen ? \quoteoff \qoteoff Verstehe ich nicht. h2 hat den Typ ∀ x, A x, ist also ein "Beweis" (wenn auch ein trivialer, per temporärer Annahme), dieser Aussage, als Teil des angefangen Beweises der rechten Implikation. Und y : U ist Teil des angefangenen Beweises von (∀ x, B x); In Prosa: "Sei $y$ ein beliebiges Element von $U$; wir zeigen nun $B(y)$...". \quoteon 3) Habe deinen Link zu tactics noch nicht gelesen. Trotzdem die Frage: Mit welcher Taktik kann man Beweise für aussagenlogische Sätze (die ich in meinem Beitrag Nr. 6 angegeben habe) generieren lassen ? (damit ich damit experimentieren kann) \quoteoff Die meisten gehen mit der Taktik finish aus mathlib zu erledigen, die noch übrigen mit vorheriger Vorbereitung. \sourceon lean import tactic -- die Taktiken hier drin verwenden auch klassische Logik theorem doppelteNegation(A : Prop): A ↔ ¬¬A := by finish theorem test(A : Prop): A → A := by finish theorem lem(A : Prop): A ∨ ¬A := by finish theorem ausschluss_1(A B : Prop): ¬A ∧ (A ∨ B) → B := by finish theorem myTheorem_1 (A B C : Prop) : A→((B→(A∧B)) ∧ (C→(A∧C))) := by finish theorem distribute_and_verteilen_1 (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := by finish theorem distribute_and_ausklammern_1 (A B C : Prop) : (A ∧ B) ∨ (A ∧ C) → A ∧ (B ∨ C) := by finish theorem distribute_and (A B C : Prop) : (A ∧ B) ∨ (A ∧ C) ↔ A ∧ (B ∨ C) := by split; finish -- finish allein tut sich hier schwer. theorem distributiv_or_ausklammern (A B C : Prop) : (A∨B) ∧ (A∨C) → A ∨ B∧C := by finish theorem distributiv_or_verteilen (A B C : Prop) : A∨(B∧C) → (A∨B) ∧ (A∨C) := by finish theorem distribute_or (A B C : Prop) : A∨(B∧C) ↔ (A∨B) ∧ (A∨C) := by split; finish -- finish allein tut sich hier schwer. theorem oderNegation_verteilen (A B : Prop) : ¬(A∨B) → ¬A∧¬B := by finish theorem oderNegation_ausklammern (A B : Prop) : ¬A∧¬B → ¬(A∨B) := by finish theorem oderNegation(A B : Prop) : ¬A∧¬B ↔ ¬(A∨B) := by finish theorem oder_Implikation_1(A B : Prop) : ¬A∨B → A→B := by finish theorem oder_Implikation_2(A B : Prop) : (A→B) → (¬A∨B) := by finish theorem oder_Implikation(A B : Prop) : (A→B) ↔ (¬A∨B) := by finish \sourceoff Mittels #print test etc. kannst du dir dir generierten Beweisterme anschauen. \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.12, vom Themenstarter, eingetragen 2021-10-12

\quoteon Verstehe ich nicht. h2 hat den Typ ∀ x, A x, ist also ein "Beweis" (wenn auch ein trivialer, per temporärer Annahme), dieser Aussage, als Teil des angefangen Beweises der rechten Implikation. Und y : U ist Teil des angefangenen Beweises von (∀ x, B x); In Prosa: "Sei $y$ ein beliebiges Element von $U$; wir zeigen nun $B(y)$...". \quoteoff 1) habe meinen Quellcode kommentiert. Ist das so ok ? \sourceon lean theorem t0 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, -- h1 sei vom Typ ∀ x, A x → B x (assume h2 : ∀ x, A x, -- h2 sei vom Typ ∀ x, A x (assume y : U, -- y sei ein beliebiges Element von U have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff 2) Du schreibst, dass x ein überflüssiger zusätzlicher Parameter ist, der nicht benutzt wird. Aber x kommt doch in \sourceon lean theorem t0 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := \sourceoff vor und muss doch deklariert werden, oder ? 3) Danke für die Angabe der Taktik bei Beweisen für die Aussagenlogik. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.13, eingetragen 2021-10-12

\quoteon(2021-10-12 18:11 - carlox in Beitrag No. 12) 1) habe meinen Quellcode kommentiert. Ist das so ok ? \sourceon lean theorem t0 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, -- h1 sei vom Typ ∀ x, A x → B x (assume h2 : ∀ x, A x, -- h2 sei vom Typ ∀ x, A x (assume y : U, -- y sei ein beliebiges Element von U have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff \quoteoff Technisch gesehen ist das zwar in Ordnung, aber im Fall von Propositionen würde ich doch eher davon sprechen, dass eine solche angenommen wird. (nd die Variablen mit den entsprechenden Typen sind kaum mehr als eine Möglichkeit, auf die Aussage zu verweisen und diese zu verwenden. \quoteon 2) Du schreibst, dass x ein überflüssiger zusätzlicher Parameter ist, der nicht benutzt wird. Aber x kommt doch in \sourceon lean theorem t0 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := \sourceoff vor und muss doch deklariert werden, oder ? \quoteoff x kommt nicht frei vor. Die Vorkommen sind gebunden. Und welchen Typ die Variablen da haben, könnte man *dort* hinschreiben. \sourceon theorem t0 (U:Type) (A B : U → Prop) : (∀ x : U, A x → B x) → ((∀ x : U, A x) → (∀ x : U, B x)) \sourceoff Das ist jedoch hier unnötig, da der Typ automatisch erkannt wird.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.14, vom Themenstarter, eingetragen 2021-10-13

\quoteon Technisch gesehen ist das zwar in Ordnung, aber im Fall von Propositionen würde ich doch eher davon sprechen, dass eine solche angenommen wird. (nd die Variablen mit den entsprechenden Typen sind kaum mehr als eine Möglichkeit, auf die Aussage zu verweisen und diese zu verwenden. \quoteoff 1) Eine prinzipielle Frage: Was sind h1,h2,h im Quellcode unten ? Sind das Variable, Konstanten, usw.? Sie werden ja nirgends deklariert. Oder ist das jeweils nur eine Abkürzung bzw. Bezeichnung für die rechts des Doppelpunkts stehende Hypothese? Welchen syntaktischen Regeln muss eine Hypothese genügen? (sie muss ja irgendwie wohlgeformt sein). Z.B. ist ja der Ausdruck unten: (assume h : y, falschgeformt. Ähnliche Frage gilt für: h3, h4 \sourceon lean theorem t0 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, -- h1 sei vom Typ ∀ x, A x → B x (assume h2 : ∀ x, A x, -- h2 sei vom Typ ∀ x, A x --(assume y : U, -- y sei ein beliebiges Element von U (assume h : y, -- y sei ein beliebiges Element von U have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff 2) \quoteon Mittels #print test etc. kannst du dir dir generierten Beweisterme anschauen. \quoteoff Habe deine Lösungen mit tactics für die Beweise kopiert. Mit "try it" gibt es auch keine Fehlermeldungen. Allerdings werden mir mit #print test keine Beweisterme angezeigt. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.15, eingetragen 2021-10-13

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-13 09:56 - carlox in Beitrag No. 14) \quoteon Technisch gesehen ist das zwar in Ordnung, aber im Fall von Propositionen würde ich doch eher davon sprechen, dass eine solche angenommen wird. (nd die Variablen mit den entsprechenden Typen sind kaum mehr als eine Möglichkeit, auf die Aussage zu verweisen und diese zu verwenden. \quoteoff 1) Eine prinzipielle Frage: Was sind h1,h2,h im Quellcode unten ? Sind das Variable, Konstanten, usw.? Sie werden ja nirgends deklariert. Oder ist das jeweils nur eine Abkürzung bzw. Bezeichnung für die rechts des Doppelpunkts stehende Hypothese? Welchen syntaktischen Regeln muss eine Hypothese genügen? (sie muss ja irgendwie wohlgeformt sein). Z.B. ist ja der Ausdruck unten: (assume h : y, falschgeformt. Ähnliche Frage gilt für: h3, h4 \sourceon lean theorem t0 (U:Type) (A B : U → Prop) : (∀ x, A x → B x) → ((∀ x, A x) → (∀ x, B x)) := (assume h1 : ∀ x, A x → B x, -- h1 sei vom Typ ∀ x, A x → B x (assume h2 : ∀ x, A x, -- h2 sei vom Typ ∀ x, A x --(assume y : U, -- y sei ein beliebiges Element von U (assume h : y, -- y sei ein beliebiges Element von U have h3 : A y, from h2 y, have h4 : A y → B y, from h1 y, show B y, from h4 h3 ) ) ) \sourceoff \quoteoff h1 und h2 sind Variablen sie werden durch das assume deklariert und ihr Skopus erstreckt sich über den Rest des Ausdrucks, der vom Komma bis jwd reicht. Ihr Typ ist das, was hinter dem (optionalen) : steht. Die zugehörigen Regeln sind sowas wie $$\begin{array}{c} \Gamma, \color{red}{h:} A \vdash \color{red}{M:} B \\\hline \Gamma \vdash \color{red}{\lambda h:A.\, M:} A \to B \end{array}(\to\text{-Intro})$$ und $$\begin{array}{c} \Gamma \color{red}{,x: A} \vdash \color{red}{M:} B \\\hline \Gamma \vdash \color{red}{\lambda x:A.\, M:} \forall x:A.\, B \end{array}(\forall\text{-Intro})$$ die man ohne den ganzen roten Kram auch in vielen "normalen" Logikbüchern findet. Bei den haves (die das fast-Synonym let haben) ist es, was Deklaration und Skopen angeht, recht ähnlich, hier kommt aber eher so etwas wie cut zum Tragen $$\begin{array}{c} \Gamma \vdash \color{red}{M:}T \qquad \Gamma, \color{red}{x:}T \vdash \color{red}{N:}A \\\hline \Gamma \vdash \color{red}{\mathrm{let}\ x:T := M\ \mathrm{in}\ N:}A \end{array}(\text{cut})$$ (Um $A$ in einem Kontext $\Gamma$ zu beweisen, kann man stattdessen auch erstmal $T$ in diesem Kontext beweisen, und danach $A$ in $\Gamma,T$.) Vielleicht hilft auch folgende Bemerkung: Propositionen sind spezielle Typen, und man kann statt mit solchen auch mit anderen arbeiten, etwa um eine Funktion $\IN \to \IN^\IN$ zu definieren: \sourceon def bar(A : Prop): A → A → A := assume h1 : A, assume h2 : A, have t : A, from h1, h2 -- Hier könnte man auch t oder h1 verwenden; eigentlich egal. def foo: ℕ → ℕ → ℕ := assume x : ℕ, assume y : ℕ, have t : ℕ, from x+y, t*t -- Hier könnte man auch irgendeinen anderen Ausdruck vom Typ ℕ nehmen, -- aber natürlich kämen dann i.A. andere Funktionen heraus! -- kürzere Version von foo, mit geringfügig anderer Syntax: def foo': ℕ → ℕ → ℕ := λ x y, let t := x+y in t*t #eval foo' 5 6 -- ergibt 121 #eval foo 5 6 -- natürlich auch 121 \sourceoff Ach ja, da es auch mal um Taktiken ging: Normalerweise benutzt man Taktiken nur für Beweise, aber ihre Verwendung ist nicht darauf beschränkt, und neben Monstern wie ring gibt es natürlich auch welche, die ganz kleine Schritte machen: \sourceon def foo'': ℕ → ℕ → ℕ := begin intro x, intro y, let t := x+y, exact t*t end #print foo'' -- schreibt den Code von foo', mit mehr Typannotationen, hin. \sourceoff \quoteon 2) \quoteon Mittels #print test etc. kannst du dir dir generierten Beweisterme anschauen. \quoteoff Habe deine Lösungen mit tactics für die Beweise kopiert. Mit "try it" gibt es auch keine Fehlermeldungen. Allerdings werden mir mit #print test keine Beweisterme angezeigt. \quoteoff Hmm. Wenn du #print test in den Code schreibst sollte das grün unterkringelt sein. Wenn du den Textcursor darauf platzierst, sollte rechts im Statusfenster der Term erscheinen.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.16, vom Themenstarter, eingetragen 2021-10-19

\sourceon lean /- Hallo tactac, habe -Dank deiner Hilfe - zu Testzwecken (siehe unten) mal einige Funktionen programmiert (addieren mit verschiedenen Versionen). Dabei sind mir folgende Fragen dazu eingefallen: 1) zur Funktion bar: Sind folgende Behauptungen von mir richtig ? Beh1) A ist eine Variable vom Typ Prop und ein Parameter der Funktion Beh2) h1 ist eine Variable vom Typ A. Beh3) h2 ist eine Variable vom Typ A. Beh4) t ist eine Variable vom Typ A. Dass A eine Variable vom Typ Prop ist, kann ich nachvollziehen. Warum ist aber h1 eine Variable vom Typ A ? A ist doch eine Variable und kein Typ ??? A ist für mich eher der Wert von h1 Beh5) A ist ein "Input-Parameter" und der Output ist A → A → A #check bar X zeigt, dass X der Input und X → X → X der Output ist. Frage: Was ist aber A → A → A? Ein Typ, ein Wert, oder ein "Ausdruck", eine Formel? Warum sind die folgenden Programmzeilen falsch: #check bar X X #check bar X∧X #eval bar X -/ def bar(A : Prop): A → A → A := assume h1 : A, assume h2 : A, have t : A, from h1, h2 -- Hier könnte man auch t oder h1 verwenden; eigentlich egal. constants X Y : Prop #check bar #check bar X /- in der Funktion addieren sind die Input-Parameter für mich klar ersichtlich: (n : ℕ) und (m : ℕ) sind die Input-Parameter und n + m ist der Output (die Rückgabe). Frage: Wo werden die Input-Parameter in den anderern Funktionen addieren_v1, addieren_v2, addieren_v3, addieren_v4 angegeben? -/ -- Vorbemerkung: -- mit F bezeichne ich i.A. in meinen Kommentaren ganz allegmein eine Funktion -- Funktion F(n) = n + m def addieren (n : ℕ) (m : ℕ) : ℕ := n + m -- Version mit Lamda-Abstraktion def addieren_v1: ℕ → ℕ → ℕ := ( λ(x : nat), λ(y : nat), (x+y)) -- Version mit Lamda-Abstraktion und let: def addieren_v2: ℕ → ℕ → ℕ := λ(x : nat), λ(y : nat), let t := x+y in t -- Version mit let: def addieren_v3 (n : ℕ) (m : ℕ) : ℕ := let t := n + m in t def addieren_v4: ℕ → ℕ → ℕ := assume x : ℕ, assume y : ℕ, (x+y) -- Funktionsaufrufe zum Testen #eval addieren 3 5 #eval addieren_v1 3 5 #eval addieren_v2 3 5 #eval addieren_v3 3 5 #eval addieren_v4 3 5 /- Was ist der prinzipielle Unterschied zwischen der Funktion bar und der Funktion addieren bzw. deren Versionen .._v1, usw. -/ \sourceoff mfg cx


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.17, vom Themenstarter, eingetragen 2021-10-20

\sourceon lean /- Hallo tactac, Was mir zum Thema Variablen und Typen noch aufgefallen ist, demonstriere ich in dem Programm unten: Wenn α, β, γ den Typ der natürlichen Zahlen haben (was ich auskommentiert habe), bekommt man einen Syntaxfehler. Warum ? Bei: def compose := g (f x) wird doch dann durch die Hintereinanderausführung Folgendes gemacht: [(β → γ)[(α → β)α]] = γ Das verstehe ich nicht. Wenn x den Typ α hat und α den Typ nat, dann hat doch x auch den Typ nat. Wo ist da mein Denkfehler? -/ /- variable α : nat variable β : nat variable γ : nat -/ variable α : Type 0 variable β : Type 0 variable γ : Type 0 /- variable α : Type* variable β : Type* variable γ : Type* -/ variable g : β → γ variable f : α → β variable h : α → α variable x : α def compose := g (f x) def do_twice := h (h x) def do_thrice := h (h (h x)) #print compose #print do_twice #print do_thrice \sourceoff


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.18, eingetragen 2021-10-20

Erstmal @#16 \quoteon 1) zur Funktion bar Sind folgende Behauptungen von mir richtig ? [Beh1 ... Beh4] \quoteoff Ja. \quoteon Dass A eine Variable vom Typ Prop ist, kann ich nachvollziehen. Warum ist aber h1 eine Variable vom Typ A ? A ist doch eine Variable und kein Typ ??? A ist für mich eher der Wert von h1 \quoteoff A ist eine Variable vom Typ Prop, und damit ist ihr Wert eine Proposition, und Propositionen sind spezielle Typen. Stichworte "propositions as types", "Curry-Howard", etc. \quoteon Beh5) A ist ein "Input-Parameter" und der Output ist A → A → A #check bar X zeigt, dass X der Input und X → X → X der Output ist. \quoteoff Der Typ von bar A ist A → A → A, für beliebige A:Prop \quoteon Frage: Was ist aber A → A → A? Ein Typ, ein Wert, oder ein "Ausdruck", eine Formel? \quoteoff Vor allem ein Typ. Spezieller: eine Proposition. \quoteon Warum sind die folgenden Programmzeilen falsch: #check bar X X \quoteoff X hat nicht den Typ X. Folgendes ginge: \sourceon lean constant x:X #check bar X x #check bar X x x \sourceoff \quoteon #check bar X∧X \quoteoff Hier fehlen Klammern um X∧X. \quoteon #eval bar X \quoteoff Hier beschwert sich Lean nicht über Typfehler oder so, sondern sagt nur, dass es nicht weiß, wie es den Ausdruck auswerten soll. \quoteon Was ist der prinzipielle Unterschied zwischen der Funktion bar und der Funktion addieren bzw. deren Versionen .._v1, usw. \quoteoff Es gibt keine sehr großen Unterschiede. Man könnte (remember: Propositionen sind spezielle Typen). Durch folgende kleine Veränderungen kommt man zum selben Ergebnis: * In der Definition von bar statt Prop auch Type nehmen. * In der Definition von addieren_v1 statt dem festen Typ einen beliebigen Typ A:Type nehmen, der dann noch als Zusatzparameter auftaucht. Und natürlich kann man dann nicht + benutzen; es sei denn, man fordert zusätzlich, dass der Typ A Instanz von has_add ist.


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.19, eingetragen 2021-10-20

@#17 \quoteon Wenn α, β, γ den Typ der natürlichen Zahlen haben (was ich auskommentiert habe), bekommt man einen Syntaxfehler. Warum ? \quoteoff Es ist kein Syntaxfehler, sondern ein Typfehler. Wenn β, γ den Typ nat haben, ist β → γ nichts sinnvolles. Beachte den Unterschied zwischen nat → nat und 47 → 11. \quoteon Wenn x den Typ α hat und α den Typ nat, dann hat doch x auch den Typ nat. \quoteoff Das stimmt höchstens, weil die Voraussetzungen zusammen falsch sind. Wenn α den Typ nat hat, kann kein x den Typ α haben. Die Relation "? hat Typ ?" ist jedoch auch nicht transitiv. So hat 5 z.B. den Typ nat, nat den Typ Type, aber 5 nicht den Typ Type. Davon abgesehen: Die variable-Deklarationen dienen dazu, in nachfolgenden Definitionen Parameter weglassen zu können, die dann aber trotzdem da sind. Deshalb hat compose eben nicht den Typ γ, sondern den Typ Π (α β γ : Type), (β → γ) → (α → β) → α → γ, bzw. compose α β γ den Typ (β → γ) → (α → β) → α → γ für beliebige α, β, γ: Type.


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.20, vom Themenstarter, eingetragen 2021-10-21

Hallo tactac, vielen Dank für deine Ratschläge, deine Mühe und deinen Langmut. Ich verstehe leider gerade überhaupt nichts mehr was die Typen betrifft und bin da total verwirrt (null Plan). Deinen Tipp „Propositions as Types“ habe ich befolgt und das Video angeschaut. https://www.youtube.com/watch?v=SknxggwRPzU Außerdem das folgende Zitat gelesen: https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html „For those more comfortable with set-theoretic foundations, it may be helpful to think of a type as nothing more than a set, in which case, the elements of the type are just the elements of the set.“ Dann habe ich das Zitat auf das Programm unten angewendet und mir dann Folgendes zusammenphantasiert: B (natürlich auch A und C) ist also eine Variable vom Typ Prop = {wahr,falsch} Prop bedeutet Aussagen, sind also wahr oder falsch. Also hat B den Wert falsch oder wahr. Ich nehme einfach mal an, dass B den Wert falsch hat. Also ist der Typ B = {falsch} hB : B bedeutet, dass die Variable hB den Typ B = {falsch} hat. Also hat hB den Wert falsch, da die Menge aus nur einem Element besteht. Wo ist der Denkfehler? Was ist die richtige Argumentation? mfg cx \sourceon lean theorem distribute_and_verteilen_2 (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := (assume h : A ∧ (B∨C), or.elim(and.right(h)) (assume hB:B, -- have h1:A prüft, ob A and.left h ein Beweis von A ist. -- Zusätzlich kann h1 an Stelle vom Beweis and.left h später verwendet werden. have h1:A, from and.left h, have h2:A∧B, from and.intro h1 hB, show (A∧B) ∨ (A∧C), from or.inl h2 ) (assume hC:C, have h1:A, from and.left h, have h2:A∧C, from and.intro h1 hC, show (A∧B) ∨ (A∧C), from or.inr h2 ) ) \sourceoff


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.21, eingetragen 2021-10-21

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-21 20:00 - carlox in Beitrag No. 20) B (natürlich auch A und C) ist also eine Variable vom Typ Prop = {wahr,falsch} Prop bedeutet Aussagen, sind also wahr oder falsch. Also hat B den Wert falsch oder wahr. Ich nehme einfach mal an, dass B den Wert falsch hat. Also ist der Typ B = {falsch} hB : B bedeutet, dass die Variable hB den Typ B = {falsch} hat. Also hat hB den Wert falsch, da die Menge aus nur einem Element besteht. Wo ist der Denkfehler? Was ist die richtige Argumentation? \quoteoff Das ist nicht richtig. Wenn B falsch ist, gilt in dem Bild B = falsch. Und wir müssen uns überlegen, was "falsch" denn als Typ sein soll, damit wir von hB : B sprechen können. Und wie man vielleicht erwartet, ist in diesem Fall B der leere Typ. D.h. aus einem Wert vom Typ B können wir dann alles zaubern. Sich Prop als {wahr, falsch} vorzustellen, ist nicht ganz so gut. Mit ein wenig Mengenlehre-statt-Typen-Terminologie funktioniert folgende erste Näherung vielleicht besser: wir fassen beliebige Mengen als "Propositionen" auf. Eine als Proposition gesehene Menge "gilt", wenn sie ein Element hat. Für Propositionen $A,B$ und beliebige Mengen $X$, und $X$-indizierte Familien von Propositionen $P$ (Also $P(x)$ sehen wir für alle $x \in X$ als Proposition) sei dann: * $False := \emptyset$, * $True := \{\emptyset\}$, * $\lnot A := A \to False$, * $A \land B := A \times B$, * $A \to B := B^A$, * $A \lor B := A + B$, * $\forall x\in X.\, P(x) := \prod_{x\in X}P(x)$, * $\exists x\in X.\, P(x) := \sum_{x\in X}P(x)$, * $A \leftrightarrow B := (A \to B) \land (B \to A)$. + und $\Sigma$ stehen dabei für disjunkte Vereinigungen. Ein "Beweis" einer "Proposition" $A$ ist nun einfach die Angabe eines Elements $x \in A$. Man beachte, dass das Gelten von $A \leftrightarrow B$ nicht bedeutet, dass es eine Bijektion zwischen $A$ und $B$ gibt oder gar eine Gleichheit, sondern nur Funktionen in beide Richtungen. Man kann daher $A \lor (B \land C) \leftrightarrow (A \lor B) \land (A \lor C)$ zeigen, wie man es von einer Logik erwarten würde. Du wirst sehen, dass eine Definition für \sourceon lean def distribute_and_verteilen_3 (A B C : Type) : A × (B ⊕ C) → (A × B) ⊕ (A × C) := \sourceoff in Lean sich direkt aus dem von dir angegebenen Beweis ergibt, wenn man * ∧ durch ×, * ∨ durch ⊕, * or.elim durch sum.cases_on, * and.left durch prod.fst, * and.right durch prod.snd, * or.inl durch sum.inl, * or.inr durch sum.inr, * and.intro durch prod.mk ersetzt (und vielleicht noch einiges anderes, das ich jetzt vergessen habe). \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.22, vom Themenstarter, eingetragen 2021-10-24

Hallo tactac, I) \quoteon Ein "Beweis" einer "Proposition" $A$ ist nun einfach die Angabe eines Elements $x \in A$. \quoteoff hoffe, dich richtig verstanden zu haben und zeige dir dazu das folgende Beispiel1: Beweis für die Proposition A → A : \(A^A \) sei die Menge aller Funktionen von einer beliebigen Menge A nach A Zeige dazu, dass es eine Funktion f \(\in A^A \) (für beliebiges A) gibt mit: f: A |-> A Diese Funktion f kann man wie folgt angeben: f(x) := x mit beliebigem x Element von A Beispiel2: Beweis für die Proposition \(A \land (B \lor C) → A \land B \lor A \land C \): \({A \times (B + C)}^{A \times B + B \times C}\) sei die Menge aller Funktionen von einer beliebigen Menge \(A \times (B + C) \) nach \(A \times B + B \times C \) Zeige dazu, dass es eine Funktion f von \( A \times (B + C)\) nach \((A \times B + B \times C\) gibt. Sei \( (x,y) \in A \times (B + C) \) also \( x \in A \) und \( y \in B+C \) Fall1: \( y \in B \) f(x,y) := (x,y) Fall2: \( y \in C \) f(x,y) := (x,y) Es gilt: \( f(x,y) \in A \times B + B \times C \) Stimmen meine Überlegungen? II) In dem folgende Buch steht: https://homotopytypetheory.org/book/ ------------- Adopting a new foundational system such as homotopy type theory as the implicit formal basis of informal reasoning will require adjusting some of one’s instincts and practices. ... By contrast, type theory is its own deductive system: it need not be formulated inside any superstructure, such as first-order logic. Instead of the two basic notions of set theory, sets and propositions, type theory has one basic notion: types. -------------- So wie ich das verstanden habe, wird also die Typentheorie _nicht_ in PL1 (Prädikatenlogik 1. Stufe) formuliert, sondern in einem eigenen "Beweissystem" (Ausdrücke ("Formeln"), Axiome, Schlussregeln) formalisiert. Stimmt das bzw. kannst du kurz beschreiben, wie das aussieht. III) Um also Typen richtig zu verstehen, müsste ich Homotopietheorie verstehen. Das würde mich vermutlich überfordern. mfg cx


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.23, vom Themenstarter, eingetragen 2021-10-25

\sourceon lean theorem distribute_and_verteilen_2 (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := (assume h : A ∧ (B∨C), or.elim(and.right(h)) (assume hB:B, -- have h1:A prüft, ob A and.left h ein Beweis von A ist. -- Zusätzlich kann h1 an Stelle vom Beweis and.left h später verwendet werden. have h1:A, from and.left h, have h2:A∧B, from and.intro h1 hB, show (A∧B) ∨ (A∧C), from or.inl h2 ) (assume hC:C, have h1:A, from and.left h, have h2:A∧C, from and.intro h1 hC, show (A∧B) ∨ (A∧C), from or.inr h2 ) ) variable R : Prop variable S : Prop variable T : Prop #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \sourceoff Ist folgende Behauptung richtig: Die Variable h2 hat den Typ A∧B und den Wert (R∧R) ∧ (S∧S) bei obigem Aufruf #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.24, eingetragen 2021-10-25

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-10-24 13:14 - carlox in Beitrag No. 22) Hallo tactac, I) \quoteon Ein "Beweis" einer "Proposition" $A$ ist nun einfach die Angabe eines Elements $x \in A$. \quoteoff hoffe, dich richtig verstanden zu haben und zeige dir dazu das folgende Beispiel1: Beweis für die Proposition A → A : \(A^A \) sei die Menge aller Funktionen von einer beliebigen Menge A nach A Zeige dazu, dass es eine Funktion f \(\in A^A \) (für beliebiges A) gibt mit: f: A |-> A Diese Funktion f kann man wie folgt angeben: f(x) := x mit beliebigem x Element von A Beispiel2: Beweis für die Proposition \(A \land (B \lor C) → A \land B \lor A \land C \): \({A \times (B + C)}^{A \times B + B \times C}\) sei die Menge aller Funktionen von einer beliebigen Menge \(A \times (B + C) \) nach \(A \times B + B \times C \) Zeige dazu, dass es eine Funktion f von \( A \times (B + C)\) nach \((A \times B + B \times C\) gibt. Sei \( (x,y) \in A \times (B + C) \) also \( x \in A \) und \( y \in B+C \) Fall1: \( y \in B \) f(x,y) := (x,y) Fall2: \( y \in C \) f(x,y) := (x,y) Es gilt: \( f(x,y) \in A \times B + B \times C \) Stimmen meine Überlegungen? \quoteoff Ja, bis auf ein paar Tippfehler und die Tatsache, dass die Menge der Funktionen von $X$ nach $Y$ mit $Y^X$ und nicht mit $X^Y$ bezeichnet wird. Und wichtig ist vielleicht noch, die Elemente einer Menge $X+Y$ als $\mathrm{inl}(x)$ bzw. $\mathrm{inr}(y)$ zu schreiben. \quoteon II) In dem folgende Buch steht: https://homotopytypetheory.org/book/ ------------- Adopting a new foundational system such as homotopy type theory as the implicit formal basis of informal reasoning will require adjusting some of one’s instincts and practices. ... By contrast, type theory is its own deductive system: it need not be formulated inside any superstructure, such as first-order logic. Instead of the two basic notions of set theory, sets and propositions, type theory has one basic notion: types. -------------- So wie ich das verstanden habe, wird also die Typentheorie _nicht_ in PL1 (Prädikatenlogik 1. Stufe) formuliert, sondern in einem eigenen "Beweissystem" (Ausdrücke ("Formeln"), Axiome, Schlussregeln) formalisiert. Stimmt das bzw. kannst du kurz beschreiben, wie das aussieht. \quoteoff Besonders kurz geht das wohl nicht. Aber das HoTT-Buch hat einen Anhang mit einer entspr. Formalisierung. \quoteon III) Um also Typen richtig zu verstehen, müsste ich Homotopietheorie verstehen. Das würde mich vermutlich überfordern. \quoteoff Das würde ich nicht sagen. Die sprachliche Basis MLTT ist schon ganz nützlich. Und nicht jede Typtheorie ist HoTT. Die von Lean zum Beispiel nicht. \(\endgroup\)


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.25, eingetragen 2021-10-25

\quoteon(2021-10-25 21:15 - carlox in Beitrag No. 23) \sourceon lean theorem distribute_and_verteilen_2 (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := (assume h : A ∧ (B∨C), or.elim(and.right(h)) (assume hB:B, -- have h1:A prüft, ob A and.left h ein Beweis von A ist. -- Zusätzlich kann h1 an Stelle vom Beweis and.left h später verwendet werden. have h1:A, from and.left h, have h2:A∧B, from and.intro h1 hB, show (A∧B) ∨ (A∧C), from or.inl h2 ) (assume hC:C, have h1:A, from and.left h, have h2:A∧C, from and.intro h1 hC, show (A∧B) ∨ (A∧C), from or.inr h2 ) ) variable R : Prop variable S : Prop variable T : Prop #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \sourceoff Ist folgende Behauptung richtig: Die Variable h2 hat den Typ A∧B und den Wert (R∧R) ∧ (S∧S) bei obigem Aufruf #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \quoteoff Der Typ der Variablen h2 (ich nehme an, du meinst die erste dieses Namens) ist lokal gesehen A∧B, und hat den Wert and.intro h1 hB, also eigentlich nicht mehr als das Paar (h1,hB). Etwas mehr von außen betrachtet kann man bei der von dir angegebenen Benutzung mehr oder weniger sagen, h2 habe den Typ (R∧R) ∧ (S∧S). Dies ergibt sich, daraus, dass für A eben (R∧R) "eingesetzt" wird und für B (S∧S).


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.26, vom Themenstarter, eingetragen 2021-10-26

\quoteon(2021-10-25 22:39 - tactac in Beitrag No. 25) \quoteon(2021-10-25 21:15 - carlox in Beitrag No. 23) \sourceon lean theorem distribute_and_verteilen_2 (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := (assume h : A ∧ (B∨C), or.elim(and.right(h)) (assume hB:B, -- have h1:A prüft, ob A and.left h ein Beweis von A ist. -- Zusätzlich kann h1 an Stelle vom Beweis and.left h später verwendet werden. have h1:A, from and.left h, have h2:A∧B, from and.intro h1 hB, show (A∧B) ∨ (A∧C), from or.inl h2 ) (assume hC:C, have h1:A, from and.left h, have h2:A∧C, from and.intro h1 hC, show (A∧B) ∨ (A∧C), from or.inr h2 ) ) variable R : Prop variable S : Prop variable T : Prop #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \sourceoff Ist folgende Behauptung richtig: Die Variable h2 hat den Typ A∧B und den Wert (R∧R) ∧ (S∧S) bei obigem Aufruf #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \quoteoff Der Typ der Variablen h2 (ich nehme an, du meinst die erste dieses Namens) ist lokal gesehen A∧B, und hat den Wert and.intro h1 hB, also eigentlich nicht mehr als das Paar (h1,hB). Etwas mehr von außen betrachtet kann man bei der von dir angegebenen Benutzung mehr oder weniger sagen, h2 habe den Typ (R∧R) ∧ (S∧S). Dies ergibt sich, daraus, dass für A eben (R∧R) "eingesetzt" wird und für B (S∧S). \quoteoff Unter dem Wert einer Variablen verstehe ich die Definition wie sie in einer imperativen Programmiersprache wie z.B. C verwendet wird. Von C aus betrachtet sehe ich das so: h2 = and.intro h1 hB Und and.intro h1 hB ist der Ausdruck ("Term"), der der Variable h2 einen Wert (und keinen Typ) zuweist. and.intro h1 hB ist also kein Wert, sondern ein "Term" (wie z.B. x+y) der einen Wert berechnet und der Variablen h2 zuweist Aber in Lean ist das irgendwie ganz anders. Was muss ich an meiner C-Denkweise ändern, damit ich Lean verstehe? Wie verwendet man die Begriffe Wert,Typ,Variable, Zuweisung in Lean im Gegensatz zu der Benutzung in C ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.27, eingetragen 2021-10-27

\quoteon(2021-10-26 10:18 - carlox in Beitrag No. 26) \quoteon(2021-10-25 22:39 - tactac in Beitrag No. 25) \quoteon(2021-10-25 21:15 - carlox in Beitrag No. 23) \sourceon lean theorem distribute_and_verteilen_2 (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) := (assume h : A ∧ (B∨C), or.elim(and.right(h)) (assume hB:B, -- have h1:A prüft, ob A and.left h ein Beweis von A ist. -- Zusätzlich kann h1 an Stelle vom Beweis and.left h später verwendet werden. have h1:A, from and.left h, have h2:A∧B, from and.intro h1 hB, show (A∧B) ∨ (A∧C), from or.inl h2 ) (assume hC:C, have h1:A, from and.left h, have h2:A∧C, from and.intro h1 hC, show (A∧B) ∨ (A∧C), from or.inr h2 ) ) variable R : Prop variable S : Prop variable T : Prop #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \sourceoff Ist folgende Behauptung richtig: Die Variable h2 hat den Typ A∧B und den Wert (R∧R) ∧ (S∧S) bei obigem Aufruf #check distribute_and_verteilen_2 (R∧R) (S∧S) (T∧T) \quoteoff Der Typ der Variablen h2 (ich nehme an, du meinst die erste dieses Namens) ist lokal gesehen A∧B, und hat den Wert and.intro h1 hB, also eigentlich nicht mehr als das Paar (h1,hB). Etwas mehr von außen betrachtet kann man bei der von dir angegebenen Benutzung mehr oder weniger sagen, h2 habe den Typ (R∧R) ∧ (S∧S). Dies ergibt sich, daraus, dass für A eben (R∧R) "eingesetzt" wird und für B (S∧S). \quoteoff Unter dem Wert einer Variablen verstehe ich die Definition wie sie in einer imperativen Programmiersprache wie z.B. C verwendet wird. Von C aus betrachtet sehe ich das so: h2 = and.intro h1 hB Und and.intro h1 hB ist der Ausdruck ("Term"), der der Variable h2 einen Wert (und keinen Typ) zuweist. and.intro h1 hB ist also kein Wert, sondern ein "Term" (wie z.B. x+y) der einen Wert berechnet und der Variablen h2 zuweist \quoteoff Ja, streng genommen, ist and.intro h1 hB ein Term. Dessen Wert ist and.intro x y, wenn x der Wert des Teilausdrucks h1 und y der Wert des Teilausdrucks hB ist. and.intro rechnet jedenfalls nicht groß mit seinen Argumenten herum, sondern ist einfach ein Paar-Konstruktor mit einem speziellen Namen. \quoteon Aber in Lean ist das irgendwie ganz anders. Was muss ich an meiner C-Denkweise ändern, damit ich Lean verstehe? \quoteoff Nein, eigentlich nicht. Es könnte sein, dass du dich mit induktiven Datentypen vertraut machen musst, wie es sie auch in F#, Swift und Haskell gibt, um Wertkonstruktoren zu verstehen. \quoteon Wie verwendet man die Begriffe Wert,Typ,Variable, Zuweisung in Lean im Gegensatz zu der Benutzung in C ? \quoteoff Zuweisungen gibt es nicht so recht, jedenfalls nicht im vollen Sinn mit Überschreibung eines vorhandenen Werts. Aber eigentlich ist alles ganz normal. Vielleicht hilft ja ein Vergleich mit Java, wo man auch ungefähr Aussagenlogik wie in Lean machen kann (nur dass man eben keine speziellen Typen für Propositionen hat und stattdessen eben ganz normale Typen wie alle anderen als Propositionen interpretiert). \sourceon Java import java.util.function.Function; class And { private A a; private B b; public static And intro(A a, B b) { return new And(a,b); } private And(A a, B b) { this.a = a; this.b = b; } public A fst() { return a; } public B snd() { return b; } } abstract class Or { public abstract C elim(Function f, Function g); public static Or inl(A a) { return new Or() { @Override public C elim(Function f, Function g) { return f.apply(a); } }; } public static Or inr(B b) { return new Or() { @Override public C elim(Function f, Function g) { return g.apply(b); } }; } } class Examples { static Or,And> distribute1(And> p) { return p.snd().elim( b -> Or.inl(And.intro(p.fst(),b)), c -> Or.inr(And.intro(p.fst(),c)) ); } static And> distribute2(Or,And> s) { return s.elim( ab -> And.intro(ab.fst(),Or.inl(ab.snd())), ac -> And.intro(ac.fst(),Or.inr(ac.snd())) ); } static And,Or> distribute3(Or> s) { return s.elim( a -> And.intro(Or.inl(a), Or.inl(a)), bc -> And.intro(Or.inr(bc.fst()), Or.inr(bc.snd())) ); } static Or> distribute4(And,Or> p) { return p.fst().elim( a -> Or.inl(a), b -> p.snd().elim( a -> Or.inl(a), c -> Or.inr(And.intro(b,c)) ) ); } } \sourceoff


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1335
  Beitrag No.28, vom Themenstarter, eingetragen 2021-10-27

\quoteon Es könnte sein, dass du dich mit induktiven Datentypen vertraut machen musst, wie es sie auch in F#, Swift und Haskell gibt, um Wertkonstruktoren zu verstehen. ... Zuweisungen gibt es nicht so recht, jedenfalls nicht im vollen Sinn mit Überschreibung eines vorhandenen Werts. Aber eigentlich ist alles ganz normal. \quoteoff Ich komme irgendwie nicht weiter. Mein Denken ist immer noch C-behaftet. Sollte ich vielleicht vorher eine funktionale Programmiersprache lernen? Vielleicht Haskell? Was meinst du? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2275
  Beitrag No.29, eingetragen 2021-10-28

\quoteon(2021-10-27 11:13 - carlox in Beitrag No. 28) \quoteon Es könnte sein, dass du dich mit induktiven Datentypen vertraut machen musst, wie es sie auch in F#, Swift und Haskell gibt, um Wertkonstruktoren zu verstehen. ... Zuweisungen gibt es nicht so recht, jedenfalls nicht im vollen Sinn mit Überschreibung eines vorhandenen Werts. Aber eigentlich ist alles ganz normal. \quoteoff Ich komme irgendwie nicht weiter. Mein Denken ist immer noch C-behaftet. Sollte ich vielleicht vorher eine funktionale Programmiersprache lernen? Vielleicht Haskell? Was meinst du? \quoteoff Es kann zumindest nicht schaden. Viele Konzepte von Haskell und ähnlichem finden sich fast direkt in Lean (und Agda, Idris, ...).


   Profil
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.

Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2021 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]