You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
|
|
|
|
import TestGame.Metadata
|
|
|
|
|
|
import Mathlib.Tactic.Ring
|
|
|
|
|
|
|
|
|
|
|
|
--set_option tactic.hygienic false
|
|
|
|
|
|
|
|
|
|
|
|
Game "TestGame"
|
|
|
|
|
|
World "Nat"
|
|
|
|
|
|
Level 1
|
|
|
|
|
|
|
|
|
|
|
|
Title "Natürliche Zahlen"
|
|
|
|
|
|
|
|
|
|
|
|
Introduction
|
|
|
|
|
|
"
|
|
|
|
|
|
Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon begegnet. Dabei haben wir
|
|
|
|
|
|
gesehen, dass explizite Gleichungen wie `2 + 3 * 5 = 17` implementationsbedingt
|
|
|
|
|
|
bereits mit `rfl` bewiesen werden können.
|
|
|
|
|
|
|
|
|
|
|
|
Algemeinere Gleichungen mit Variablen kann man mit der Taktik `ring` lösen.
|
|
|
|
|
|
"
|
|
|
|
|
|
|
|
|
|
|
|
Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
|
|
|
|
|
|
ring
|
|
|
|
|
|
|
|
|
|
|
|
Conclusion
|
|
|
|
|
|
"
|
|
|
|
|
|
Die Taktik heisst übrigens `ring` weil sie dafür entwickelt wurde, Gleichungen in einem abstrakten
|
|
|
|
|
|
Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
|
|
|
|
|
|
(erst `ℤ` ist ein Ring).
|
|
|
|
|
|
"
|
|
|
|
|
|
|
|
|
|
|
|
Tactics ring
|
