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.
A 'list' von Koeffizienten könnte eine einfachere Definition sein mit –
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? –
@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