2017-10-19 22 views
1

Für meine erste Formalisierung. Ich möchte Polynome in Lean definieren. Der erste Versuch ist unten dargestellt:Testen der Polynomdefinition (von natürlichen Zahlen zu ganzen Zahlen)

def polynomial (f : ℕ → ℤ ) (p: (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (f n = (0:ℤ) ))):= f 

Jetzt Kauf meine Definition zu testen, mit:

def test : ℕ → ℤ 
| 0 := (2:ℤ) 
| 1 := (3:ℤ) 
| 2 := (4:ℤ) 
| _ := (0:ℤ) 

Aber Ich habe Probleme, den Beweis Begriff Konstruktion:

def prf : (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (test n = (0:ℤ) )):= 
exists.intro (3:ℕ) (
assume n : ℕ, 
nat.rec_on (n:ℕ) 
() 
() 
) 

Auch Feedback auf die Definition selbst ist willkommen.

+0

A 'list' von Koeffizienten könnte eine einfachere Definition sein mit –

+0

arbeiten @ SebastianUllrich Ich habe das berücksichtigt, aber was, wenn du eine Addition und Multiplikation definieren willst, ist das nicht schwieriger, wenn du zwei Polynome unterschiedlichen Grades hast? –

+0

@JensWageMaker-Listen werden ein wenig einfacher, aber wir brauchen noch eine Annahme: Wenn die Liste nicht leer ist, sollte das Kopfelement nicht "0" sein. Andernfalls hätten wir "0 * x + 1" und "1" unterschiedliche Polynome. List geht davon aus, dass der Kopf der Liste die niedrigeren Koeffizienten ist, d. H. "[A, b, c]" repräsentiert das Polynom "c * x^2 + b * x + a". Für 'prf': In diesem Fall wollen Sie keine Rekursion verwenden, sondern' match'. Die Fälle 0, 1 und 2 sollten mit dem Beweis 'dec_trivial' arbeiten. – Johannes

Antwort

1

Die Formulierung def polynomial funktioniert nicht. Sie Tag Ihre Funktion ein Polynom sein, aber das kann nicht von der Logik selbst verwendet werden. Insbesondere erlaubt es uns nicht, Typklasseninstanzen für Polynome einzurichten.

Was wollen wir ein Subtyp statt:

def polynomial (A : Type) [ring A] : Type := 
{p : ℕ -> A // ∃ m : ℕ, ∀ n ≥ m, p n = 0} 

damit wir können Setup eine Instanz

instance {A : Type} [ring A] : polynomial A := ...

+0

Was bedeutet "//"? Auch ich kann nicht finden, was {...} bedeutet, erklärst du hier eine Struktur? Ist es möglich, dieselbe Definition ausführlicher zu machen? –

+0

'{x: A // p x}' ist der Subtyp aller Elemente 'x' in' A', für die 'px' gilt. Das '//' ist Teil der '{_: _ // _}' Syntax. – Johannes

Verwandte Themen