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: 1250
  Themenstart: 2021-10-05 13:12

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: 2187
  Beitrag No.1, eingetragen 2021-10-05 20:37

\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: 1250
  Beitrag No.2, vom Themenstarter, eingetragen 2021-10-06 11:27

\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: 2187
  Beitrag No.3, eingetragen 2021-10-06 21:21

\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: 1250
  Beitrag No.4, vom Themenstarter, eingetragen 2021-10-07 20:12

\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: 2187
  Beitrag No.5, eingetragen 2021-10-07 22:16

\(\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: 1250
  Beitrag No.6, vom Themenstarter, eingetragen 2021-10-09 12:40

\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: 2187
  Beitrag No.7, eingetragen 2021-10-09 21:45

\(\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: 1250
  Beitrag No.8, vom Themenstarter, eingetragen 2021-10-11 10:52

\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: 2187
  Beitrag No.9, eingetragen 2021-10-11 21:58

\(\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: 1250
  Beitrag No.10, vom Themenstarter, eingetragen 2021-10-12 14:11

\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: 2187
  Beitrag No.11, eingetragen 2021-10-12 17:19

\(\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: 1250
  Beitrag No.12, vom Themenstarter, eingetragen 2021-10-12 18:11

\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: 2187
  Beitrag No.13, eingetragen 2021-10-12 21:29

\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: 1250
  Beitrag No.14, vom Themenstarter, eingetragen 2021-10-13 09:56

\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: 2187
  Beitrag No.15, eingetragen 2021-10-13 22:56

\(\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: 1250
  Beitrag No.16, vom Themenstarter, eingetragen 2021-10-19 17:00

\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 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]