Italian translation of NNG4 (#84)
* begin translation * continue * Progress * begin translating Addition world * Progress * Copy original to untranslated and mark as fuzzy * most of Power World * start translating Implication World * continue Implication World * continue Implication World * translate Algorithm World * translate Advanced Addition World * start Inequality World * continue Inequality World * substitute with js script * translate Inequality World * traslate Advanced Multiplication World * last few messages * a few corrections * credits * add generated json * clean up Tutorial World * Update .i18n/it/Game.json Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> * Update .i18n/it/Game.json Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> * Update .i18n/it/Game.json Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> * Update .i18n/it/Game.json Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> * Update .i18n/it/Game.json Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> * reflect corrections in Game.po * review Addition World * review Multiplication World * review Implication World * review Power World * go over Advanced Addition and >= worlds * review Algorithm World, intro * nitpicking --------- Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
This commit is contained in:
Federico Dal Pio Luogo
committed by
GitHub
GitHub
parent
36a82b7cfd
commit
ff20831ad7
878
.i18n/it/Game.json
Normal file
878
.i18n/it/Game.json
Normal file
@@ -0,0 +1,878 @@
|
||||
{"≤ World": "Mondo ≤",
|
||||
"≠": "≠",
|
||||
"zero_pow_zero": "zero_pow_zero",
|
||||
"zero_pow_succ": "zero_pow_succ",
|
||||
"zero_ne_succ": "zero_ne_succ",
|
||||
"zero_mul": "zero_mul",
|
||||
"zero_add": "zero_add",
|
||||
"x ≤ y or y ≤ x": "x ≤ y o y ≤ x",
|
||||
"x ≤ y and y ≤ z implies x ≤ z": "x ≤ y e y ≤ z implica x ≤ z",
|
||||
"x ≤ y and y ≤ x implies x = y": "x ≤ y e y ≤ x implica x = y",
|
||||
"x ≤ succ x": "x ≤ succ x",
|
||||
"x ≤ 1": "x ≤ 1",
|
||||
"x ≤ 0 → x = 0": "x ≤ 0 → x = 0",
|
||||
"two_mul": "two_mul",
|
||||
"try rewriting `add_zero`.": "prova a riscrivere `add_zero`.",
|
||||
"the simplest approach": "l'approccio più semplice",
|
||||
"the rw tactic": "la tattica rw",
|
||||
"succ_mul": "succ_mul",
|
||||
"succ_inj : the successor function is injective":
|
||||
"succ_inj : la funzione successore è iniettiva",
|
||||
"succ_add": "succ_add",
|
||||
"succ x ≤ succ y → x ≤ y": "succ x ≤ succ y → x ≤ y",
|
||||
"rewriting backwards": "riscrivere all'indietro",
|
||||
"pred": "pred",
|
||||
"pow_two": "pow_two",
|
||||
"pow_pow": "pow_pow",
|
||||
"pow_one": "pow_one",
|
||||
"pow_add": "pow_add",
|
||||
"one_pow": "one_pow",
|
||||
"one_mul": "one_mul",
|
||||
"one_le_of_ne_zero": "one_le_of_ne_zero",
|
||||
"mul_right_eq_self": "mul_right_eq_self",
|
||||
"mul_right_eq_one": "mul_right_eq_one",
|
||||
"mul_pow": "mul_pow",
|
||||
"mul_one": "mul_one",
|
||||
"mul_ne_zero": "mul_ne_zero",
|
||||
"mul_left_ne_zero": "mul_left_ne_zero",
|
||||
"mul_left_cancel": "mul_left_cancel",
|
||||
"mul_le_mul_right": "mul_le_mul_right",
|
||||
"mul_eq_zero": "mul_eq_zero",
|
||||
"mul_comm": "mul_comm",
|
||||
"mul_assoc": "mul_assoc",
|
||||
"mul_add": "mul_add",
|
||||
"making life simple": "semplifichiamoci la vita",
|
||||
"making life easier": "semplifichiamoci la vita",
|
||||
"level completed! 🎉": "livello completato! 🎉",
|
||||
"level completed with warnings… 🎭":
|
||||
"livello completato, ma ci sono dei warning... 🎭",
|
||||
"le_two": "le_two",
|
||||
"le_mul_right": "le_mul_right",
|
||||
"is_zero": "is_zero",
|
||||
"intro practice": "esercizi su intro",
|
||||
"intro": "intro",
|
||||
"intermediate goal solved! 🎉": "goal intermedio risolto! 🎉",
|
||||
"eq_succ_of_ne_zero": "eq_succ_of_ne_zero",
|
||||
"decide again": "decide, ancora",
|
||||
"decide": "decide",
|
||||
"add_succ": "add_succ",
|
||||
"add_sq": "add_sq",
|
||||
"add_right_eq_zero": "add_right_eq_zero",
|
||||
"add_right_eq_self": "add_right_eq_self",
|
||||
"add_right_comm": "add_right_comm",
|
||||
"add_right_cancel": "add_right_cancel",
|
||||
"add_mul": "add_mul",
|
||||
"add_left_eq_zero": "add_left_eq_zero",
|
||||
"add_left_eq_self": "add_left_eq_self",
|
||||
"add_left_comm": "add_left_comm",
|
||||
"add_left_cancel": "add_left_cancel",
|
||||
"add_comm (level boss)": "add_comm (livello boss)",
|
||||
"add_assoc (associativity of addition)":
|
||||
"add_assoc (proprietà associativa dell'addizione)",
|
||||
"`ℕ` is the natural numbers, just called \\\"numbers\\\" in this game. It's\ndefined via two rules:\n\n* `0 : ℕ` (zero is a number)\n* `succ (n : ℕ) : ℕ` (the successor of a number is a number)\n\n## Game Implementation\n\n*The game uses its own copy of the natural numbers, called `MyNat` with notation `ℕ`.\nIt is distinct from the Lean natural numbers `Nat`, which should hopefully\nnever leak into the natural number game.*":
|
||||
"`ℕ` denota l'insieme dei numeri naturali, che chiameremo semplicemente \\\"numeri \\\" nel resto del gioco. Questo insieme è\ndefinito tramite due regole:\n\n* `0 : ℕ` (zero è un numero)\n* `succ (n: ℕ): ℕ` (il successore di un numero è un numero)\n\n## Implementazione del gioco \n\n*Il gioco usa una versione propria dei numeri naturali - chiamata `Mynat` con notazione` ℕ` -\ndiversa dal tipo primitivo dei numeri naturali di Lean `Nat`; quest'ultimo\nnon dovrebbe venire utilizzato nel contesto del gioco.*",
|
||||
"`zero_ne_succ n` is the proof that `0 ≠ succ n`.\n\nIn Lean, `a ≠ b` is *defined to mean* `a = b → False`. Hence\n`zero_ne_succ n` is really a proof of `0 = succ n → False`.\nHere `False` is a generic false statement. This means that\nyou can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`.":
|
||||
"`zero_ne_succ n` è la dimostrazione che `0 ≠ succ n`.\n\nIn Lean, `a ≠ b` è *definito come* `a = b → False`. Dunque\n`zero_ne_succ n` è in realtà la dimostrazione di `0 = succ n → False`.\nQui `False` è la proposizione false più banale. Essendo un'implicazione\npuoi applicarla ad una `h` che dimostra `0 = succ n` con `apply zero_ne_succ at h`.",
|
||||
"`zero_ne_one` is a proof of `0 ≠ 1`.":
|
||||
"`zero_ne_one` è la dimostrazione di `0 ≠ 1`.",
|
||||
"`zero_mul x` is the proof that `0 * x = 0`.\n\nNote: `zero_mul` is a `simp` lemma.":
|
||||
"`zero_mul x` è la dimostrazione di `0 * x = 0`.\n\nNB: `zero_mul` è un lemma di semplificazione (`simp`).",
|
||||
"`zero_le x` is a proof that `0 ≤ x`.":
|
||||
"`zero_le x` è la dimostrazione che `0 ≤ x`.",
|
||||
"`zero_add x` is the proof of `0 + x = x`.\n\n`zero_add` is a `simp` lemma, because replacing `0 + x` by `x`\nis almost always what you want to do if you're simplifying an expression.":
|
||||
"`zero_add x` è la dimostrazione di `0 + x = x`.\n\n`zero_add` è un lemma del tipo `simp` (semplificazione), infatti sostituire `0 + x` con `x`\nè quasi sempre uno dei passi più ovvi della semplificazione di un'espressione.",
|
||||
"`xyzzy` is an ancient magic spell, believed to be the origin of the\nmodern word `sorry`. The game won't complain - or notice - if you\nprove anything with `xyzzy`.":
|
||||
"`xyzzy` è un incantesimo arcaico, si crede che sia l'origine\ndella parola inglese `sorry`. Il gioco non si lamenterà - e nemmeno noterà - se\nrisolvi tutti i livelli con `xyzzy`.",
|
||||
"`two_mul m` is the proof that `2 * m = m + m`.":
|
||||
"`two_mul m` è la dimostrazione che `2 * m = m + m`.",
|
||||
"`two_eq_succ_one` is a proof of `2 = succ 1`.":
|
||||
"`two_eq_succ_one` è la dimostrazione di `2 = succ 1`.",
|
||||
"`three_eq_succ_two` is a proof of `3 = succ 2`.":
|
||||
"`three_eq_succ_two` è la dimostrazione di `3 = succ 2`.",
|
||||
"`tauto` is good enough to solve this goal.":
|
||||
"`tauto` è in grado di risolvere questo goal.",
|
||||
"`succ_ne_zero a` is a proof of `succ a ≠ 0`.":
|
||||
"`succ_ne_zero a` è la dimostrazione di `succ a ≠ 0`.",
|
||||
"`succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`.":
|
||||
"`succ_ne_succ m n` è la dimostrazione di `m ≠ n → succ m ≠ succ n`.",
|
||||
"`succ_mul a b` is the proof that `succ a * b = a * b + b`.\n\nIt could be deduced from `mul_succ` and `mul_comm`, however this argument\nwould be circular because the proof of `mul_comm` uses `mul_succ`.":
|
||||
"`succ_mul a b` è la dimostrazione di `succ a * b = a * b + b`.\n\nQuesto lemma potrebbe essere dedotto da `mul_succ` e `mul_comm`, ma risulterebbe\nin un ragionamento circolare in quanto la dimostrazione di `mul_comm` dipende da `mul_succ`.",
|
||||
"`succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`.":
|
||||
"`succ_le_succ x y` è la dimostrazione che se `succ x ≤ succ y`, allora `x ≤ y`.",
|
||||
"`succ_eq_add_one n` is the proof that `succ n = n + 1`.":
|
||||
"`succ_eq_add_one n` è la dimostrazione di `succ n = n + 1`.",
|
||||
"`succ_add a b` is a proof that `succ a + b = succ (a + b)`.":
|
||||
"`succ_add a b` è la dimostrazione che `succ a + b = succ (a + b)`.",
|
||||
"`rw [one_eq_succ_zero]` will do this.":
|
||||
"`rw [one_eq_succ_zero]` per espandere.",
|
||||
"`rw [add_zero]` will change `b + 0` into `b`.":
|
||||
"`rw [add_zero]` trasformerà `b + 0` in `b`.",
|
||||
"`rw [add_comm b d]`.": "`rw [add_comm b d]`.",
|
||||
"`pred_succ n` is a proof of `pred (succ n) = n`.":
|
||||
"`pred_succ n` è la dimostrazione di `pred (succ n) = n`.",
|
||||
"`pow_zero a : a ^ 0 = 1` is one of the two axioms\ndefining exponentiation in this game.":
|
||||
"`pow_zero a : a ^ 0 = 1` è uno dei due assiomi che\ndefiniscono l'elevamento a potenza in questo gioco.",
|
||||
"`pow_two a` says that `a ^ 2 = a * a`.":
|
||||
"`pow_two a` afferma `a ^ 2 = a * a`.",
|
||||
"`pow_succ a b : a ^ (succ b) = a ^ b * a` is one of the\ntwo axioms defining exponentiation in this game.":
|
||||
"`pow_succ a b : a ^ (succ b) = a ^ b * a` è uno dei\ndue assiomi che definiscono l'elevamento a potenza in questo gioco.",
|
||||
"`pow_pow a m n` is a proof that $(a^m)^n=a^{mn}.$":
|
||||
"`pow_pow a m n` è la dimostrazione di $(a^m)^n=a^{mn}.$",
|
||||
"`pow_one a` says that `a ^ 1 = a`.\n\nNote that this is not quite true by definition: `a ^ 1` is\ndefined to be `a ^ 0 * a` so it's `1 * a`, and to prove\nthat this is equal to `a` you need to use induction somewhere.":
|
||||
"`pow_one a` afferma `a ^ 1 = a`.\n\nQuesto fatto non deriva direttamente dalla definizione: `a ^ 1` si\nespande in `a ^ 0 * a` ovvero `1 * a`, e abbiamo visto che per dimostrare\nche tale prodotto è uguale ad `a` bisogna usare l'induzione.",
|
||||
"`pow_add a m n` is a proof that $a^{m+n}=a^ma^n.$":
|
||||
"`pow_add a m n` è la dimostrazione che $a^{m+n}=a^ma^n.$",
|
||||
"`one_pow n` is a proof that $1^n=1$.":
|
||||
"`one_pow n` è la dimostrazione che $1^n=1$.",
|
||||
"`one_ne_zero` is a proof that `1 ≠ 0`.":
|
||||
"`one_ne_zero` è la dimostrazione di `1 ≠ 0`.",
|
||||
"`one_mul m` is the proof `1 * m = m`.":
|
||||
"`one_mul m` è la dimostrazione che `1 * m = m`.",
|
||||
"`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`.":
|
||||
"`one_le_of_ne_zero a` è la dimostrazione che `a ≠ 0 → 1 ≤ a`.",
|
||||
"`one_eq_succ_zero` is a proof of `1 = succ 0`.\"":
|
||||
"`one_eq_succ_zero` è la dimostrazione di `1 = succ 0`.\"",
|
||||
"`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`.":
|
||||
"`nth_rewrite 2 [two_eq_succ_one]` più veloce di `rw [two_eq_succ_one]`, secondo me.",
|
||||
"`mul_zero m` is the proof that `m * 0 = 0`.":
|
||||
"`mul_zero m` è la dimostrazione di `m * 0 = 0`.",
|
||||
"`mul_succ a b` is the proof that `a * succ b = a * b + a`.":
|
||||
"`mul_succ a b` è la dimostrazione di `a * succ b = a * b + a`.",
|
||||
"`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`.":
|
||||
"`mul_right_eq_self a b` è la dimostrazione che se `a ≠ 0` e `a * b = a` allora `b = 1`.",
|
||||
"`mul_right_eq_one a b` is a proof that `a * b = 1 → a = 1`.":
|
||||
"`mul_right_eq_one a b` è la dimostrazione che `a * b = 1 → a = 1`.",
|
||||
"`mul_pow a b n` is a proof that $(ab)^n=a^nb^n.$":
|
||||
"`mul_pow a b n` è la dimostrazione che $(ab)^n=a^nb^n.$",
|
||||
"`mul_one m` is the proof that `m * 1 = m`.":
|
||||
"`mul_one m` è la dimostrazione di `m * 1 = m`.",
|
||||
"`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`.":
|
||||
"`mul_ne_zero a b` è la dimostrazione che se `a ≠ 0` e `b ≠ 0` allora `a * b ≠ 0`.",
|
||||
"`mul_left_ne_zero a b` is a proof that `a * b ≠ 0 → b ≠ 0`.":
|
||||
"`mul_left_ne_zero a b` è la dimostrazione che `a * b ≠ 0 → b ≠ 0`.",
|
||||
"`mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`.":
|
||||
"`mul_left_cancel a b c` è la dimostrazione che se `a ≠ 0` e `a * b = a * c` allora `b = c`.",
|
||||
"`mul_le_mul_right a b t` is a proof that `a ≤ b → a * t ≤ b * t`.":
|
||||
"`mul_le_mul_right a b t` è la dimostrazione che `a ≤ b → a * t ≤ b * t`.",
|
||||
"`mul_eq_zero a b` is a proof that if `a * b = 0` then `a = 0` or `b = 0`.":
|
||||
"`mul_eq_zero a b` è la dimostrazione che se `a * b = 0` allora `a = 0` or `b = 0`.",
|
||||
"`mul_comm` is the proof that multiplication is commutative. More precisely,\n`mul_comm a b` is the proof that `a * b = b * a`.":
|
||||
"`mul_comm` è la dimostrazione che la moltiplicazione è commutativa. Più precisamente,\n`mul_comm a b` è la dimostrazione che `a * b = b * a`.",
|
||||
"`mul_assoc a b c` is a proof that `(a * b) * c = a * (b * c)`.\n\nNote that when Lean says `a * b * c` it means `(a * b) * c`.\n\nNote that `(a * b) * c = a * (b * c)` cannot be proved by \\\"pure thought\\\":\nfor example subtraction is not associative, as `(6 - 2) - 1` is not\nequal to `6 - (2 - 1)`.":
|
||||
"`mul_assoc a b c` è la dimostrazione che `(a * b) * c = a * (b * c)`.\n\nRicorda che Lean per `a * b * c` intende `(a * b) * c`.\n\nRicorda che `(a * b) * c = a * (b * c)` non è una legge universale della matematica\":\nun esempio famoso di operazione non associativa è la sottrazione, dato che `(6 - 2) - 1` non è\nuguale a `6 - (2 - 1)`.",
|
||||
"`le_zero x` is a proof of the implication `x ≤ 0 → x = 0`.":
|
||||
"`le_zero x` è la dimostrazione dell'implicazione `x ≤ 0 → x = 0`.",
|
||||
"`le_zero x` is a proof of `x ≤ 0 → x = 0`.":
|
||||
"`le_zero x` è la dimostrazione di `x ≤ 0 → x = 0`.",
|
||||
"`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`.":
|
||||
"`le_two x` è la dimostrazione che se `x ≤ 2` allora `x = 0` o `x = 1` or `x = 2`.",
|
||||
"`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.\nMore precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,\nIf $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.\n\n## A note on associativity\n\nIn Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However\n`→` is right associative. This means that `x ≤ y → y ≤ z → x ≤ z` in Lean means\nexactly that `≤` is transitive. This is different to how mathematicians use\n$P \\implies Q \\implies R$; for them, this usually means that $P \\implies Q$\nand $Q \\implies R$.":
|
||||
"`le_trans x y z` è la dimostrazione che se `x ≤ y` e `y ≤ z` allora `x ≤ z`.\nRiscritto in termini logici, è la dimostrazione che `x ≤ y → (y ≤ z → x ≤ z)`. Questa formula si legge ad alta voce così:\nSe $x \\le y$ allora (pausa) se $y \\le z$ allora $x \\le z$.\n\n## Nota sull'associatività\n\nCome sai già, in Lean `a + b + c` sta per `(a + b) + c`, dato che `+` associa a sinistra. Invece l'implicazione\n`→` associa a destra. Dunque su Lean possiamo scrivere direttamente `x ≤ y → y ≤ z → x ≤ z`, che codifica\nproprio la proprietà transitiva di `≤`. Attenzione però, in quanto a volte i matematici interpretano le sequenze di `→` diversamente; \nper alcuni, $P \\implies Q \\implies R$ si traduce nella congiunzione $P \\implies Q$\ne $Q \\implies R$.",
|
||||
"`le_total x y` is a proof that `x ≤ y` or `y ≤ x`.":
|
||||
"`le_total x y` è la dimostrazione che `x ≤ y` or `y ≤ x`.",
|
||||
"`le_succ_self x` is a proof that `x ≤ succ x`.":
|
||||
"`le_succ_self x` è la dimostrazione che `x ≤ succ x`.",
|
||||
"`le_refl x` is a proof of `x ≤ x`.\n\nThe reason for the name is that this lemma is \"reflexivity of $\\le$\"":
|
||||
"`le_refl x` è la dimostrazione di `x ≤ x`.\n\nIl nome di questo lemma deriva da \"reflexivity of $\\le$\", dove \"le\"\nè l'abbreviazione tipica di \"less than or equal\" (minore o uguale)",
|
||||
"`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`.":
|
||||
"`le_one x` è la dimostrazione che se `x ≤ 1` allora `x = 0` or `x = 1`.",
|
||||
"`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.\n\nIt's one way of saying that a divisor of a positive number\nhas to be at most that number.":
|
||||
"`le_mul_right a b` è la dimostrazione che `a * b ≠ 0 → a ≤ a * b`.\n\nÈ un modo di dire che un divisore di un numero positivo dev'essere per forza\nal massimo il numero stesso.",
|
||||
"`le_antisymm x y` is a proof that if `x ≤ y` and `y ≤ x` then `x = y`.":
|
||||
"`le_antisymm x y` è la dimostrazione che `x ≤ y` e `y ≤ x` implica `x = y`.",
|
||||
"`is_zero_zero` is a proof of `is_zero 0 = True`.":
|
||||
"`is_zero_zero` è la dimostrazione di `is_zero 0 = True`.",
|
||||
"`is_zero_succ a` is a proof of `is_zero (succ a) = False`.":
|
||||
"`is_zero_succ a` è la dimostrazione di `is_zero (succ a) = False`.",
|
||||
"`four_eq_succ_three` is a proof of `4 = succ 3`.":
|
||||
"`four_eq_succ_three` è la dimostrazione di `4 = succ 3`.",
|
||||
"`exact` practice.": "esercizi su `exact`.",
|
||||
"`eq_succ_of_ne_zero a` is a proof that `a ≠ 0 → ∃ n, a = succ n`.":
|
||||
"`eq_succ_of_ne_zero a` è la dimostrazione che `a ≠ 0 → ∃ n, a = succ n`.",
|
||||
"`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.\nYou can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You\ncan usually stick to `rw [add_zero]` unless you need real precision.":
|
||||
"`add_zero c` è la dimostrazione di `c + 0 = c`, proprio quello che è stato riscritto.\nOra puoi scambiare `b + 0` con `b` scrivendo `rw [add_zero]` o `rw [add_zero b]`. Nella pratica, usa\n`rw [add_zero]` quando non hai bisogno di precisare il termine da sostituire.",
|
||||
"`add_zero a` is a proof that `a + 0 = a`.\n\n## Summary\n\n`add_zero` is really a function, which\neats a number, and returns a proof of a theorem\nabout that number. For example `add_zero 37` is\na proof that `37 + 0 = 37`.\n\nThe `rw` tactic will accept `rw [add_zero]`\nand will try to figure out which number you omitted\nto input.\n\n## Details\n\nA mathematician sometimes thinks of `add_zero`\nas \\\"one thing\\\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.\nThis is just another way of saying that it's a function which\ncan eat any number n and will return a proof that `n + 0 = n`.":
|
||||
"`add_zero a` è una prova della proposizione `a + 0 = a`.\n\n## Descrizione\n\n`add_zero` in realtà è una funzione, che\nprende un numero, e restituisce una dimostrazione di un teorema\nche riguarda proprio quel numero. Ad esempio `add_zero 37` è\nuna dimostrazione che `37 + 0 = 37`.\n\nLa tattica `rw`, se usata come in `rw [add_zero]`,\ntenterà di capire da sola quale sia il numero da passare a `add_zero`.\n\n\n## Dettagli\n\nAi matematici piace pensare a `add_zero`\ncome un'\\\"unica cosa\\\", ossia la dimostrazione che $\\forall n ∈ ℕ, n + 0 = n$.\nQuesta è un'altra notazione per dire che è una funzione che\nprende un qualsiasi numero n e restituisce una dimostrazione che `n + 0 = n`.",
|
||||
"`add_succ a b` is the proof of `a + succ b = succ (a + b)`.":
|
||||
"`add_succ a b` è la dimostrazione di `a + succ b = succ (a + b)`.",
|
||||
"`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$":
|
||||
"`add_sq a b` è l'enunciato $(a+b)^2=a^2+b^2+2ab.$",
|
||||
"`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\nTwo ways to do it spring to mind; I'll mention them when you've solved it.":
|
||||
"`add_right_eq_self x y` è il teorema $x + y = x\\implies y=0.$\nMi vengono in mente due modi per dimostrarlo, ma te li dirò una volta che lo dimostri.",
|
||||
"`add_right_eq_self x y` is the theorem that $x + y = x \\implies y=0.$":
|
||||
"`add_right_eq_self x y` è il teorema $x + y = x \\implies y=0.$",
|
||||
"`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n\nIn Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\nas `a + b + c = a + c + b`.":
|
||||
"`add_right_comm a b c` è la dimostrazione di `(a + b) + c = (a + c) + b`\n\nSu Lean, `a + b + c` è zucchero sintattico per `(a + b) + c`, quindi il nostro risultato verrà visualizzato\ncome `a + b + c = a + c + b`.",
|
||||
"`add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$":
|
||||
"`add_right_cancel a b n` è il teorema $a+n=b+n \\implies a=b.$",
|
||||
"`add_mul` is just as fiddly to prove by induction; but there's a trick\nwhich avoids it. Can you spot it?":
|
||||
"`add_mul` è altrettanto macchinoso da dimostrare per induzione; ma c'è un trucco\nche ci permette di evitarla. Sai individuarlo?",
|
||||
"`add_mul a b c` is a proof that $(a+b)c=ac+bc$.":
|
||||
"`add_mul a b c` è la dimostrazione che $(a+b)c=ac+bc$.",
|
||||
"`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$":
|
||||
"`add_left_eq_self x y` è il teorema $x + y = y\\implies x=0.$",
|
||||
"`add_left_eq_self x y` is the theorem that $x + y = y \\implies x=0.$":
|
||||
"`add_left_eq_self x y` è il teorema $x + y = y \\implies x=0.$",
|
||||
"`add_left_comm a b c` is a proof that `a + (b + c) = b + (a + c)`.":
|
||||
"`add_left_comm a b c` è la dimostrazione di `a + (b + c) = b + (a + c)`.",
|
||||
"`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.\nYou can prove it by induction on `n` or you can deduce it from `add_right_cancel`.":
|
||||
"`add_left_cancel a b n` è il teorema che dice $n+a=n+b\\implies a=b$.\nPuoi dimostrarlo facendo induzione su `n` oppure puoi dedurlo tramite `add_right_cancel`.",
|
||||
"`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$":
|
||||
"`add_left_cancel a b n` è il teorema $n+a=n+b \\implies a=b.$",
|
||||
"`add_comm x y` is a proof of `x + y = y + x`.":
|
||||
"`add_comm x y` è la dimostrazione di `x + y = y + x`.",
|
||||
"`add_comm b c` is a proof that `b + c = c + b`. But if your goal\nis `a + b + c = a + c + b` then `rw [add_comm b c]` will not\nwork! Because the goal means `(a + b) + c = (a + c) + b` so there\nis no `b + c` term *directly* in the goal.\n\nUse associativity and commutativity to prove `add_right_comm`.\nYou don't need induction. `add_assoc` moves brackets around,\nand `add_comm` moves variables around.\n\nRemember that you can do more targetted rewrites by\nadding explicit variables as inputs to theorems. For example `rw [add_comm b]`\nwill only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\nwill only do rewrites of the form `b + c = c + b`.":
|
||||
"`add_comm b c` è una dimostrazione di `b + c = c + b`. Ma se il goal\nè `a + b + c = a + c + b`, `rw [add_comm b c]` non funzionerà!\nQuesto perché il goal sta in realtà per `(a + b) + c = (a + c) + b`, e se guardi bene questo goal non include\nil termine `b + c` *direttamente*.\n\nUsa l'associatività e la commutatività per dimostrare `add_right_comm`.\nNon è necessario procedere per induzione. `add_assoc` sposta le parentesi,\ne `add_comm` sposta le variabili.\n\nRicorda che puoi fare sostituzioni mirate fornendo\nesplicitamente le variabili in input ai teoremi. Ad esempio `rw [add_comm b]`\nfarà solo sostituzioni della forma `b + ? = ? + b`, e `rw [add_comm b c]`\nfarà solo sostituzioni della forma `b + c = c + b`.",
|
||||
"`add_assoc a b c` is a proof\nthat `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\nas `a + b + c`, because the notation for addition is defined to be left\nassociative.":
|
||||
"`add_assoc a b c` è la dimostrazione\ndi `(a + b) + c = a + (b + c)`. Ricordati che in Lean `(a + b) + c` viene\nstampato come `a + b + c`, perché la notazione dell'addizione è left \nassociative.",
|
||||
"`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\nmeans \"there exists\". So `a ≤ b` means that there exists\na number `c` such that `b = a + c`. This definition works\nbecause there are no negative numbers in this game.\n\nTo *prove* an \"exists\" statement, use the `use` tactic.\nLet's see an example.":
|
||||
"`a ≤ b` è *notazione* per `∃ c, b = a + c`. La \"E rovesciata\"\nsi legge \"esiste\". Quindi `a ≤ b` vuol dire che esiste\nun numero `c` tale che `b = a + c`. Questa definizione è valida\nperché non abbiamo i numeri negativi in questo gioco.\n\nPer *dimostrare* un \"esiste\", puoi usare la tattica `use`.\nVediamo un esempio.",
|
||||
"`a ≤ b` is *notation* for `∃ c, b = a + c`.\n\nBecause this game doesn't have negative numbers, this definition\nis mathematically valid.\n\nThis means that if you have a goal of the form `a ≤ b` you can\nmake progress with the `use` tactic, and if you have a hypothesis\n`h : a ≤ b`, you can make progress with `cases h with c hc`.":
|
||||
"`a ≤ b` è *notazione* per `∃ c, b = a + c`.\n\nDato che in questo gioco non abbiamo i numeri negativi, questa definizione\nè matematicamente valida.\n\nUna conseguenza pratica di tale definizione è che se hai un goal della forma `a ≤ b` puoi\nscomporlo con la tattica `use`, e se hai un'ipotesi\n`h : a ≤ b`, puoi scomporla tramite `cases h with c hc`.",
|
||||
"`a ≠ b` is *notation* for `(a = b) → False`.\n\nThe reason this is mathematically\nvalid is that if `P` is a true-false statement then `P → False`\nis the logical opposite of `P`. Indeed `True → False` is false,\nand `False → False` is true!\n\nThe upshot of this is that use can treat `a ≠ b` in exactly\nthe same way as you treat any implication `P → Q`. For example,\nif your *goal* is of the form `a ≠ b` then you can make progress\nwith `intro h`, and if you have a hypothesis `h` of the\nform `a ≠ b` then you can `apply h at h1` if `h1` is a proof\nof `a = b`.":
|
||||
"`a ≠ b` è *notazione* per `(a = b) → False`.\n\nQuesta interpretazione è valida in matematica\nperché se `P` è una proposizione vero-falso allora `P → False`\nè la negazione logica di `P`. Infatti `True → False` è falso,\ne `False → False` è vero!\n\nIl vantaggio di questa notazione è che possiamo trattare una disuguaglianza `a ≠ b`\ncome se fosse un implicazione `P → Q`, che sappiamo già come manipolare. Ad esempio,\nse il tuo *goal* è una disuguaglianza `a ≠ b`, puoi fare progresso\ncon `intro h`, e se un'ipotesi `h` è una disuguaglianza\n`a ≠ b` allora puoi fare `apply h at h1` se `h1` è la prova di\ndi `a = b`.",
|
||||
"`Pow a b`, with notation `a ^ b`, is the usual\n exponentiation of natural numbers. Internally it is\n defined via two axioms:\n\n * `pow_zero a : a ^ 0 = 1`\n\n * `pow_succ a b : a ^ succ b = a ^ b * a`\n\nNote in particular that `0 ^ 0 = 1`.":
|
||||
"`Pow a b`, con notazione `a ^ b`, è\n l'elevamento a potenza sui numeri naturali. Dentro Lean è\n definita tramite due assiomi:\n\n * `pow_zero a : a ^ 0 = 1`\n\n * `pow_succ a b : a ^ succ b = a ^ b * a`\n\nIn particolare, dal primo segue che `0 ^ 0 = 1`.",
|
||||
"`Mul a b`, with notation `a * b`, is the usual\n product of natural numbers. Internally it is\n via two axioms:\n\n * `mul_zero a : a * 0 = 0`\n\n * `mul_succ a b : a * succ b = a * b + a`\n\nOther theorems about naturals, such as `zero_mul`,\nare proved by induction from these two basic theorems.":
|
||||
"`Mul a b`, con notazione `a * b`, è il solito\n prodotto tra numeri naturali. Dentro Lean è\n definito tramite due assiomi:\n\n * `mul_zero a : a * 0 = 0`\n\n * `mul_succ a b : a * succ b = a * b + a`\n\nTutti gli altri teoremi sulla moltiplicazione e i naturali, come `zero_mul`,\nsi dimostrano per induzione usando questi due assiomi fondamentali.",
|
||||
"`Add a b`, with notation `a + b`, is\nthe usual sum of natural numbers. Internally it is defined\nvia the following two hypotheses:\n\n* `add_zero a : a + 0 = a`\n\n* `add_succ a b : a + succ b = succ (a + b)`\n\nOther theorems about naturals, such as `zero_add a : 0 + a = a`, are proved\nby induction using these two basic theorems.\"":
|
||||
"`Add a b`, con la notazione `a + b`, è\nl'operazione di addizione sui numeri naturali. Dentro Lean è definita\ntramite due ipotesi:\n\n* `add_zero a : a + 0 = a`\n\n* `add_succ a b : a + succ b = succ (a + b)`\n\nGli altri teoremi sui numeri naturali e l'addizione, come `zero_add a : 0 + a = a`, si dimostrano\nper induzione usando questi due teoremi fondamentali.\"",
|
||||
"[final boss music]": "[final boss music]",
|
||||
"[dramatic music]. Now are you ready to face the first boss of the game?":
|
||||
"[musica drammatica] Sei pronto per affrontare il primo boss del gioco?",
|
||||
"[boss battle music]\n\nLook in your inventory to see the proofs you have available.\nThese should be enough.":
|
||||
"[musica da boss battle]\n\nSfrutta le dimostrazioni disponibili nel tuo inventario.\nDovrebbero bastarti.",
|
||||
"You've now seen all the tactics you need to beat the final boss of the game.\nYou can begin the journey towards this boss by entering Multiplication World.\n\nOr you can go off the beaten track and learn some new tactics in Implication\nWorld. These tactics let you prove more facts about addition, such as\nhow to deduce `a = 0` from `x + a = x`.\n\nClick \"Leave World\" and make your choice.":
|
||||
"Ora hai incontrato tutte le tattiche che ti servono per sconfiggere il boss finale del gioco.\nPuoi proseguire spedito la tua marcia verso il boss finale passando dal Mondo Moltiplicazione.\n\nOppure puoi fare una deviazione e imparare qualche nuova tattica esotica nel Mondo Implicazione.\nQueste tattiche ti permetteranno di dimostrare altre proprietà dell'addizione, ad esempio\ncome dedurre `a = 0` da `x + a = x`.\n\nPremi \"Abbandona mondo\" e scegli la tua strada.",
|
||||
"You want to use `add_right_eq_zero`, which you already\nproved, but you'll have to start with `symm at` your hypothesis.":
|
||||
"Qui è opportuno usare `add_right_eq_zero`, che hai già\ndimostrato, ma prima dovrai applicare `symm at` su un'ipotesi.",
|
||||
"You still don't know which way to go, so do `cases «{e}» with a`.":
|
||||
"Non sai ancora che direzione intraprendere, quindi esegui `cases «{e}» with a`.",
|
||||
"You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey.":
|
||||
"Ora conosci abbastanza tattiche per dimostrare `2 + 2 = 4`! Proseguiamo l'avventura.",
|
||||
"You might want to think about whether induction\non `a` or `b` is the best idea.":
|
||||
"Procedi per induzione: su cosa è meglio farla qua, su\n`a` o `b`?",
|
||||
"You can use `rw [zero_add] at «{h}»` to rewrite at `«{h}»` instead\nof at the goal.":
|
||||
"Puoi eseguire `rw [zero_add] at «{h}»` per sostituire all'interno dell'ipotesi `«{h}»` invece che\nnel goal.",
|
||||
"You can start a proof by induction on `n` by typing:\n`induction n with d hd`.":
|
||||
"Per avviare una dimostrazione per induzione su `n` digita:\n`induction n with d hd`.",
|
||||
"You can read more about the `decide` tactic by clicking\non it in the top right.":
|
||||
"Puoi leggere di più sulla tattica `decide` cliccando\nsul suo nome in alto a destra.",
|
||||
"You can put a `←` in front of any theorem provided to `rw` to rewrite\nthe other way around. Look at the docs for `rw` for an explanation. Type `←` with `\\l`.":
|
||||
"Ricorda che mettendo `←` davanti a un teorema che passi a `rw` puoi\nsostituire nel senso opposto. Guarda la documentazione di `rw` per capire meglio il suo funzionamento.\n`←` si ottiene digitando `\\l`.",
|
||||
"You can prove $1\\times m=m$ in at least three ways.\nEither by induction, or by using `succ_mul`, or\nby using commutativity. Which do you think is quickest?":
|
||||
"Puoi dimostrare $1\\times m=m$ in almeno tre modi.\nO per induzione, o tramite `succ_mul`, oppure\nusando la commutatività. Qual è il modo più veloce secondo te?",
|
||||
"You can probably take it from here.": "Prova a proseguire da solo.",
|
||||
"You can now finish with `exact h`.":
|
||||
"Concludi la dimostrazione con `exact h`.",
|
||||
"You can now `apply mul_left_cancel at h`":
|
||||
"Ora puoi fare `apply mul_left_cancel at h`",
|
||||
"You can make your own tactics in Lean.\nThis code here\n```\nmacro \"simp_add\" : tactic => `(tactic|(\n simp only [add_assoc, add_left_comm, add_comm]))\n```\nwas used to create a new tactic `simp_add`, which runs\n`simp only [add_assoc, add_left_comm, add_comm]`.\nTry running `simp_add` to solve this level!":
|
||||
"Puoi creare le tue tattiche personalizzate su Lean.\nCon questo codice\n```\nmacro \"simp_add\" : tattica => `(tattica|(\n simp only [add_assoc, add_left_comm, add_comm]))\n```\nabbiamo creato la nuova tattica `simp_add`, che esegue\n`simp only [add_assoc, add_left_comm, add_comm]`.\nProva ad eseguire `simp_add` per risolvere questo livello!",
|
||||
"You can just mimic the previous proof to do this one -- or you can figure out a way\nof using it.":
|
||||
"Puoi imitare la dimostrazione precedente per risolvere questa qua -- oppure potresti cercare un\nmodo di applicarla.",
|
||||
"You can do induction on any of the three variables. Some choices\nare harder to push through than others. Can you do the inductive step in\n5 rewrites only?":
|
||||
"Puoi procedere per induzione su una qualsiasi delle tre variabili. Scegli bene, perché\ncon certe scelte la dimostrazione si aggroviglia più che con altre. Riesci a dimostrare il caso induttivo in\nsole cinque sostituzioni?",
|
||||
"Why did we not just define `succ n` to be `n + 1`? Because we have not\neven *defined* addition yet! We'll do that in the next level.":
|
||||
"Come mai non abbiamo definito `succ n` semplicemente come `n + 1`? Perché non abbiamo\nancora *definito* il concetto di addizione! Provvederemo nel prossimo livello.",
|
||||
"What do you think of this two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` doesn't just take hypotheses, it will eat any proof which exists\nin the system.":
|
||||
"Guarda il mio two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` non prende soltanto ipotesi, puoi passargli qualsiasi dimostrazione\ndefinita nel gioco.",
|
||||
"Well done! You now have enough tools to tackle the main boss of this level.":
|
||||
"Ottimo lavoro! Ora sei abbastanza pratico per affrontare il boss principale di questo mondo.",
|
||||
"Well done!": "Ottimo lavoro!",
|
||||
"Welcome to tutorial world! In this world we learn the basics\nof proving theorems. The boss level of this world\nis the theorem `2 + 2 = 4`.\n\nYou prove theorems by solving puzzles using tools called *tactics*.\nThe aim is to prove the theorem by applying tactics\nin the right order.\n\nLet's learn some basic tactics. Click on \"Start\" below\nto begin your quest.":
|
||||
"Benvenuto nel Mondo Tutorial! In questo mondo impareremo le basi\ndella dimostrazione formale. Il livello boss di questo mondo\nè il teorema `2 + 2 = 4`.\n\nDimostrare i teoremi consiste nel risolvere dei puzzle matematici utilizzando degli strumenti chiamati *tactics* (tattiche).\nPer dimostrare un teorema dovrai applicare le tattiche nell'ordine\ngiusto.\n\nImpariamo subito qualche tattica basilare. Premi sul pulsante \"Via\" qui sotto\nper cominciare l'avventura.",
|
||||
"Welcome to Addition World! In this world we'll learn the `induction` tactic.\nThis will enable us to defeat the boss level of this world, namely `x + y = y + x`.\n\nThe tactics `rw`, `rfl` and `induction` are the only tactics you'll need to\nbeat all the levels in Addition World, Multiplication World, and Power World.\nPower World contains the final boss of the game.\n\nThere are plenty more tactics in this game, but you'll only need to know them if you\nwant to explore the game further (for example if you decide to 100%\nthe game).":
|
||||
"Benvenuto nel Mondo Addizione! In questo mondo impareremo la tattica `induction`,\nche ci permetterà di sconfiggere il boss di questo mondo, il teorema `x + y = y + x`.\n\nLe tattiche `rw`, `rfl` e `induction` sono le uniche tattiche di cui avrai bisogno per\nper battere tutti i livelli del Mondo Addizione, del Mondo Moltiplicazione e del Mondo Potenza.\nIl Mondo Potenza contiene il boss finale del gioco.\n\nCi sono tante altre tattiche in questo gioco, ma ne avrai bisogno solo se\ndesideri immergerti ulteriormente nel gioco (o hai intenzione di completarlo al 100%).",
|
||||
"We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.\nNow we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`.":
|
||||
"Abbiamo già visto `le_zero`, la prova di `x ≤ 0` implica `x = 0`.\nAdesso dimostreremo che `x ≤ 1` implica `x = 0` o `x = 1`.",
|
||||
"We've proved that `x ≤ 0` implies `x = 0`. The last two levels\nin this world will prove which numbers are `≤ 1` and `≤ 2`.\nThis lemma will be helpful for them.":
|
||||
"Abbiamo dimostrato che `x ≤ 0` implica `x = 0`. Gli ultimi due livelli\ndi questo mondo ci mostreranno quali sono i numeri `≤ 1` e `≤ 2`.\nQuesto lemma è propedeutico alle loro dimostrazioni.",
|
||||
"We've proved that $2+2=4$; in Implication World we'll learn\nhow to prove $2+2\\neq 5$.\n\nIn Addition World we proved *equalities* like $x + y = y + x$.\nIn this second tutorial world we'll learn some new tactics,\nenabling us to prove *implications*\nlike $x+1=4 \\implies x=3.$\n\nWe'll also learn two new fundamental facts about\nnatural numbers, which Peano introduced as axioms.\n\nClick on \"Start\" to proceed.":
|
||||
"Abbiamo dimostrato $2+2=4$; nel Mondo Implicazione vedremo\ncome dimostrare $2+2\\neq 5$.\n\nNel Mondo Addizione abbiamo dimostrato *uguaglianze* del tipo $x + y = y + x$.\nIn questo mondo apprenderai le tattiche\nche ci permettono di dimostrare le *implicazioni*\ncome $x+1=4 \\implies x=3.$\n\nImparerai inoltre due nuovi fatti fondamentali sui\nnumeri naturali, che Peano postulò come assiomi.\n\nPremi su \"Via\" per iniziare.",
|
||||
"We've just seen that `0 ^ 0 = 1`, but if `n`\nis a successor, then `0 ^ n = 0`. We prove that here.":
|
||||
"Abbiamo appena visto che `0 ^ 0 = 1`, ma se l'esponente `n`\nè un successore, allora `0 ^ n = 0`. Lo dimostriamo in questo livello.",
|
||||
"We've been adding up two numbers; in this level we will add up three.\n\n What does $x+y+z$ *mean*? It could either mean $(x+y)+z$, or it\n could mean $x+(y+z)$. In Lean, $x+y+z$ means $(x+y)+z$.\n\n But why do we care which one it means; $(x+y)+z$ and $x+(y+z)$ are *equal*!\n\n That's true, but we didn't prove it yet. Let's prove it now by induction.":
|
||||
"Finora abbiamo sommato solo due numeri alla volta; in questo livello ne sommeremo tre.\n\n Ma per cosa sta $x+y+z$ *esattamente*? Può stare per $(x+y)+z$, oppure può stare\n per $x+(y+z)$. In Lean, $x+y+z$ sta per $(x+y)+z$.\n\n La posizione delle parentesi potrebbe sembrarti irrilevante; d'altronde $(x+y)+z$ e $x+(y+z)$ sono *uguali*!\n\n Hai ragione, ma non l'abbiamo ancora dimostrato. Dimostriamolo subito tramite induzione.",
|
||||
"We're going to change that `False` into `True`. Start by changing it into\n`is_zero (succ a)` by executing `rw [← is_zero_succ a]`.":
|
||||
"Vogliamo trasformare quel `False` in un `True`. Inizia a trasformarlo in\n`is_zero (succ a)` eseguendo `rw [← is_zero_succ a]`.",
|
||||
"We'll need this lemma to prove that two is prime!\n\nYou'll need to know that `∨` is right associative. This means that\n`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`.\nThis affects how `left` and `right` work.":
|
||||
"Questo lemma ci aiuterà a dimostrare che due è un numero primo!\n\nQui ti serve sapere che `∨` associa a destra. Significa che\n`x = 0 ∨ x = 1 ∨ x = 2` sta in realtà per `x = 0 ∨ (x = 1 ∨ x = 2)`.\nL'associatività influisce sul comportamento di `left` e `right`.",
|
||||
"We'd like to prove `2 + 2 = 4` but right now\nwe can't even *state* it\nbecause we haven't yet defined addition.\n\n## Defining addition.\n\nHow are we going to add $37$ to an arbitrary number $x$? Well,\nthere are only two ways to make numbers in this game: $0$\nand successors. So to define `37 + x` we will need\nto know what `37 + 0` is and what `37 + succ x` is.\nLet's start with adding `0`.\n\n### Adding 0\n\nTo make addition agree with our intuition, we should *define* `37 + 0`\nto be `37`. More generally, we should define `a + 0` to be `a` for\nany number `a`. The name of this proof in Lean is `add_zero a`.\nFor example `add_zero 37` is a proof of `37 + 0 = 37`,\n`add_zero x` is a proof of `x + 0 = x`, and `add_zero` is a proof\nof `? + 0 = ?`.\n\nWe write `add_zero x : x + 0 = x`, so `proof : statement`.":
|
||||
"Il nostro obiettivo è dimostrare `2 + 2 = 4`, ma per ora non\npossiamo nemmeno *enunciarlo*\ndato che non abbiamo ancora definito l'addizione.\n\n## Definiamo l'addizione\n\nCome possiamo sommare $37$ a un numero arbitrario $x$? Beh,\nquesto numero arbitrario può essere stato creato in due modi: o $0$\no il successore. Dunque per definire `37 + x` abbiamo bisogno\ndi sapere quanto fa `37 + 0` e quanto fa `37 + succ x`.\nPartiamo dall'aggiungere `0` a qualcosa.\n\n### Aggiungere zero\n\nPer far sì che l'addizione rispetti la nostra intuizione, *definiamo* `37 + 0`\ncome `37`. In generale, definiamo `a + 0` uguale ad `a` per\nqualsiasi numero `a`. Questa dimostrazione in Lean si chiama `add_zero a`.\nAd esempio `add_zero 37` è la dimostrazione di `37 + 0 = 37`,\n`add_zero x` è la dimostrazione di `x + 0 = x`, `add_zero` da solo è la dimostrazione\ndi `? + 0 = ?`.\n\nLa sintassi è `add_zero x : x + 0 = x`, dunque `dimostrazione : enunciato`.",
|
||||
"We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0`\nwhich we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\\ne`).\nYou'll be asked to\nprove it, and then you'll have a new hypothesis which you can apply\n`le_mul_right` to.":
|
||||
"Il piano è applicare `le_mul_right`, ma per farlo abbiamo bisogno dell'ipotesi `x * y ≠ 0`\nche non è presente tra le ipotesi, per ora. Esegui `have h2 : x * y ≠ 0` (digita `≠` tramite `\\ne`).\nLean ti chiederà di\ndimostrarlo, e dopo avrai un'ipotesi nuova di zecca a cui puoi applicare\n`le_mul_right`.",
|
||||
"We want to reduce this to a hypothesis `b = 0` and a goal `a * b = 0`,\nwhich is logically equivalent but much easier to prove. Remember that `X ≠ 0`\nis notation for `X = 0 → False`. Click on `Show more help!` if you need hints.":
|
||||
"Vogliamo ridurre questo teorema a un'ipotesi `b = 0` e a un goal `a * b = 0`,\nche insieme sono logicamente equivalenti all'originale ma più facili da dimostrare. Ricorda che `X ≠ 0`\nè zucchero sintattico per `X = 0 → False`. Clicca su `Aiutami!` se hai bisogno di un indizio.",
|
||||
"We still can't prove `2 + 2 ≠ 5` because we have not talked about the\ndefinition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.\nHere `False` is a generic false proposition, and `→` is Lean's notation\nfor \"implies\". In logic we learn\nthat `True → False` is false, but `False → False` is true. Hence\n`X → False` is the logical opposite of `X`.\n\nEven though `a ≠ b` does not look like an implication,\nyou should treat it as an implication. The next two levels will show you how.\n\n`False` is a goal which you cannot deduce from a consistent set of assumptions!\nSo if your goal is `False` then you had better hope that your hypotheses\nare contradictory, which they are in this level.":
|
||||
"Non possiamo ancora dimostrare `2 + 2 ≠ 5` perché non abbiamo ancora dato la\ndefinizione dell'operatore `≠`. In Lean, `a ≠ b` è *notazione* per `a = b → False`.\n`False` è la proposizione falsa più banale, e `→` è la notazione di Lean\nper l'operatore \"implica\". Dalla tabella della verità dell'implicazione sappiamo\nche `True → False` è falso, mentre `False → False` è vero. Quindi\n`X → False` equivale alla negazione logica di `X`.\n\nNon si è abituati a vedere `a ≠ b` come un'implicazione, ma\nin Lean è comodo trattarla come tale. I prossimi due livelli ti faranno vedere come.\n\n`False` è un goal insoddisfacibile, impossibile da dedurre da un insieme consistente di ipotesi!\nQuindi se ti capita `False` come goal, puoi solo sperare di avere una contraddizione tra le\ntue ipotesi, come accade in questo livello.",
|
||||
"We now start work on an algorithm to do addition more efficiently. Recall that\nwe defined addition by recursion, saying what it did on `0` and successors.\nIt is an axiom of Lean that recursion is a valid\nway to define functions from types such as the naturals.\n\nLet's define a new function `pred` from the naturals to the naturals, which\nattempts to subtract 1 from the input. The definition is this:\n\n```\npred 0 := 37\npred (succ n) := n\n```\n\nWe cannot subtract one from 0, so we just return a junk value. As well as this\ndefinition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\nLet's use this lemma to prove `succ_inj`, the theorem which\nPeano assumed as an axiom and which we have already used extensively without justification.":
|
||||
"Ora svilupperemo un algoritmo che ci permette di svolgere le addizioni in maniera più efficiente. Se ricordi,\nabbiamo definito l'addizione tramite la ricorsione, definendo il suo comportamento su `0` e sul successore.\nUno degli assiomi di Lean dice proprio che la ricorsione è un metodo valido\nper definire funzioni su tipi di dato induttivi, come i numeri naturali.\n\nDefiniamo una nuova funzione `pred` dai naturali ai naturali, che\ntenta di sottrarre 1 dall'input. La definizione è la seguente:\n\n```\npred 0 := 37\npred (succ n) := n\n```\n\nNon potendo sottrarre uno da 0, in tal caso restituiamo un valore spazzatura. In aggiunta a questa\ndefinizione, creiamo un nuovo lemma `pred_succ` che dice `pred (succ n) = n`.\nUsiamo subito questo lemma per dimostrare `succ_inj`, il teorema che\nPeano postulò come assioma e che abbiamo usato estensivamente finora senza mai motivarlo.",
|
||||
"We now have enough to state a mathematically accurate, but slightly\nclunky, version of Fermat's Last Theorem.\n\nFermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\\not =z^m$.\nIf you didn't do inequality world yet then we can't talk about $m \\geq 3$,\nso we have to resort to the hack of using `n + 3` for `m`,\nwhich guarantees it's big enough. Similarly instead of `x > 0` we\nuse `a + 1`.\n\nThis level looks superficially like other levels we have seen,\nbut the shortest solution known to humans would translate into\nmany millions of lines of Lean code. The author of this game,\nKevin Buzzard, is working on translating the proof by Wiles\nand Taylor into Lean, although this task will take many years.\n\n## CONGRATULATIONS!\n\nYou've finished the main quest of the natural number game!\nIf you would like to learn more about how to use Lean to\nprove theorems in mathematics, then take a look\nat [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\nan interactive textbook which you can read in your browser,\nand which explains how to work with many more mathematical concepts in Lean.":
|
||||
"Ora abbiamo abbastanza materiale per asserire una versione matematicamente accurata, tuttavia un po' goffa, dell'Ultimo Teorema di Fermat.\n\nL'Ultimo Teorema di Fermat afferma che se $x,y,z>0$ e $m \\geq 3$ allora $x^m+y^m\\not =z^m$.\nSe non sei ancora stato nel Mondo Disequazioni, non possiamo parlare ancora di $m \\geq 3$,\nquindi dobbiamo ricorrere all'espediente `n + 3` per `m`,\nche garantisce che sia abbastanza grande. Allo stesso modo, simuliamo `x > 0`\ntramite `a + 1`.\n\nA primo sguardo, questo livello assomiglia ad altri livelli che abbiamo visto,\nma in realtà è impossibile da dimostrare a mano. Purtroppo, la soluzione più breve nota all'uomo\ncorrisponde a milioni di righe di codice Lean. Questo boss imbattibile ti lascia tutti perplessi, ma\nnon perdiamoci d'animo! L'autore di questo gioco,\nKevin Buzzard, sta lavorando al traduzione della prova di Wiles e Taylor in Lean,\nnonostante sia un compito che richiederà parecchi anni.\n\n## CONGRATULAZIONI!\n\nHai completato la missione principale del Gioco dei Numeri Naturali!\nSe vuoi sapere di più su come si usa Lean per\ndimostrare i teoremi della matematica, ti indirizziamo a \n[Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\nun web book interattivo che puoi leggere dal tuo browser,\nche spiega come trattare tanti altri concetti matematici su Lean.",
|
||||
"We now have enough to prove that multiplication is associative,\nthe boss level of multiplication world. Good luck!":
|
||||
"Adesso abbiamo abbastanza informazioni per dimostrare che la moltiplicazione è associativa,\nil boss del Mondo Moltiplicazione. Avanti guerriero!",
|
||||
"We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\nif we have a hypothesis `succ n = 0`? It's the wrong way around!\n\nThe `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\nto `y ≠ x`. And `symm at h`\ndoes the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\nthe proof `zero_ne_one`; now try proving $1 \\neq 0$.":
|
||||
"Abbiamo visto che `zero_ne_succ n` è la dimostrazione di `0 = succ n → False` -- ma come possiamo applicarla\nall'ipotesi `succ n = 0`? È la stessa uguaglianza, solo con i due lati scambiati!\n\nLa tattica `symm` ci viene in soccorso: riscrive un goal `x = y` in `y = x`, e un goal `x ≠ y`\nin `y ≠ x`. `symm at h`\nè la versione che opera sull'ipotesi `h`. Abbiamo dimostrato poco fa $0 \\neq 1$ e chiamato\nla sua dimostrazione `zero_ne_one`; ora prova a dimostrare $1 \\neq 0$.",
|
||||
"We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\nin Lean. We do this with the `intro` tactic.":
|
||||
"Abbiamo visto come fare `apply` di teoremi e ipotesi\ndella forma `P → Q`. Ma come ci comportiamo se è il *goal* ad avere la forma `P → Q`?\nPer dimostrare questo tipo di goal, ci serve un modo per dire a Lean \"supponiamo `P` e deduciamo `Q`\".\nLo possiamo fare con la tattica `intro`.",
|
||||
"We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.":
|
||||
"La dimostrazione che abbiamo dato prima per `2 + 2 ≠ 5` non è stata molto elegante; danne una più carina.",
|
||||
"We don't know whether to go left or right yet. So start with `cases «{h}» with hx hy`.":
|
||||
"Non sappiamo ancora se andare a sinistra o a destra nel goal. Dunque lavoriamo sull'ipotesi, inizia con `cases «{h}» with hx hy`.",
|
||||
"We define a function `is_zero` thus:\n\n```\nis_zero 0 := True\nis_zero (succ n) := False\n```\n\nWe also create two lemmas, `is_zero_zero` and `is_zero_succ n`, saying that `is_zero 0 = True`\nand `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`, Peano's\nLast Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have\nthis opposite version too, which can be proved in the same way. Note: you can\ncheat here by using `zero_ne_succ` but the point of this world is to show\nyou how to *prove* results like that.\n\nIf you can turn your goal into `True`, then the `trivial` tactic will solve it.":
|
||||
"Definiamo la funzione `is_zero` così:\n\n```\nis_zero 0 := True\nis_zero (succ n) := False\n```\n\nE creiamo due lemmi associati, `is_zero_zero` e `is_zero_succ n`, che dicono che `is_zero 0 = True`\ne `is_zero (succ n) = False`. Usiamo questi due lemmi per dimostrare `succ_ne_zero`, l'ultimo assioma di\nPeano. Può sembrare ripetitivo perché abbiamo già `zero_ne_succ` nel nostro arsenale, ma è comodo avere anche\nla versione opposta, la cui dimostrazione è identica. Nota: ora potresti\nbarare usando `zero_ne_succ`, ma l'obiettivo di questo mondo\nè proprio insegnarti a *dimostrare* tali risultati.\n\nSe riesci a riscrivere il goal a `True`, potrai risolverlo con la tattica `trivial`.",
|
||||
"Very well done.\n\nA passing mathematician remarks that with you've just proved that `ℕ` is totally\nordered.\n\nThe final few levels in this world are much easier.":
|
||||
"Ben fatto.\n\nUn matematico di passaggio ti fa notare che hai appena dimostrato che `ℕ` è ordinato\ntotalmente.\n\nIl resto dei livelli di questo mondo sono tutti in discesa.",
|
||||
"Use the previous lemma with `apply eq_succ_of_ne_zero at ha`.":
|
||||
"Usa il lemma precedente con `apply eq_succ_of_ne_zero at ha`.",
|
||||
"Use `mul_eq_zero` and remember that `tauto` will solve a goal\nif there are hypotheses `a = 0` and `a ≠ 0`.":
|
||||
"Usa `mul_eq_zero` e ricorda che `tauto` risolve qualsiasi goal\nse hai le ipotesi contraddittorie `a = 0` e `a ≠ 0`.",
|
||||
"Use `add_succ`.": "Usa `add_succ`.",
|
||||
"Tutorial World": "Mondo Tutorial",
|
||||
"Try `rw [← one_eq_succ_zero]` to change `succ 0` into `1`.":
|
||||
"Scrivi `rw [← one_eq_succ_zero]` per trasformare `succ 0` in `1`.",
|
||||
"Try `rw [add_zero c]`.": "Esegui `rw [add_zero c]`.",
|
||||
"Try `cases «{hd}» with h1 h2`.": "Prova `cases «{hd}» with h1 h2`.",
|
||||
"Totality of `≤` is the boss level of this world, and it's coming up next. It says that\nif `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.\nBut we haven't talked about `or` at all. Here's a run-through.\n\n1) The notation for \"or\" is `∨`. You won't need to type it, but you can\ntype it with `\\or`.\n\n2) If you have an \"or\" statement in the *goal*, then two tactics made\nprogress: `left` and `right`. But don't choose a direction unless your\nhypotheses guarantee that it's the correct one.\n\n3) If you have an \"or\" statement as a *hypothesis* `h`, then\n`cases h with h1 h2` will create two goals, one where you went left,\nand the other where you went right.":
|
||||
"La totalità di `≤` è il livello boss di questo mondo, ed è il prossimo livello. Essa afferma che\nse `a` e `b` sono due numeri naturali allora `a ≤ b` or `b ≤ a`.\nMa non abbiamo mai parlato di `or` (o, oppure). In breve:\n\n1) La notazione per \"or\" è `∨`. Non avrai bisogno di digitarlo, ma puoi ottenere quel simbolo\ndigitando `\\or`.\n\n2) Se hai un enunciato \"or\" nel *goal*, due tattiche ti consentono di fare progresso:\n`left` e `right`. Ma non avere mai fretta di prendere una direzione o l'altra \nse le tue ipotesi non ti garantiscono che stai scegliendo la direzione giusta.\n\n3) Se hai un enunciato \"or\" come *ipotesi* `h`, allora\n`cases h with h1 h2` creerà due goal, in uno devi dimostrare il lato sinistro,\ne nel secondo devi dimostrare il lato destro.",
|
||||
"To solve this level, you need to `use` a number `c` such that `x = 0 + c`.":
|
||||
"Per risolvere questo livello, dovrai chiamare `use` su un numero `c` tale che `x = 0 + c`.",
|
||||
"Those of you interested in speedrunning the game may want to know\nthat `repeat rw [add_zero]` will do both rewrites at once.":
|
||||
"Se sei interessato a fare lo speedrun del gioco, sappi\nche `repeat rw [add_zero]` esegue entrambe le sostituzioni in un'unica mossa.",
|
||||
"This world introduces exponentiation. If you want to define `37 ^ n`\nthen, as always, you will need to know what `37 ^ 0` is, and\nwhat `37 ^ (succ d)` is, given only `37 ^ d`.\n\nYou can probably guess the names of the general theorems:\n\n * `pow_zero (a : ℕ) : a ^ 0 = 1`\n * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n\nUsing only these, can you get past the final boss level?\n\nThe levels in this world were designed by Sian Carey, a UROP student\nat Imperial College London, funded by a Mary Lister McCammon Fellowship\nin the summer of 2019. Thanks to Sian and also thanks to Imperial\nCollege for funding her.":
|
||||
"Questo mondo è casa dell'elevamento a potenza. Come al solito, per definire `37 ^ n`,\ndobbiamo stabilire cosa significa `37 ^ 0`, e poi\ncosa significa `37 ^ (succ d)` data la conoscenza `37 ^ d`.\n\nQuesti due assiomi, il cui nome allude al nome dell'operazione in inglese (\"power\"), sono:\n\n * `pow_zero (a : ℕ) : a ^ 0 = 1`\n * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n\nRiuscirai a battere il livello boss usando solo questi due?\n\nQuesto mondo è stato progettato da Sian Carey, studente UROP\nal Imperial College London, finanziato dalla Mary Lister McCammon Fellowship\nnell'estate 2019. Grazie a Sian e grazie a Imperial\nCollege per averla sostenuta economicamente.",
|
||||
"This time, use the `left` tactic.":
|
||||
"Questa volta, puoi usare tattica `left`.",
|
||||
"This state is not provable! Did you maybe use `rw [add_left_eq_self] at h`\ninstead of `apply [add_left_eq_self] at h`? You can complare the two in the inventory.":
|
||||
"Questo stato non è dimostrabile! Per caso hai usato `rw [add_left_eq_self] at h`\nanziché `apply [add_left_eq_self] at h`? Puoi confrontare il loro effetto nell'inventario.",
|
||||
"This level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy\nis to write both `a` and `b` as `succ` of something, deduce that `a * b` is\nalso `succ` of something, and then `apply zero_ne_succ`.":
|
||||
"Questo livello dimostra che se `a ≠ 0` e `b ≠ 0` allora `a * b ≠ 0`. Una strategia vincente\nè riscrivere sia `a` che `b` come `succ` di qualcosa, dedurre che `a * b` è \nanche lui `succ` di qualcosa, e infine fare `apply zero_ne_succ`.",
|
||||
"This level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is\nlogically equivalent to the last level, so there is a very short proof.":
|
||||
"Questo livello dimostra che se `a * b = 0` allora `a = 0` or `b = 0`. È\nlogicamente equivalente allo scorso livello, quindi puoi dare una dimostrazione veramente corta.",
|
||||
"This level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition\nWorld's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the\nlemma `le_one` from `≤` world.\n\nWe'll prove it using a new and very useful tactic called `have`.":
|
||||
"Questo livello dimostra `x * y = 1 → x = 1`, l'analogo moltiplicativo del lemma `x + y = 0 → x = 0`\nincontrato del Mondo Addizione Avanzata. La strategia è dimostrare prima che `x ≤ 1` e poi usare il\nlemma `le_one` del Mondo `≤`.\n\nLo dimostreremo con una nuova tattica assai utile, `have`.",
|
||||
"This level is more important than you think; it plays\na useful role when battling a big boss later on.":
|
||||
"Questo livello è più importante di quanto non sembri; giocherà\nun ruolo importante in uno dei boss successivi.",
|
||||
"This level asks you to prove *antisymmetry* of $\\leq$.\nIn other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.\nIt's the trickiest one so far. Good luck!":
|
||||
"Questo livello ti chiede di dimostrare la proprietà *antisimmetrica* di $\\leq$.\nIn formula, se $x \\leq y$ e $y \\leq x$ allora $x = y$.\nÈ forse la più complicata tra quelle affrontate finora. Buona fortuna!",
|
||||
"This lemma would have been easy if we had known that `x + y = y + x`. That theorem\n is called `add_comm` and it is *true*, but unfortunately its proof *uses* both\n `add_zero` and `zero_add`!\n\n Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`.":
|
||||
"Questo lemma sarebbe stato semplice se avessimo potuto usare `x + y = y + x`. Quel teorema\n si chiama `add_comm` e, sebbene sia *vero*, la sua dimostrazione *dipende* sia da\n `add_zero` che da `zero_add`!\n\n Proseguiamo la nostra avventura verso `add_comm`, la dimostrazione di `x + y = y + x`.",
|
||||
"This is I think the toughest level yet. Tips: if `a` is a number\nthen `cases a with b` will split into cases `a = 0` and `a = succ b`.\nAnd don't go left or right until your hypotheses guarantee that\nyou can prove the resulting goal!\n\nI've left hidden hints; if you need them, retry from the beginning\nand click on \"Show more help!\"":
|
||||
"Questo è a mio parere il livello più tosto. Due consigli: se `a` è un numero naturale\nallora `cases a with b` lo scomporrà nei casi `a = 0` e `a = succ b`.\nNon andare a sinistra o a destra fin quando le tue ipotesi non ti garantiscono che\npuoi dimostrare quel ramo!\n\nTi ho lasciato alcuni indizi nascosti; quando ne hai bisogno, riavvia il livello\ne clicca su \"Aiutami!\"",
|
||||
"The way to start this proof is `induction b with d hd generalizing c`.":
|
||||
"Il modo giusto di aprire questa dimostrazione è `induction b with d hd generalizing c`.",
|
||||
"The rfl tactic": "La tattica rfl",
|
||||
"The reason `«{x}» ≤ «{x}»` is because `«{x}» = «{x}» + 0`.\nSo you should start this proof with `use 0`.":
|
||||
"La ragione per cui `«{x}» ≤ «{x}»` è perché `«{x}» = «{x}» + 0`.\nDunque dovresti aprire la dimostrazione con `use 0`.",
|
||||
"The previous lemma can be used to prove this one.":
|
||||
"Il lemma precedente può essere usato per dimostrare questo.",
|
||||
"The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\nLet's prove one of these facts in this level, and the other in the next.\n\n## A new tactic: `cases`\n\nThe `cases` tactic will split an object or hypothesis up into the possible ways\nthat it could have been created.\n\nFor example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\nbut don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\nIn this situation you can use `cases b with d` instead. There are two ways to make\na number: it's either zero or a successor. So you will end up with two goals, one\nwith `b = 0` and one with `b = succ d`.\n\nAnother example: if you have a hypothesis `h : False` then you are done, because a false statement implies\nany statement. Here `cases h` will close the goal, because there are *no* ways to\nmake a proof of `False`! So you will end up with no goals, meaning you have proved everything.":
|
||||
"Il prossimo risultato di cui abbiamo bisogno per il Mondo `≤` è: se `a + b = 0` allora `a = 0` e `b = 0`.\nIn questo livello dimostriamo solo la prima parte della conclusione, la seconda nel livello successivo.\n\n## Nuova tattica: `cases`\n\nLa tattica `cases` scompone un oggetto o un'ipotesi in tutti i modi possibili\nin cui può essere stato creato.\n\nAd esempio, su un numero naturale a volte è sufficiente ragionare con i due casi `b = 0` e `b = succ d` separatamente,\ntralasciando l'ipotesi induttiva `hd` prodotta da `induction b with d hd`.\nIn questa situazione puoi usare `cases b with d`. Ci sono due modi per creare un numero:\ncome zero o come successore di qualcosa. `case` riprodurrà proprio queste due alternative, spezzando la dimostrazione in due sotto-goal, uno\ncon l'ipotesi `b = 0` e un'altro con l'ipotesi `b = succ d`.\n\nChiariamo con un altro esempio: se hai l'ipotesi `h : False` allora hai finito, perché un'affermazione falsa implica\nqualsiasi cosa. Qua `cases h` chiuderà la dimostrazione, perché *non* vi è alcun modo\ndi costruire una dimostrazione di `False`! Quindi rimarrai con zero sotto-goal da dimostrare, ossia hai dimostrato tutto.",
|
||||
"The music gets ever more dramatic, as we explore\nthe interplay between exponentiation and multiplication.\n\nIf you're having trouble exchanging the right `x * y`\nbecause `rw [mul_comm]` swaps the wrong multiplication,\nthen read the documentation of `rw` for tips on how to fix this.":
|
||||
"La musica si fa sempre più drammatica nel mentre che ci addentriamo\nnella relazione tra elevamento a potenza e prodotto.\n\nSe stai avendo difficoltà a scambiare il giusto `x * y`\nperché `rw [mul_comm]` sta operando su un prodotto diverso,\nleggi la documentazione di `rw` per ripassare come fare sostituzioni mirate.",
|
||||
"The music dies down. Is that it?\n\nCourse it isn't, you can\nclearly see that there are two worlds left.\n\nA passing mathematician says that mathematicians don't have a name\nfor the structure you just constructed. You feel cheated.\n\nSuddenly the music starts up again. This really is the final boss.":
|
||||
"La musica cessa di suonare. È finita?\n\nOvvio che no, come vedi\nci sono ancora due livelli da battere.\n\nIntanto, un matematico di passaggio ti svela che i matematici non hanno dato un nome\nalla struttura che hai appena costruito. Questa notizia ti lascia l'amaro in bocca.\n\nLa musica riparte improvvisamente. Ti lasci alle spalle il passato: lo scontro con il boss finale è vicino.",
|
||||
"The lemma proved in the final level of this world will be helpful\nin Divisibility World.":
|
||||
"Il lemma dimostrato nel livello finale di questo mondo ci sarà d'aiuto\nnel Mondo Divisibilità.",
|
||||
"The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\".\nYou can `apply` it `at` any hypothesis of the form `a * d = a * ?`.":
|
||||
"L'ipotesi induttiva `hd` è \"Per tutti i numeri naturali `c`, `a * d = a * c → d = c`\".\nPuoi sfruttarla con `apply` e `at` su un'ipotesi della forma `a * d = a * ?`.",
|
||||
"The goal in this level is one of our hypotheses. Solve the goal by executing `exact h1`.":
|
||||
"Il goal di questo livello è una delle nostre ipotesi. Risolvilo eseguendo `exact h1`.",
|
||||
"The first sub-boss of Multiplication World is `mul_comm x y : x * y = y * x`.\n\nWhen you've proved this theorem we will have \"spare\" proofs\nsuch as `zero_mul`, which is now easily deducible from `mul_zero`.\nBut we'll keep hold of these proofs anyway, because it's convenient\nto have exactly the right tool for a job.":
|
||||
"Il primo mini-boss del Mondo Moltiplicazione è `mul_comm x y : x * y = y * x`.\n\nUna volta dimostrata la commutatività della moltiplicazione certe dimostrazioni che abbiamo fatto diventano \"superflue\",\ncome `zero_mul`, il quale ora può essere dedotto facilmente da `mul_zero`.\nMa ce le teniamo care comunque, perché sono strumenti specializzati che\npossono rivelarsi sempre utili.",
|
||||
"The classical introduction game for Lean.":
|
||||
"Il classico gioco introduttivo per Lean.",
|
||||
"The `use` tactic": "La tattica `use`",
|
||||
"The `exact` tactic": "La tattica `exact`",
|
||||
"The `apply` tactic.": "La tattica `apply`.",
|
||||
"Start with induction on `n`.": "Inizia facendo induzione su `n`.",
|
||||
"Start with `rw [← pred_succ a]` and take it from there.":
|
||||
"Inizia con `rw [← pred_succ a]` e prosegui da solo.",
|
||||
"Start with `rw [two_eq_succ_one]` to begin to break `2` down into its definition.":
|
||||
"Inizia eseguendo `rw [two_eq_succ_one]` per sostituire `2` con la sua definizione.",
|
||||
"Start with `repeat rw [add_assoc]` to push all the brackets to the right.":
|
||||
"Inizia con `repeat rw [add_assoc]` per portare tutte le parentesi a destra.",
|
||||
"Start with `intro hb`.": "Inizia con `intro hb`.",
|
||||
"Start with `intro h`.": "Inizia con `intro h`.",
|
||||
"Start with `intro h` to assume the hypothesis.":
|
||||
"Inizia con `intro h` per supporre l'ipotesi.",
|
||||
"Start with `intro h` to assume the hypothesis and call its proof `h`.":
|
||||
"Comincia eseguendo `intro h` per introdurre l'ipotesi nel contesto e darle il nome `h`.",
|
||||
"Start with `intro h` (remembering that `X ≠ Y` is just notation\nfor `X = Y → False`).":
|
||||
"Parti con `intro h` (ricordandoti che `X ≠ Y` è notazione per\n`X = Y → False`).",
|
||||
"Start with `induction «{y}» with d hd`.":
|
||||
"Inizia con `induction «{y}» with d hd`.",
|
||||
"Start with `have h2 := mul_ne_zero a b`.":
|
||||
"Inizia con `have h2 := mul_ne_zero a b`.",
|
||||
"Start with `contrapose! h`, to change the goal into its\ncontrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`.":
|
||||
"Inizia con `contrapose! h`, che ti fa dimostrare la\ncontronominale del goal, cioè avrai tra le ipotesi la negazione del goal, `succ m = succ m`, e come nuovo goal avrai la negazione dell'ipotesi `h`, `m = n`.",
|
||||
"Start with `cases «{hxy}» with a ha`.":
|
||||
"Inizia con `cases «{hxy}» with a ha`.",
|
||||
"Start with `cases a with d` to do a case split on `a = 0` and `a = succ d`.":
|
||||
"Inizia con `cases a with d` per spezzare il numero nei casi `a = 0` e `a = succ d`.",
|
||||
"Start with `apply succ_inj` to apply `succ_inj` to the *goal*.":
|
||||
"Parti con `apply succ_inj` per applicare `succ_inj` *sul goal*.",
|
||||
"Start with `apply h2 at h1`. This will change `h1` to `y = 42`.":
|
||||
"Inizia con `apply h2 at h1`. Questo trasformerà `h1` in `y = 42`.",
|
||||
"Start with `apply eq_succ_of_ne_zero at ha` and `... at hb`":
|
||||
"Inizia con `apply eq_succ_of_ne_zero at ha` e `... at hb`",
|
||||
"Start by unravelling the `1`.": "Comincia espandendo `1`.",
|
||||
"Split into cases `c = 0` and `c = succ e` with `cases c with e`.":
|
||||
"Suddividi la dimostrazione nei casi `c = 0` e `c = succ e` con `cases c with e`.",
|
||||
"Solve this level in one line with `simp only [add_assoc, add_left_comm, add_comm]`":
|
||||
"Completa questo livello in un'unica riga con `simp only [add_assoc, add_left_comm, add_comm]`",
|
||||
"So that's the algorithm: now let's use automation to perform it\nautomatically.":
|
||||
"Questo è l'algoritmo: ora cerchiamo di automatizzarlo con\nl'automazione di Lean.",
|
||||
"Similarly we have `mul_succ`\nbut we're going to need `succ_mul` (guess what it says -- maybe you\nare getting the hang of Lean's naming conventions).\n\nThe last level from addition world might help you in this level.\nIf you can't remember what it is, you can go back to the\nhome screen by clicking the house icon and then taking a look.\nYou won't lose any progress.":
|
||||
"In modo simile, abbiamo `mul_succ` come assioma\ne vogliamo dimostrare `succ_mul` (puoi immaginarti cosa dice se hai già\nfamiliarizzato con le convenzioni di nomenclatura di Lean).\n\nL'ultimo livello del Mondo Addizione potrebbe aiutarti qui.\nPer ridargli un'occhiata, puoi tornare al menu principale cliccando sull'icona della casetta.\nNon perderai il progresso fatto in questo livello.",
|
||||
"See the new \"*\" tab in your lemmas, containing `mul_zero` and `mul_succ`.\nRight now these are the only facts we know about multiplication.\nLet's prove nine more.\n\nLet's start with a warm-up: no induction needed for this one,\nbecause we know `1` is a successor.":
|
||||
"Nell'inventario è comparso il nuovo tab \"*\", dove vedrai `mul_zero` e `mul_succ`.\nPer ora queste sono le uniche due proprietà della moltiplicazione che conosciamo.\nInsieme ne dimostreremo altre nove.\n\nCominciamo con un esercizio di riscaldamento: non hai bisogno dell'induzione qua,\nperché sappiamo che `1` è un successore.",
|
||||
"See if you can take it from here. Look at the new lemmas and tactic\navailable on the right.":
|
||||
"Lascio il resto a te. Sfrutta i nuovi lemmi e tattiche\ndisponibili nell'inventario a destra.",
|
||||
"Remember, `x ≠ y` is *notation* for `x = y → False`.":
|
||||
"Ricorda, `x ≠ y` è *zucchero sintattico* per `x = y → False`.",
|
||||
"Remember that when Lean writes `a + b + c`, it means `(a + b) + c`.\nIf you are not sure where the brackets are in an expression, just hover\nyour cursor over it and look at what gets highlighted. For example,\nhover over both `+` symbols on the left hand side of the goal and\nyou'll see where the invisible brackets are.":
|
||||
"Ricorda che, per pura brevità, Lean mostra `a + b + c` al posto di `(a + b) + c`.\nSe non sei sicuro di dove si trovino le parentesi in un'espressione, puoi spostare il\nmouse al di sopra e guardare cosa viene evidenziato. Ad esempio,\nse sposti il puntatore sopra entrambi i simboli `+` nel membro sinistro del goal\navrai un'idea di dove Lean ha messo le parentesi invisibili.",
|
||||
"Remember that `h2` is a proof of `x = y → False`. Try\n`apply`ing `h2` either `at h1` or directly to the goal.":
|
||||
"Ricorda che `h2` è la dimostrazione di `x = y → False`. Fai\nl'`apply` di `h2` con `at h1` o direttamente sul goal.",
|
||||
"Reduce to the previous lemma with `nth_rewrite 2 [← mul_one a] at h`":
|
||||
"Riduci al lemma precedente con `nth_rewrite 2 [← mul_one a] at h`",
|
||||
"Ready for the boss level of this world?":
|
||||
"Pronto per il livello boss di questo mondo?",
|
||||
"Proofs like $2+2=4$ and $a+b+c+d+e=e+d+c+b+a$ are very tedious to do by hand.\nIn Algorithm World we learn how to get the computer to do them for us.\n\nClick on \"Start\" to proceed.":
|
||||
"Dimostrazioni come quelle di $2+2=4$ e $a+b+c+d+e=e+d+c+b+a$ sono una tortura da fare a mano.\nNel Mondo Algoritmi vedremo come farle risolvere al computer al posto nostro.\n\nPremi su \"Via\" per cominciare.",
|
||||
"Precision rewriting": "Rewriting mirato",
|
||||
"Power World": "Mondo Potenza",
|
||||
"Our next goal is \"left and right distributivity\",\nmeaning $a(b+c)=ab+ac$ and $(b+c)a=ba+ca$. Rather than\nthese slightly pompous names, the name of the proofs\nin Lean are descriptive. Let's start with\n`mul_add a b c`, the proof of `a * (b + c) = a * b + a * c`.\nNote that the left hand side contains a multiplication\nand then an addition.":
|
||||
"Il nostro nuovo obiettivo è dimostrare la \"distributività sinistra e destra\",\nossia $a(b+c)=ab+ac$ e $(b+c)a=ba+ca$. Al posto di questo nome\nun po' tecnico e altisonante, le dimostrazioni di Lean\nhanno nomi descrittivi. Partiamo da\n`mul_add a b c`, la dimostrazione di `a * (b + c) = a * b + a * c`.\nNota che a sinistra dell'uguale abbiamo la moltiplicazione\ndi un'addizione.",
|
||||
"Our first challenge is `mul_comm x y : x * y = y * x`,\nand we want to prove it by induction. The zero\ncase will need `mul_zero` (which we have)\nand `zero_mul` (which we don't), so let's\nstart with this.":
|
||||
"La prima sfida è dimostrare `mul_comm x y : x * y = y * x`,\ne vogliamo farlo per induzione. Per dimostrare il caso\nbase utilizzeremo `mul_zero` (che abbiamo come assioma)\ne `zero_mul`, che non abbiamo ancora, dunque partiamo\nda quest'ultimo.",
|
||||
"One of the best named levels in the game, a savage `pow_pow`\nsub-boss appears as the music reaches a frenzy. What\nelse could there be to prove about powers after this?":
|
||||
"Con il suo nome degno di premio Oscar, il mini-boss `pow_pow`\nsalta nel ring e la musica si fa ancora più intensa. Cos'altro c'è da\ndimostrare sulle potenze dopo di lui?!",
|
||||
"On the set of natural numbers, addition is commutative.\nIn other words, if `a` and `b` are arbitrary natural numbers, then\n$a + b = b + a$.":
|
||||
"L'addizione è commutativa sull'insieme dei naturali.\nEquivalentemente, se `a` e `b` sono due numeri naturali qualsiasi, allora\n$a + b = b + a$.",
|
||||
"On the set of natural numbers, addition is associative.\nIn other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n$ (a + b) + c = a + (b + c). $":
|
||||
"Sull'insieme dei numeri naturali, l'addizione è associativa.\nOvvero, se $a, b$ sono $c$ due numeri naturali qualsiasi, si ha che\n$ (a + b) + c = a + (b + c). $",
|
||||
"Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add a b`\nis the proof that `(succ a) + b = succ (a + b)` for `a` and `b` numbers.\nThis result is what's standing in the way of `x + y = y + x`. Again\nwe have the problem that we are adding `b` to things, so we need\nto use induction to split into the cases where `b = 0` and `b` is a successor.":
|
||||
"Oh no! Lungo la strada per `add_comm`, salta fuori un `succ_add` selvatico. `succ_add a b`\nè la dimostrazione dell'enunciato `(succ a) + b = succ (a + b)` per due numeri `a` e `b` qualsiasi.\nQuesto risultato è ciò che ci manca per dimostrare `x + y = y + x`. E ancora una volta,\nabbiamo il problema di sommare una `b` generica a destra, dunque dobbiamo\nricorrere all'induzione per spezzare questa `b` nei casi in cui `b = 0` e `b` è un successore.",
|
||||
"Numbers": "Numeri",
|
||||
"Now you need to figure out which number to `use`. See if you can take it from here.":
|
||||
"Ora devi individuare il numero su cui applicare `use`. Fai un tentativo!",
|
||||
"Now you have two goals. Once you proved the first, you will jump to the second one.\nThis first goal is the base case $n = 0$.\n\nRecall that you can rewrite the proof of any lemma which is visible\nin your inventory, or of any assumption displayed above the goal,\nas long as it is of the form `X = Y`.":
|
||||
"Ora hai due goal. Appena dimostrerai il primo, ti verrà dato il secondo goal da dimostrare.\nQuesto primo goal rappresenta il caso base $n = 0$.\n\nRicorda che puoi riscrivere la dimostrazione di qualsiasi lemma che è visibile\nnell'inventario, o una qualsiasi ipotesi presente al di sopra del goal,\na patto che abbia la forma `X = Y`.",
|
||||
"Now you could finish with `rw [«{h}»]` then `rfl`, but `exact «{h}»`\ndoes it in one line.":
|
||||
"Adesso potresti chiudere con `rw [«{h}»]` e `rfl`, ma `exact «{h}»`\nfa lo stesso lavoro in una sola riga.",
|
||||
"Now you can `rw [add_succ]`": "Ora puoi eseguire `rw [add_succ]`",
|
||||
"Now you can `apply zero_ne_succ at h`.":
|
||||
"Ora puoi fare `apply zero_ne_succ at h`.",
|
||||
"Now you can `apply le_mul_right at h2`.":
|
||||
"Ora puoi eseguire `apply le_mul_right at h2`.",
|
||||
"Now we can prove the `or` statement by proving the statement on the right,\nso use the `right` tactic.":
|
||||
"Ora possiamo dimostrare il goal con `or` dimostrando la proposizione a destra,\nperciò usa `right`.",
|
||||
"Now use `rw [add_left_comm b c]` to switch `b` and `c` on the left\nhand side.":
|
||||
"Ora fai `rw [add_left_comm b c]` per scambiare `b` con `c` a sinistra\ndell'uguale.",
|
||||
"Now the goal can be deduced from `h2` by pure logic, so use the `tauto`\ntactic.":
|
||||
"Adesso il goal può essere dedotto da `h2` tramite pura logica, dunque usa la tattica\n`tauto`.",
|
||||
"Now take apart the existence statement with `cases ha with n hn`.":
|
||||
"Ora scomponi l'ipotesi esistenziale con `cases ha with n hn`.",
|
||||
"Now rewrite `succ_eq_add_one` backwards at `h`\nto get the right hand side.":
|
||||
"Adesso riscrivi `succ_eq_add_one` all'indietro all'interno di `h`\nper avere il suo membro destro.",
|
||||
"Now rewrite `four_eq_succ_three` backwards to make the goal\nequal to the hypothesis.":
|
||||
"Ora sostituisci `four_eq_succ_three` all'indietro per eguagliare il\ngoal all'ipotesi.",
|
||||
"Now let's `apply` our new theorem. Execute `apply succ_inj at h`\nto change `h` to a proof of `x = 3`.":
|
||||
"Ora facciamo l'`apply` del nuovo teorema. Esegui `apply succ_inj at h`\nper trasformare `h` in una dimostrazione di `x = 3`.",
|
||||
"Now for to the second goal. Here you have the induction hypothesis\n`«{hd}» : 0 + «{d}» = «{d}»`, and you need to prove that `0 + succ «{d}» = succ «{d}»`.":
|
||||
"Adesso viene il secondo goal. Qui hai l'ipotesi induttiva\n`«{hd}» : 0 + «{d}» = «{d}»`, e devi dimostrare che `0 + succ «{d}» = succ «{d}»`.",
|
||||
"Now finish using the `exact` tactic.":
|
||||
"Adesso chiudi la dimostrazione usando `exact`.",
|
||||
"Now finish the job with `rfl`.": "Concludi la dimostrazione con `rfl`.",
|
||||
"Now finish in one line.": "Ora concludi in una linea.",
|
||||
"Now change `1` to `succ 0` in `h`.": "Ora riscrivi `1` in `succ 0` in `h`.",
|
||||
"Now `«{ha}»` is a proof that `«{y}» = «{x}» + «{a}»`, and `hxy` has vanished. Similarly, you can destruct\n`«{hyz}»` into its parts with `cases «{hyz}» with b hb`.":
|
||||
"Ora `«{ha}»` è una dimostrazione di `«{y}» = «{x}» + «{a}»`, mentre `hxy` è scomparso. In modo simile, puoi scomporre\n`«{hyz}»` nelle sue varie parti tramite `cases «{hyz}» with b hb`.",
|
||||
"Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`.":
|
||||
"Ora con `rw [← two_eq_succ_one]` `succ 1` diventa `2`.",
|
||||
"Now `rw [h]` then `rfl` works, but `exact h` is quicker.":
|
||||
"Ora potresti usare `rw [h]` e `rfl` in successione, ma `exact h` è più elegante.",
|
||||
"Now `rw [h] at h2` so you can `apply le_one at hx`.":
|
||||
"Adesso `rw [h] at h2` così puoi fare `apply le_one at hx`.",
|
||||
"Now `rw [add_zero]` will change `c + 0` into `c`.":
|
||||
"Ora `rw [add_zero]` trasformerà `c + 0` in `c`.",
|
||||
"Now `rfl` will work.": "Adesso `rfl` funzionerà.",
|
||||
"Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\nchange `succ x = succ y`.":
|
||||
"Adesso puoi fare `repeat rw [← succ_eq_add_one] at h` per fare due sostituzioni in un colpo\ne avrai `succ x = succ y`.",
|
||||
"Now `exact h` finishes the job.": "Ora concludi con `exact h`.",
|
||||
"Now `cases «{h2}» with e he`.": "Ora `cases «{h2}» with e he`.",
|
||||
"Now `cases h2 with h0 h1` and deal with the two\ncases separately.":
|
||||
"Ora `cases h2 with h0 h1` e lavora sui due casi\nseparatamente.",
|
||||
"Now `apply succ_inj at h` to cancel the `succ`s.":
|
||||
"Ora esegui `apply succ_inj at h` per togliere i `succ`.",
|
||||
"Now `apply h` and you can probably take it from here.":
|
||||
"Ora fai `apply h` e credo che puoi proseguire da solo.",
|
||||
"Note: this lemma will be useful for the final boss!":
|
||||
"Nota: questo lemma sarà d'aiuto per il boss finale!",
|
||||
"Note that you can do `rw [two_eq_succ_one, one_eq_succ_zero]`\nand then `rfl` to solve this level in two lines.":
|
||||
"Puoi anche fare `rw [two_eq_succ_one, one_eq_succ_zero]`\ne poi `rfl` per risolvere questo livello in due sole righe.",
|
||||
"Note that `succ a + «{d}»` means `(succ a) + «{d}»`. Put your cursor\non any `succ` in the goal or assumptions to see what exactly it's eating.":
|
||||
"Attento che `succ a + «{d}»` sta per `(succ a) + «{d}»`. Sposta il mouse\nsopra `succ` o nel goal o nelle ipotesi per capire su cosa agisce esattamente.",
|
||||
"Nice! You've proved `succ_inj`!\nLet's now prove Peano's other axiom, that successors can't be $0$.":
|
||||
"Bene! Hai dimostrato `succ_inj`!\nOra dimostriamo l'altro assioma di Peano, ossia che un successore non può essere $0$.",
|
||||
"Nice!\n\nThe next step in the development of order theory is to develop\nthe theory of the interplay between `≤` and multiplication.\nIf you've already done Multiplication World, you're now ready for\nAdvanced Multiplication World. Click on \"Leave World\" to access it.":
|
||||
"Bene!\n\nIl passo successivo nello sviluppo della teoria degli ordini è sviluppare\nla teoria dell'interazione tra `≤` e la moltiplicazione.\nSe hai già fatto il Mondo Moltiplicazione, sei pronto per ascendere al\nMondo Moltiplicazione Avanzata. Clicca su \"Abbandona mondo\" per accedervi.",
|
||||
"Nice!": "Ottimo!",
|
||||
"Next turn `1` into `succ 0` with `rw [one_eq_succ_zero]`.":
|
||||
"Adesso rendi `1` in uno `succ 0` con `rw [one_eq_succ_zero]`.",
|
||||
"Natural Number Game": "Il Gioco dei Numeri Naturali",
|
||||
"My proof:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```":
|
||||
"La mia dimostrazione:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```",
|
||||
"Multiplication usually makes a number bigger, but multiplication by zero can make\nit smaller. Thus many lemmas about inequalities and multiplication need the\nhypothesis `a ≠ 0`. Here is a key lemma enables us to use this hypothesis.\nTo help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\non the right to see what it does.":
|
||||
"La moltiplicazione di norma fa crescere un numero, ma moltiplicare per zero lo rende\npiù piccolo, o meglio, lo azzera. Ecco perché gran parte dei teoremi che mischiano le disuguaglianze con la moltiplicazione hanno\nl'ipotesi `a ≠ 0`. Questo livello è un lemma chiave che ci permette di mettere a frutto questa ipotesi.\nPer aiutarci nella dimostrazione, possiamo usare la tattica `tauto`. Clicca sul nome della tattica\nsulla destra per una descrizione dettagliata su cosa fa.",
|
||||
"Multiplication is distributive over addition on the left.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$a(b + c) = ab + ac$.":
|
||||
"La moltiplicazione è distributiva a sinistra rispetto all'addizione.\nEquivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n$a(b + c) = ab + ac$.",
|
||||
"Multiplication is commutative.": "La moltiplicazione è commutativa.",
|
||||
"Multiplication is associative.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(ab)c = a(bc)$.":
|
||||
"La moltiplicazione è un'operazione associativa.\nEquivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n$(ab)c = a(bc)$.",
|
||||
"Multiplication distributes\nover addition on the left.\n\n`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`.":
|
||||
"La moltiplicazione si distribuisce\nsull'addizione a sinistra.\n\n`mul_add a b c` è la dimostrazione di `a * (b + c) = a * b + a * c`.",
|
||||
"Multiplication World": "Mondo Moltiplicazione",
|
||||
"Mathematicians sometimes debate what `0 ^ 0` is;\nthe answer depends, of course, on your definitions. In this\ngame, `0 ^ 0 = 1`. See if you can prove it.\n\nCheck out the *Pow* tab in your list of theorems\nto see the new proofs which are available.":
|
||||
"Cosa rappresenta `0 ^ 0` è oggetto di dibattito tra i matematici;\nla risposta dipende, ovviamente, dalle tue definizioni. In questo\ngioco, `0 ^ 0 = 1`. Prova a dimostrarlo.\n\nGuarda nel tab *^* nell'elenco di teoremi\nper vedere le nuove dimostrazioni disponibili.",
|
||||
"Mathematicians sometimes argue that `0 ^ 0 = 0` is also\na good convention. But it is not a good convention in this\ngame; all the later levels come out beautifully with the\nconvention that `0 ^ 0 = 1`.":
|
||||
"Certi matematici sostengono che `0 ^ 0 = 0` sia pure una\nconvenzione ragionevole. Tuttavia non va d'accordo con il modo in cui abbiamo strutturato\ni livelli successivi del gioco, e nell'intento di difendere la loro eleganza matematica\nrimaniamo fermi sulla convenzione `0 ^ 0 = 1`.",
|
||||
"Many people find `apply t at h` easy, but some find `apply t` confusing.\nIf you find it confusing, then just argue forwards.\n\nYou can read more about the `apply` tactic in its documentation, which you can view by\nclicking on the tactic in the list on the right.":
|
||||
"Molte persone trovano più facile ragionare in avanti con `apply t at h`, mentre ad alcuni ragionare all'indietro con `apply t` confonde le idee.\nSe confonde le idee anche a te, puoi sempre ragionare in avanti, i due metodi sono equivalenti.\n\nTrovi più informazioni sulla tattica `apply` nella sua documentazione, a cui puoi accedere\ncliccando sul suo nome nell'elenco di tattiche a destra.",
|
||||
"Let's warm up with an easy one, which works even if `t = 0`.":
|
||||
"Riscaldiamoci le dita con un teorema facile, che vale anche per `t = 0`.",
|
||||
"Let's see if you can use the tactics we've learnt to prove $x+1=y+1\\implies x=y$.\nTry this one by yourself; if you need help then click on \"Show more help!\".":
|
||||
"Mettiti alla prova applicando le tattiche che abbiamo appena visto per dimostrare $x+1=y+1\\implies x=y$.\nCerca di dimostrarlo da solo; se ti perdi e hai bisogno di una mano clicca su \"Aiutami!\".",
|
||||
"Let's now move on to a more efficient approach to questions\ninvolving numerals, such as `20 + 20 = 40`.":
|
||||
"Adesso vediamo un metodo più efficiente per risolvere i\nlemmi che contengono numeri, come `20 + 20 = 40`.",
|
||||
"Let's now make our own tactic to do this.":
|
||||
"Ora creiamo la nostra tattica per fare qualcosa di simile.",
|
||||
"Let's now learn about Peano's second axiom for addition, `add_succ`.":
|
||||
"Vediamo adesso il secondo assioma di Peano sull'addizione, `add_succ`.",
|
||||
"Let's now begin our approach to the final boss,\nby proving some more subtle facts about powers.":
|
||||
"Vediamo meglio come affrontare il boss finale,\ndimostrando altre proprietà insidiose delle potenze.",
|
||||
"Let's first get `h` into the form `succ x = succ 3` so we can\napply `succ_inj`. First execute `rw [four_eq_succ_three] at h`\nto change the 4 on the right hand side.":
|
||||
"Prima di tutto portiamo `h` alla forma `succ x = succ 3` in modo da poter applicare\n`succ_inj`. Esegui `rw [four_eq_succ_three] at h`\nper sostituire il 4 nel membro destro.",
|
||||
"Lean's simplifier, `simp`, is \"`rw` on steroids\". It will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\n\nThis level is not a level which you want to solve by hand.\nGet the simplifier to solve it for you.":
|
||||
"Il semplificatore Lean, `simp`, può essere considerato una versione dopata di `rw`. Esso riscriverà ogni lemma\ntaggato `simp` e ogni lemma passato dall'utente fin tanto c'è qualcosa da riscrivere, più che può.\n\nQuesto è un livello che non vorresti risolvere a mano.\nFai fare il lavoro sporco al semplificatore.",
|
||||
"It's all over! You have proved a theorem which has tripped up\nschoolkids for generations (some of them think $(a+b)^2=a^2+b^2$:\nthis is \"the freshman's dream\").\n\nHow many rewrites did you use? I can do it in 12.\n\nBut wait! This boss is stirring...and mutating into a second more powerful form!":
|
||||
"Hai vinto tutto! Hai dimostrato un teorema che ha tormentato\nintere generazioni di alunni (alcuni credono che $(a+b)^2=a^2+b^2$:\nil cosiddetto \"freshman's dream\").\n\nQuante sostituzioni hai fatto? Io ci sono riuscito in 12.\n\nIn guardia! Il boss si agita...si sta trasformando nella sua seconda forma ancora più letale!",
|
||||
"It's \"intuitively obvious\" that there are no numbers less than zero,\nbut to prove it you will need a result which you showed in advanced\naddition world.":
|
||||
"È \"intuitivamente ovvio\" che non esistono numeri naturali minori di zero,\nma per dimostrarlo dovrai ricorrere a un risultato che abbiamo dimostrato nel mondo\nAddizione Avanzata.",
|
||||
"Induction on `a` will not work here. You are still stuck with an `+ b`.\nI suggest you delete this line and try a different approach.":
|
||||
"Fare induzione su `a` non aiuta: rimarrai bloccato con `+ b`.\nCancella la linea e tenta un altro approccio.",
|
||||
"Induction on `a` or `b` -- it's all the same in this one.":
|
||||
"Induzione su `a` o su `b` -- vanno entrambe bene qua.",
|
||||
"Induction on `a` is the most troublesome, then `b`,\nand `c` is the easiest.":
|
||||
"L'induzione su `a` è la più faticosa, mentre su `b`,\no su `c` è più facile.",
|
||||
"In this world we'll learn how to prove theorems of the form $P\\implies Q$.\nIn other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\nTo do that we need to learn some more tactics.\n\nThe `exact` tactic can be used to close a goal which is exactly one of\nthe hypotheses. It takes the name of the hypothesis as argument: `exact h`.":
|
||||
"In questo mondo vedremo come dimostrare teoremi della forma $P\\implies Q$.\nIn altre parole, verificheremo frasi della forma \"se $P$ è vero, allora $Q$ è vero\".\nPer farlo abbiamo bisogno di qualche tattica in più nel nostro arsenale.\n\nLa tattica `exact` può essere usata per risolvere un goal che coincide con una\ndelle ipotesi. Prende come argomento il nome dell'ipotesi: `exact h`.",
|
||||
"In this world we define `a ≤ b` and prove standard facts\nabout it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"\n\nThe definition of `a ≤ b` is \"there exists a number `c`\nsuch that `b = a + c`. \" So we're going to have to learn\na tactic to prove \"exists\" theorems, and another one\nto use \"exists\" hypotheses.\n\nClick on \"Start\" to proceed.":
|
||||
"In questo mondo diamo la definizione `a ≤ b` e dimostreremo qualche fatto comune\nsulle diseguaglianze, come \"se ho `a ≤ b` e `b ≤ c`, allora `a ≤ c`\".\n\nLa definizione di `a ≤ b` è \"esiste un numero `c`\ntale che `b = a + c`\". Dunque avremo bisogno di imparare una\ntattica che dimostri i teoremi con \"esiste\", e un'altra tattica\nper utilizzare gli \"esiste\" nelle ipotesi.\n\nPremi su \"Via\" per procedere.",
|
||||
"In this world I will mostly leave you on your own.\n\n`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$.":
|
||||
"In questo mondo non parlerò troppo.\n\n`add_right_cancel a b n` è il teorema che afferma $a+n=b+n\\implies a=b$.",
|
||||
"In this level, we see inequalities as *hypotheses*. We have not seen this before.\nThe `cases` tactic can be used to take `hxy` apart.":
|
||||
"In questo livello, abbiamo delle disuguaglianze tra le *ipotesi*. Non abbiamo ancora visto questo caso.\nLa tattica `cases` può essere usata per scomporre l'ipotesi `hxy`.",
|
||||
"In this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n\nWait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\nThis is `zero_add`, which is different.\n\nThe difficulty with proving `0 + n = n` is that we do not have a *formula* for\n`0 + n` in general, we can only use `add_zero` and `add_succ` once\nwe know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n\nThe base case will require us to prove `0 + 0 = 0`, and the inductive step\nwill ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because\n`0` and successor are the only way to make numbers, this will cover all the cases.\n\nSee if you can do your first induction proof in Lean.\n\n(By the way, if you are still in the \"Editor mode\" from the last world, you can swap\nback to \"Typewriter mode\" by clicking the `>_` button in the top right.)":
|
||||
"In questo livello dimostreremo l'enunciato $0+n=n$, dove $n$ è un numero naturale incognito.\n\nMa come, non l'abbiamo già dimostrato? No! Abbiamo dimostrato $n+0=n$, che abbiamo chiamato `add_zero`.\nQuesto è `zero_add`, un teorema diverso.\n\nCiò che complica le cose nel dimostrare `0 + n = n` è che non abbiamo una *formula* per riscrivere\n`0 + n` in generale, possiamo solo applicare `add_zero` o `add_succ` una volta che sappiamo che\n`n` è `0` oppure un successore. La tattica `induction` spezza la dimostrazione in questi due casi.\n\nNel caso base dovremo dimostrare `0 + 0 = 0`, e nel caso induttivo dovremo dimostrare\nche se `0 + d = d` allora `0 + succ d = succ d`. Dato che\n`0` e il successore sono i due soli modi per costruire i numeri naturali, la dimostrazione coprirà tutti i casi possibili.\n\nOra prova a svolgere la tua prima dimostrazione per induzione su Lean.\n\n(Se sei ancora nella \"Modalità editor\" dallo scorso mondo, puoi rientrare nella\n\"Modalità interattiva\" cliccando sul pulsante `>_` in alto a destra.)",
|
||||
"In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\nseveral reasons. One of these is that\nwe need to introduce a new idea: we will need to understand the concept of\nmathematical induction a little better.\n\nStarting with `induction b with d hd` is too naive, because in the inductive step\nthe hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\nso the induction hypothesis does not apply!\n\nAssume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,\nbecause we now have the flexibility to change `c`.\"":
|
||||
"In questo livello dimostriamo se `a * b = a * c` e `a ≠ 0` allora `b = c`. È un pò complicato, per\ndiverse ragioni. Una di queste è che\nabbiamo bisogno di introdurre una nuova idea, approfondendo la nozione di\ninduzione matematica.\n\nSarebbe ingenuo partire con `induction b with d hd`, perché nel passo induttivo\nl'ipotesi è `a * d = a * c → d = c` ma quello che sappiamo è solo che `a * succ d = a * c`,\ndunque non possiamo applicare l'ipotesi ipotesi induttiva!\n\nSupponiamo di fissare la variabile `a ≠ 0`. Il vero enunciato che vogliamo dimostrare per induzione su `b` è\n\"per tutte le `c`, se `a * b = a * c` allora `b = c`\". Questo *può* essere dimostrato per induzione,\nperché abbiamo permesso alla `c` di variare.",
|
||||
"In this level the *goal* is $2y=2(x+7)$ but to help us we\nhave an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\nyour list of assumptions. Lean thinks of `h` as being a secret proof of the\nassumption, rather like `x` is a secret number.\n\nBefore we can use `rfl`, we have to \"substitute in for $y$\".\nWe do this in Lean by *rewriting* the proof `h`,\nusing the `rw` tactic.":
|
||||
"In questo livello il *goal* è $2y=2(x+7)$ e l'unica informazione che\npuò aiutarci a dimostrarlo è l'*ipotesi* `h` che dice $y = x + 7$. Verifica di avere `h` sotto la voce \"Ipotesi\".\nLean vede `h` come una dimostrazione segreta dell'ipotesi,\nun po' come il valore della variabile `x` è un'incognita.\n\nPrima di poter usare la tattica `rfl`, dobbiamo \"sostituire per la variabile $y$\".\nIn Lean possiamo *riscrivere* la dimostrazione `h`\nattraverso la tattica `rw`.",
|
||||
"In this level one of our hypotheses is an *implication*. We can use this\nhypothesis with the `apply` tactic.":
|
||||
"In questo livello una delle nostre ipotesi è un'*implicazione*. Possiamo usare\nquesta ipotesi con la tattica `apply`.",
|
||||
"In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\nlearning the basics about theorem proving in Lean.\n\nThis is a good first introduction to Lean!":
|
||||
"In questo gioco ricreerai l'insieme dei numeri naturali $\\mathbb{N}$ partendo dagli assiomi di Peano,\ne lungo il percorso imparerai le basi del *theorem proving* su Lean.\n\nQuesto gioco è un'ottima introduzione a Lean!",
|
||||
"In the next level, we'll do the same proof but backwards.":
|
||||
"Nel livello successivo, dimostreremo lo stesso enunciato, al contrario.",
|
||||
"In the last level, we manipulated the hypothesis `x + 1 = 4`\n until it became the goal `x = 3`. In this level we'll manipulate\n the goal until it becomes our hypothesis! In other words, we\n will \"argue backwards\". The `apply` tactic can do this too.\n Again I will walk you through this one (assuming you're in\n command line mode).":
|
||||
"Nell'ultimo livello abbiamo manipolato l'ipotesi `x + 1 = 4`\n per farla coincidere con il goal `x = 3`. In questo livello manipoleremo\n il goal per farlo combaciare con una delle ipotesi! Si puo dire che\n \"ragioneremo all'indietro\". È ancora la tattica `apply` che ce lo consente.\n Ti guiderò io anche in questa dimostrazione (assicurati di essere in modalità\n interattiva).",
|
||||
"In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\nfrom a false statement. The `tauto` tactic will close this goal.":
|
||||
"Nel \"caso base\" abbiamo un'ipotesi `ha : 0 ≠ 0`, e sappiamo che puoi dedurre qualsiasi cosa\nda una proposizione falsa. La tattica `tauto` chiuderà il goal.",
|
||||
"In some later worlds, we're going to see some much nastier levels,\nlike `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\nBrackets need to be moved around, and variables need to be swapped.\n\nIn this level, `(a + b) + (c + d) = ((a + c) + d) + b`,\nlet's forget about the brackets and just think about\nthe variable order.\nTo turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,\nand then swap `b` and `d`. But this is easier than you\nthink with `add_left_comm`.":
|
||||
"Nei mondi successivi ci sono livelli molto più brutti\ncome `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\nQui le parentesi vanno spostate, e le variabili vanno scambiate tra di loro.\n\nIn questo livello, `(a + b) + (c + d) = ((a + c) + d) + b`,\ndimentichiamoci delle parentesi e concentriamoci solamente\nsull'ordine delle variabili.\nPer portare `a+b+c+d` a `a+c+d+b` dobbiamo scambiare `b` con `c`,\ne poi scambiare `b` con `d`. Questo è più facile di quanto\npensi tramite `add_left_comm`.",
|
||||
"In order to use the tactic `rfl` you can enter it in the text box\nunder the goal and hit \"Execute\".":
|
||||
"Per utilizzare la tattica `rfl` digitala nella casella di testo\nsotto il goal e premi \"Esegui\".",
|
||||
"In Prime Number World we will be proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 ≠ 37 × 42.$\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using pretty much everything which we've proved in this world so far.":
|
||||
"Nel Mondo Numeri Primi dimostreremo che $2$ è primo.\nMa per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42.$\nLo faremo mostrando che ogni fattore di $2$ è al più $2$,\nche avremo gratis grazie a questo lemma. La dimostrazione che ho in mente io manipola l'ipotesi finché\nnon diventa il goal, usando praticamente tutto ciò che abbiamo dimostrato in questo mondo finora.",
|
||||
"In Advanced Addition World we will prove some basic\naddition facts such as $x+y=x\\implies y=0$. The theorems\nproved in this world will be used to build\na theory of inequalities in `≤` World.\n\nClick on \"Start\" to proceed.":
|
||||
"Nel Mondo Addizione Avanzata dimostreremo delle proprietà\nbasilari dell'addizione come $x+y=x\\implies y=0$. I teoremi\ndimostrati in questo mondo servono da mattoncini teorici con cui costruiremo\nla teoria delle disuguaglianze nel Mondo `≤`.\n\nPremi su \"Via\" per iniziare.",
|
||||
"Implication World": "Mondo Implicazione",
|
||||
"Implementing the algorithm for equality of naturals, and the proof that it is correct,\nlooks like this:\n\n```\ninstance instDecidableEq : DecidableEq ℕ\n| 0, 0 => isTrue <| by\n show 0 = 0\n rfl\n| succ m, 0 => isFalse <| by\n show succ m ≠ 0\n exact succ_ne_zero m\n| 0, succ n => isFalse <| by\n show 0 ≠ succ n\n exact zero_ne_succ n\n| succ m, succ n =>\n match instDecidableEq m n with\n | isTrue (h : m = n) => isTrue <| by\n show succ m = succ n\n rw [h]\n rfl\n | isFalse (h : m ≠ n) => isFalse <| by\n show succ m ≠ succ n\n exact succ_ne_succ m n h\n```\n\nThis Lean code is a formally verified algorithm for deciding equality\nbetween two naturals. I've typed it in already, behind the scenes.\nBecause the algorithm is formally verified to be correct, we can\nuse it in Lean proofs. You can run the algorithm with the `decide` tactic.":
|
||||
"L'implementazione dell'algoritmo di uguaglianza tra naturali, e la sua dimostrazione di correttezza,\nsomigliano a questo:\n\n```\ninstance instDecidableEq : DecidableEq ℕ\n| 0, 0 => isTrue <| by\n show 0 = 0\n rfl\n| succ m, 0 => isFalse <| by\n show succ m ≠ 0\n exact succ_ne_zero m\n| 0, succ n => isFalse <| by\n show 0 ≠ succ n\n exact zero_ne_succ n\n| succ m, succ n =>\n match instDecidableEq m n with\n | isTrue (h : m = n) => isTrue <| by\n show succ m = succ n\n rw [h]\n rfl\n | isFalse (h : m ≠ n) => isFalse <| by\n show succ m ≠ succ n\n exact succ_ne_succ m n h\n```\n\nQuesto codice Lean è un algoritmo formalmente verificato che risolve il problema decisionale dell'uguaglianza\ndi due numeri naturali. L'ho già inserito dietro le quinte nel gioco.\nDato che abbiamo prova formale della correttezza dell'algoritmo, possiamo\nimpiegarlo nelle dimostrazioni di Lean. Puoi eseguire l'algoritmo all'interno di una dimostrazione con la tattica `decide`.",
|
||||
"If you have completed Algorithm World then you can use the `contrapose!` tactic\nhere. If not then I'll talk you through a manual approach.":
|
||||
"Se hai già completato il Mondo Algoritmi puoi usare la tattica `contrapose!`\nqui. Altrimenti ti farò vedere un approccio manuale.",
|
||||
"If you `use` the wrong number, you get stuck with a goal you can't prove.\nWhat number will you `use` here?":
|
||||
"Se applichi `use` su un numero errato, rimarrai bloccato con un goal non dimostrabile.\nSu che numero applicherai `use` qui?",
|
||||
"If the goal is not *exactly* a hypothesis, we can sometimes\nuse rewrites to fix things up.":
|
||||
"Se il goal non coincide *esattamente* con una delle ipotesi, possiamo\nprovare a renderli uguali con qualche sostituzione.",
|
||||
"If `h` is a proof of `X = Y` then `rw [h]` will\nturn `X`s into `Y`s. But what if we want to\nturn `Y`s into `X`s? To tell the `rw` tactic\nwe want this, we use a left arrow `←`. Type\n`\\l` and then hit the space bar to get this arrow.\n\nLet's prove that $2$ is the number after the number\nafter $0$ again, this time by changing `succ (succ 0)`\ninto `2`.":
|
||||
"Se `h` è una prova di `X = Y` allora `rw [h]` riscriverà\nle `X` in `Y`. E se volessimo invece riscrive\nle `Y` in `X`? Per dire alla tattica `rw` che vogliamo\nriscrivere nell'altro verso, usiamo una freccetta a sinistra `←`. Per ottenere questa freccetta, digita\n`\\l` e premi la barra spaziatrice.\n\nDimostriamo che $2$ è il numero che viene dopo il numero che viene dopo\n$0$ di nuovo, però questa volta procediamo nel senso opposto, trasformando `succ (succ 0)`\nin `2`.",
|
||||
"If `a` and `b` are numbers, then `succ_inj a b` is a proof\nthat `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*\ntab for more information.\n\nPeano had this theorem as an axiom, but in Algorithm World\nwe will show how to prove it in Lean. Right now let's just assume it,\nand let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed\nby manipulating our hypothesis until it becomes the goal. I will\nwalk you through this level.":
|
||||
"Se `a` e `b` sono due numeri, allora `succ_inj a b` è una dimostrazione\nche `succ a = succ b` implica `a = b`. Clicca su questo teorema nel tab *Peano*\nper maggiori dettagli.\n\nPeano formulò questo teorema come assioma, ma nel Mondo Algoritmi\nvedremo come dimostrarlo su Lean. Per ora lo diamo per scontato,\ne lo usiamo per dimostrare $x+1=4 \\implies x=3$. Procederemo nuovamente\nmanipolando un'ipotesi ipotesi per farla coincidere con il goal. Ti seguirò\npasso per passo in questo livello.",
|
||||
"If $x=y$ and $x \\neq y$ then we can deduce a contradiction.":
|
||||
"Se $x=y$ e $x \\neq y$ allora possiamo dedurre una contraddizione.",
|
||||
"If $x=37$ or $y=42$, then $y=42$ or $x=37$.":
|
||||
"Se $x=37$ o $y=42$, allora $y=42$ o $x=37$.",
|
||||
"If $x=37$ and we know that $x=37\\implies y=42$ then we can deduce $y=42$.":
|
||||
"Se $x=37$ e abbiamo che $x=37\\implies y=42$ allora possiamo dedurre $y=42$.",
|
||||
"If $x+1=4$ then $x=3$.": "Se $x+1=4$ allora $x=3$.",
|
||||
"If $x$ is a number, then $x \\le x$.":
|
||||
"Se $x$ è un numero, allora $x \\le x$.",
|
||||
"If $x$ is a number, then $x \\le \\operatorname{succ}(x)$.":
|
||||
"Sia $x$ un numero, allora $x \\le \\operatorname{succ}(x)$.",
|
||||
"If $x$ is a number, then $0 \\le x$.":
|
||||
"Se $x$ è un numero, allora $0 \\le x$.",
|
||||
"If $x$ and $y$ are numbers, then either $x \\leq y$ or $y \\leq x$.":
|
||||
"Se $x$ e $y$ sono numeri, allora vale $x \\leq y$ oppure $y \\leq x$.",
|
||||
"If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$.":
|
||||
"Se $x$ e $y$ sono numeri naturali, e $y = x + 7$, allora $2y = 2(x + 7)$.",
|
||||
"If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$":
|
||||
"Se $x$ e $q$ sono numeri naturali qualsiasi, allora $37x+q=37x+q.$",
|
||||
"If $x \\leq y$ and $y \\leq z$, then $x \\leq z$.":
|
||||
"Se $x \\leq y$ e $y \\leq z$, allora $x \\leq z$.",
|
||||
"If $x \\leq y$ and $y \\leq x$, then $x = y$.":
|
||||
"Se $x \\leq y$ e $y \\leq x$, allora $x = y$.",
|
||||
"If $x \\leq 2$ then $x = 0$ or $1$ or $2$.":
|
||||
"Se $x \\leq 2$ allora $x = 0$ o $1$ o $2$.",
|
||||
"If $x \\leq 1$ then either $x = 0$ or $x = 1$.":
|
||||
"Se $x \\leq 1$ allora vale $x = 0$ oppure $x = 1$.",
|
||||
"If $x \\leq 0$, then $x=0$.": "Se $x \\leq 0$, allora $x=0$.",
|
||||
"If $a, b,\\ldots h$ are arbitrary natural numbers, we have\n$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$.":
|
||||
"Se $a, b,\\ldots h$ sono numeri naturali qualsiasi, si ha che\n$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$.",
|
||||
"If $a, b, c$ are numbers, then $a+(b+c)=b+(a+c)$.":
|
||||
"Se $a, b, c$ sono dei numeri, allora $a+(b+c)=b+(a+c)$.",
|
||||
"If $a, b$, $c$ and $d$ are numbers, we have\n$(a + b) + (c + d) = ((a + c) + d) + b.$":
|
||||
"Se $a, b$, $c$ e $d$ sono numeri, si ha che\n$(a + b) + (c + d) = ((a + c) + d) + b.$",
|
||||
"If $a, b$ and $c$ are arbitrary natural numbers, we have\n$(a + b) + c = (a + c) + b$.":
|
||||
"Se $a, b$ e $c$ sono numeri naturali qualsiasi, si ha che\n$(a + b) + c = (a + c) + b$.",
|
||||
"If $a+b=0$ then $b=0$.": "Se $a+b=0$ allora $b=0$.",
|
||||
"If $a+b=0$ then $a=0$.": "Se $a+b=0$ allora $a=0$.",
|
||||
"If $a \\neq b$ then $\\operatorname{succ}(a) \\neq\\operatorname{succ}(b)$.":
|
||||
"Se $a \\neq b$ allora $\\operatorname{succ}(a) \\neq\\operatorname{succ}(b)$.",
|
||||
"If $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ then $x \\leq y$.":
|
||||
"Se $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ allora $x \\leq y$.",
|
||||
"If $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ then $a=b$.":
|
||||
"Se $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ allora $a=b$.",
|
||||
"How should we define `37 * x`? Just like addition, we need to give definitions\nwhen $x=0$ and when $x$ is a successor.\n\nThe zero case is easy: we define `37 * 0` to be `0`. Now say we know\n`37 * d`. What should `37 * succ d` be? Well, that's $(d+1)$ $37$s,\nso it should be `37 * d + 37`.\n\nHere are the definitions in Lean.\n\n * `mul_zero a : a * 0 = 0`\n * `mul_succ a d : a * succ d = a * d + a`\n\nIn this world, we must not only prove facts about multiplication like `a * b = b * a`,\nwe must also prove facts about how multiplication interacts with addition, like `a * (b + c) = a * b + a * c`.\nLet's get started.":
|
||||
"Come si può definire `37 * x`? Come per l'addizione, dobbiamo dare la definizione per\nquando $x=0$ e quando $x$ è un successore.\n\nIl caso di zero è facile: definiamo `37 * 0` uguale a `0`. Ora, immaginiamo di sapere quanto fa\n`37 * d`. Quanto fa allora `37 * succ d`? Beh, non è altro che $37$ sommato a se stesso $(d+1)$ volte,\nquindi `37 * d + 37`.\n\nEcco le due definizioni in Lean.\n\n * `mul_zero a : a * 0 = 0`\n * `mul_succ a d : a * succ d = a * d + a`\n\nIn questo mondo non ci limiteremo a dimostrare fatti riguardanti solo la moltiplicazione come `a * b = b * a`,\nma anche fatti su come la moltiplicazione interagisce con l'addizione, come `a * (b + c) = a * b + a * c`.\nIniziamo!",
|
||||
"How about this for a proof:\n```\nrepeat rw [add_comm n]\nexact add_right_cancel a b n\n```":
|
||||
"Cosa ne pensi di questa dimostrazione:\n```\nrepeat rw [add_comm n]\nexact add_right_cancel a b n\n```",
|
||||
"How about this for a proof:\n\n```\nrw [add_comm]\nexact add_right_eq_zero b a\n```\n\nThat's the end of Advanced Addition World! You'll need these theorems\nfor the next world, `≤` World. Click on \"Leave World\" to access it.":
|
||||
"Come ti sembra questa dimostrazione:\n\n```\nrw [add_comm]\nexact add_right_eq_zero b a\n```\n\nQuesto è tutto per il Mondo Addizione Avanzata! I teoremi di questo mondo ti torneranno utili\nnel prossimo mondo, il Mondo `≤`. Clicca su \"Abbandona mondo\" per navigarci.",
|
||||
"Here's what I was thinking of:\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```":
|
||||
"Ecco quello che avevo in mente:\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```",
|
||||
"Here's my solution:\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```":
|
||||
"Ecco come l'ho fatta io:\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```",
|
||||
"Here's my solution:\n```\nrw [mul_comm, mul_one]\nrfl\n```":
|
||||
"Ecco come l'ho fatta io:\n```\nrw [mul_comm, mul_one]\nrfl\n```",
|
||||
"Here's my solution:\n```\ninduction c with d hd\nrw [add_zero, mul_zero, add_zero]\nrfl\nrw [add_succ, mul_succ, hd, mul_succ, add_assoc]\nrfl\n```\n\nInducting on `a` or `b` also works, but might take longer.":
|
||||
"Ecco come l'ho fatta io:\n```\ninduction c with d hd\nrw [add_zero, mul_zero, add_zero]\nrfl\nrw [add_succ, mul_succ, hd, mul_succ, add_assoc]\nrfl\n```\n\nSi poteva risolvere anche per induzione su `a` or `b`, ma avrebbe richiesto più passi.",
|
||||
"Here's my proof:\n```\nrw [mul_comm, mul_add]\nrepeat rw [mul_comm c]\nrfl\n```":
|
||||
"Ecco la mia dimostrazione:\n```\nrw [mul_comm, mul_add]\nrepeat rw [mul_comm c]\nrfl\n```",
|
||||
"Here's my proof:\n```\nintro h\nrw [add_succ, add_succ, add_zero] at h\nrepeat apply succ_inj at h\napply zero_ne_succ at h\nexact h\n```\n\nEven though Lean is a theorem prover, right now it's pretty clear that we have not\ndeveloped enough material to make it an adequate calculator. In Algorithm\nWorld, a more computer-sciency world, we will develop machinery which makes\nquestions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.\nAlternatively you can do more mathematics in Advanced Addition World, where we prove\nthe lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\ndecide your route.":
|
||||
"Ecco la mia dimostrazione:\n```\nintro h\nrw [add_succ, add_succ, add_zero] at h\nrepeat apply succ_inj at h\napply zero_ne_succ at h\nexact h\n```\n\nLean è un theorem prover, ma non abbiamo ancora parlato del fatto che può anche fungere da linguaggio di programmazione. Nel Mondo Algoritmi,\nun mondo dal carattere più informatico, svilupperemo programmi per automatizzare le\ndimostrazioni, grazie ai quali potremo dimostrare $20 + 20 ≠ 41$ senza diventare matti.\nIn alternativa, puoi proseguire lungo il filo matematico nel Mondo Addizione Avanzata, dove dimostreremo\ni lemmi che supportano la teoria delle disuguaglianze. Clicca su \"Abbandona mondo\" e\nscegli la tua strada.",
|
||||
"Here's my proof:\n```\ncases x with y\nleft\nrfl\nrw [one_eq_succ_zero] at hx ⊢\napply succ_le_succ at hx\napply le_zero at hx\nrw [hx]\nright\nrfl\n```\n\nIf you solved this level then you should be fine with the next level!":
|
||||
"Ecco la mia dimostrazione:\n```\ncases x with y\nleft\nrfl\nrw [one_eq_succ_zero] at hx ⊢\napply succ_le_succ at hx\napply le_zero at hx\nrw [hx]\nright\nrfl\n```\n\nSe hai risolto questo livello allora puoi risolvere tranquillamente anche il successivo!",
|
||||
"Here's my proof:\n```\ncases hxy with a ha\ncases hyx with b hb\nrw [ha]\nrw [ha, add_assoc] at hb\nsymm at hb\napply add_right_eq_self at hb\napply add_right_eq_zero at hb\nrw [hb, add_zero]\nrfl\n```\n\nA passing mathematician remarks that with antisymmetry as well,\nyou have proved that `≤` is a *partial order* on `ℕ`.\n\nThe boss level of this world is to prove\nthat `≤` is a total order. Let's learn two more easy tactics\nfirst.":
|
||||
"Ecco la mia dimostrazione:\n```\ncases hxy with a ha\ncases hyx with b hb\nrw [ha]\nrw [ha, add_assoc] at hb\nsymm at hb\napply add_right_eq_self at hb\napply add_right_eq_zero at hb\nrw [hb, add_zero]\nrfl\n```\n\nUn matematico di passaggio ti fa notare che con l'aggiunta dell'antisimmetria,\nhai dimostrato che `≤` è un *ordine parziale* su `ℕ`.\n\nIl livello boss di questo mondo consiste nel dimostrare\nche `≤` è un ordine totale. Prima di affrontarlo vediamo altre due\ntattiche utili.",
|
||||
"Here's my proof:\n```\ncases hx with d hd\nuse d\nrw [succ_add] at hd\napply succ_inj at hd\nexact hd\n```":
|
||||
"Ecco la mia dimostrazione:\n```\ncases hx with d hd\nuse d\nrw [succ_add] at hd\napply succ_inj at hd\nexact hd\n```",
|
||||
"Here's a two-liner:\n```\nuse 1\nexact succ_eq_add_one x\n```\n\nThis works because `succ_eq_add_one x` is a proof of `succ x = x + 1`.":
|
||||
"Ecco una dimostrazione di due righe:\n```\nuse 1\nexact succ_eq_add_one x\n```\n\nQuesto funziona perché `succ_eq_add_one x` è la dimostrazione di `succ x = x + 1`.",
|
||||
"Here's a two-line proof:\n```\nrepeat rw [zero_add] at h\nexact h\n```":
|
||||
"Ecco una dimostrazione di due righe:\n```\nrepeat rw [zero_add] at h\nexact h\n```",
|
||||
"Here's a proof using `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\nand here's an even shorter one using the same idea:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nAlternatively you can just prove it by induction on `x`\n(the dots in the proof just indicate the two goals and\ncan be omitted):\n\n```\n induction x with d hd\n · intro h\n rw [zero_add] at h\n assumption\n · intro h\n rw [succ_add] at h\n apply succ_inj at h\n apply hd at h\n assumption\n```":
|
||||
"Ecco una dimostrazione che usa `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\ned eccone una più breve che condensa le ultime tre righe in una sola:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nVolendo puoi anche dimostrarlo per induzione su `x`\n(i pallini nel codice qui sotto hanno solo funzione decorativa,\nassieme all'indentazione servono per riconoscere più facilmente i due sottogoal, ma possono essere omessi):\n\n```\n induction x with d hd\n · intro h\n rw [zero_add] at h\n assumption\n · intro h\n rw [succ_add] at h\n apply succ_inj at h\n apply hd at h\n assumption\n```",
|
||||
"Here's a completely backwards proof:\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```":
|
||||
"Ecco una dimostrazione che procede all'indietro:\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```",
|
||||
"Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,\nso start with `cases b with d`.":
|
||||
"Qui vogliamo ragionare separatamente con i due casi `b = 0` e `b ≠ 0`,\nquindi parti con `cases b with d`.",
|
||||
"Here we begin to\ndevelop an algorithm which, given two naturals `a` and `b`, returns the answer\nto \"does `a = b`?\"\n\nHere is the algorithm. First note that `a` and `b` are numbers, and hence\nare either `0` or successors.\n\n*) If `a` and `b` are both `0`, return \"yes\".\n\n*) If one is `0` and the other is `succ n`, return \"no\".\n\n*) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"\n\nOur job now is to *prove* that this algorithm always gives the correct answer. The proof that\n`0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof\nthat `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then\n`succ m = succ n` is `rw [h]` and then `rfl`. This level is a proof of the one\nremaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`.":
|
||||
"Cominciamo lo sviluppo\ndi un algoritmo che, dati due naturali `a` e`b`, restituisce la risposta\nalla domanda \"does `a = b`?\"\n\nPresentiamo l'algoritmo. Nota prima che `a` e `b` sono entrambi numeri, e dunque\nsono `0` oppure dei successori.\n\n*) Se `a` e `b` sono entrambi `0`, restituiamo \"sì\".\n\n*) Se uno dei due è `0` e l'altro è `succ n`, restituiamo \"no\".\n\n*) Se `a = succ m` e `b = succ n`, restituiamo la risposta a \"`m = n`?\"\n\nNon ci rimane che *dimostrare* che questo algoritmo ci dà sempre la risposta corretta. Procediamo per casi. La dimostrazione di\n`0 = 0` è `rfl`. La dimostrazione di `0 ≠ succ n` è `zero_ne_succ n`, e la dimostrazione di\n`succ m ≠ 0` è `succ_ne_zero m`. La dimostrazione di \"se `h : m = n` allora\n`succ m = succ n`\" è `rw [h]` e infine `rfl`. Questo livello ci salva una parte di\nlavoro per dimostrare: se `a ≠ b` allora `succ a ≠ succ b`.",
|
||||
"Here is an example proof of 2+2=4 showing off various techniques.\n\n```lean\nnth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.\nrw [add_succ]\nrw [one_eq_succ_zero]\nrw [add_succ, add_zero] -- two rewrites at once\nrw [← three_eq_succ_two] -- change `succ 2` to `3`\nrw [← four_eq_succ_three]\nrfl\n```\n\nOptional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\non the `</>` button in the top right. You can now see your proof\nwritten as several lines of code. Move your cursor between lines to see\nthe goal state at any point. Now cut and paste your code elsewhere if you\nwant to save it, and paste the above proof in instead. Move your cursor\naround to investigate. When you've finished, click the `>_` button in the top right to\nmove back into \"Typewriter mode\".\n\nYou have finished tutorial world!\nClick \"Leave World\" to go back to the\noverworld, and select Addition World, where you will learn\nabout the `induction` tactic.":
|
||||
"Ecco un esempio di dimostrazione di 2+2=4 che impiega varie tecniche.\n\n```lean\nnth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.\nrw [add_succ]\nrw [one_eq_succ_zero]\nrw [add_succ, add_zero] -- two rewrites at once\nrw [← three_eq_succ_two] -- change `succ 2` to `3`\nrw [← four_eq_succ_three]\nrfl\n```\n\nEsercizio facoltativo: prova ad eseguire questa dimostrazione. Entra nella \"Modalità editor\" cliccando sul pulsante\n`</>` in alto a destra. Dovresti vedere la tua dimostrazione estesa su\ndiverse linee di codice. Muovendo il cursore da una linea all'altra vedrai\nlo stato della dimostrazione in ogni punto. Ora copia la tua dimostrazione e salvala da qualche parte per non\nperderla, e incolla la dimostrazione che abbiamo riportato qui sopra al posto del tuo codice. Muovi il cursore\ntra le linee per vedere come si comporta, sperimenta un po' con l'interfaccia. Quando hai finito, premi il pulsante `>_` in alto a destra per\nritornare nella \"Modalità interattiva\".\n\nHai completato il Mondo Tutorial!\nPremi \"Abbandona mondo\" per tornare al \nmenu principale, ed entra nel Mondo Addizione, dove imparerai a usare\nla tattica `induction`.",
|
||||
"Having to rearrange variables manually using commutativity and\nassociativity is very tedious. We start by reminding you of this. `add_left_comm`\nis a key component in the first algorithm which we'll explain, but we need\nto prove it manually.\n\nRemember that you can do precision commutativity rewriting\nwith things like `rw [add_comm b c]`. And remember that\n`a + b + c` means `(a + b) + c`.":
|
||||
"Ricollocare le variabili manualmente usando la commutatività e\nl'associatività è un lavoraccio. Ma possiamo fare di meglio. `add_left_comm`\nè un lemma chiave del primo algoritmo che spiegheremo, ma prima di impiegarlo dobbiamo\ndimostrarlo.\n\nRicorda che puoi applicare la commutatività precisando le \nvariabili che vuoi scambiare, scrivendo tipo `rw [add_comm b c]`. Ricorda anche che\n`a + b + c` sta per `(a + b) + c`.",
|
||||
"Good luck!\n\n One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.\n If you only want to change one of them, say the 3rd one, then use\n `nth_rewrite 3 [h]`.":
|
||||
"Buona fortuna!\n\n Un'ultima cosa. Se hai `h : X = Y`, con `rw [h]` cambierai *tutte* le `X` in`Y`.\n Se vuoi cambiarne solo una, la terza ad esempio, allora devi scrivere\n`nth_rewrite 3 [h]`.",
|
||||
"For any natural number $m$, we have $ m \\times 1 = m$.":
|
||||
"Per ogni numero naturale $m$, si ha che $ m \\times 1 = m$.",
|
||||
"For any natural number $m$, we have $ 2 \\times m = m+m$.":
|
||||
"Per ogni numero naturale $m$, si ha che $ 2 \\times m = m+m$.",
|
||||
"For any natural number $m$, we have $ 1 \\times m = m$.":
|
||||
"Per ogni numero naturale $m$, si ha che $ 1 \\times m = m$.",
|
||||
"For all numbers $m$, $0 ^{\\operatorname{succ} (m)} = 0$.":
|
||||
"Per tutti i numeri naturali $m$, $0 ^{\\operatorname{succ} (m)} = 0$.",
|
||||
"For all numbers $a$ and $b$, we have\n$$(a+b)^2=a^2+b^2+2ab.$$":
|
||||
"Per tutti i numeri naturali $a$ e $b$, si ha che\n$$(a+b)^2=a^2+b^2+2ab.$$",
|
||||
"For all naturals $m$, $1 ^ m = 1$.":
|
||||
"Per tutti i numeri naturali $m$, $1 ^ m = 1$.",
|
||||
"For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m a ^ n$.":
|
||||
"Per tutti i numeri naturali $a$, $m$, $n$, si ha che $a^{m + n} = a ^ m a ^ n$.",
|
||||
"For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$.":
|
||||
"Per tutti i numeri naturali $a$, $m$, $n$, si ha che $(a ^ m) ^ n = a ^ {mn}$.",
|
||||
"For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$.":
|
||||
"Per tutti i numeri naturali $a$, $b$, $n$, si ha che $(ab) ^ n = a ^ nb ^ n$.",
|
||||
"For all naturals $a$, $a ^ 2 = a \\times a$.":
|
||||
"Per tutti i numeri naturali $a$, $a ^ 2 = a \\times a$.",
|
||||
"For all naturals $a$, $a ^ 1 = a$.":
|
||||
"Per tutti i numeri naturali $a$, $a ^ 1 = a$.",
|
||||
"For all naturals $a$ $b$ $c$ and $n$, we have\n$$(a+1)^{n+3}+(b+1)^{n+3}\\not=(c+1)^{n+3}.$$":
|
||||
"Per tutti i numeri naturali $a$ $b$ $c$ e $n$, si ha che\n$$(a+1)^{n+3}+(b+1)^{n+3}\\not=(c+1)^{n+3}.$$",
|
||||
"For all natural numbers $n$, we have $0 + n = n$.":
|
||||
"Per ogni numero naturale $n$, si ha che $0 + n = n$.",
|
||||
"For all natural numbers $m$, we have $ 0 \\times m = 0$.":
|
||||
"Per tutti i numeri naturali $m$, si ha $ 0 \\times m = 0$.",
|
||||
"For all natural numbers $a, b$, we have\n$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$.":
|
||||
"Per tutti i numeri naturali $a, b$, si ha che\n$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$.",
|
||||
"For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$.":
|
||||
"Per ogni numero naturale $a$, si ha che $\\operatorname{succ}(a) = a+1$.",
|
||||
"For all natural numbers $a$ and $b$, we have\n$(\\operatorname{succ}\\ a) \\times b = a\\times b + b$.":
|
||||
"Per tutti i numeri naturali $a$ e $b$, si ha che\n$(\\operatorname{succ}\\ a) \\times b = a\\times b + b$.",
|
||||
"First execute `rw [h]` to replace the `y` with `x + 7`.":
|
||||
"Innanzitutto, esegui `rw [h]` per sostituire `y` con `x + 7`.",
|
||||
"Finally use a targetted `add_comm` to switch `b` and `d`":
|
||||
"Infine fai un rewrite mirato di `add_comm` per scambiare `b` con `d`",
|
||||
"Fermat's Last Theorem": "L'ultimo teorema di Fermat",
|
||||
"Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
|
||||
"Ogni numero in Lean è $0$ oppure il successore di un altro numero. Abbiamo già visto come aggiungere $0$,\ne ci rimane da capire come aggiungere un successore. Ipotizziamo di sapere\nche vale l'uguaglianza `37 + d = q`. A cosa dovrebbe essere uguale `37 + succ d`? Beh,\n`succ d` è un'unità più grande di `d`, quindi `37 + succ d` dovrebbe essere `succ q`,\nossia un'unità più grande di `q`. In generale `x + succ d` dovrebbe\ndare `succ (x + d)`. Formalizziamo questo ragionamento in un lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nQuando vedi `... + succ ...` nel goal, eseguire `rw [add_succ]` è una\nbuona idea.\n\nDimostriamo ora che `succ n = n + 1`. Cerca di introdurre un `+ succ` nel\ngoal, poi esegui `rw [add_succ]`. Controlla entrambi i tab `+` (addizione) e\n`012` (numeri) nella sezione \"Teoremi\" a destra\nper vedere quali teoremi da riscrivere hai a disposizione.",
|
||||
"Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
|
||||
"Ripeti lo stesso comando!\n\n`rw [zero_add] at «{h}»` ha completato automaticamente\nla chiamata a `zero_add` (trovando l'argomento `«{x}»`) e poi ha sostituito tutte le occorrenze di\n`0 + «{x}»` in un solo colpo. Dunque non ha toccato `0 + «{y}»` ancora, perciò dovresti ripetere il comando.",
|
||||
"Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
|
||||
"Per caso hai fatto induzione su `y`?\nEcco una dimostrazione in due righe `add_left_eq_self` che sfrutta `add_right_cancel`.\nSe vuoi vedere come funziona, vai in editor mode cliccando su `</>` in alto a destra,\ncopia e incolla la mia dimostrazione e muoviti tra le linee con il cursore\nper vedere le ipotesi e il goal in ogni punto\n(prima salva la tua dimostrazione però, altrimenti la perdi). Premi su `>_` per\ntornare alla modalità command line.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
|
||||
"Dealing with `or`": "Come ragionare con `or`",
|
||||
"Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World.":
|
||||
"Congratulazioni! Hai finito il Mondo Algoritmi. Questi algoritmi\nti saranno sicuramente utili per il Mondo Pari-Dispari.",
|
||||
"Congratulations! You have proved Fermat's Last Theorem!\n\nEither that, or you used magic...":
|
||||
"Congratulazioni! Hai dimostrato l'ultimo teorema di Fermat!\n\nO forse no... ti ho visto usare la polvere magica...",
|
||||
"Congratulations! You completed your first verified proof!\n\nRemember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,\nyou can click on `rfl` in the list of tactics on the right.\n\nNow click on \"Next\" to learn about the `rw` tactic.":
|
||||
"Congratulazioni! Hai completato la tua prima dimostrazione formale!\n\nRicorda che `rfl` è una *tattica*. Se vuoi sapere di più sulla tattica `rfl`,\nclicca su `rfl` nella lista di tattiche a destra.\n\nAdesso vedremo la tattica `rw`. Premi \"Avanti\".",
|
||||
"Concretely: `rw [← succ_eq_add_one] at h`.":
|
||||
"Sintassi concreta: `rw [← succ_eq_add_one] at h`.",
|
||||
"Can you take it from here? Click on \"Show more help!\" if you need a hint.":
|
||||
"Riesci a finire la dimostrazione da solo? Clicca su \"Aiutami!\" se hai bisogno di un indizio.",
|
||||
"Can you take it from here? (note: if you try `contrapose! h` again, it will\ntake you back to where you started!)":
|
||||
"Sai proseguire da solo? (nota: se rifai `contrapose! h` ritornerai\nallo stato originale della dimostrazione!)",
|
||||
"Can you take it from here?": "Sai proseguire da solo?",
|
||||
"Can you now change the goal into `2 = 2`?":
|
||||
"Puoi trasformare il goal in `2 = 2`?",
|
||||
"At this point you see the term `0 + «{d}»`, so you can use the\ninduction hypothesis with `rw [«{hd}»]`.":
|
||||
"A questo punto hai davanti il termine `0 + «{d}»`, quindi puoi riscrivere\nl'ipotesi induttiva con `rw [«{hd}»]`.",
|
||||
"Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$.":
|
||||
"Ipotizzando che $x+y=37$ e $3x+z=42$, si ha che $x+y=37$.",
|
||||
"Assuming $0+x=(0+y)+2$, we have $x=y+2$.":
|
||||
"Ipotizzando che $0+x=(0+y)+2$, si ha che $x=y+2$.",
|
||||
"As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to\nintroduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.\nTo learn about this result, click on it in the list of lemmas on the right.":
|
||||
"Come riscaldamento per il boss `2 + 2 ≠ 5` dimostriamo `0 ≠ 1`. A tal fine dobbiamo introdurre\nl'ultimo assioma di Peano, `zero_ne_succ n`, che dimostra che `0 ≠ succ n`.\nPer capire meglio questo risultato, puoi consultare la sua voce nella lista di lemmi a destra.",
|
||||
"Arguing backwards": "Ragionare all'indietro",
|
||||
"Applying a proof of $P\\implies Q$ to the *goal* changes $Q$ to $P$.\nNow try `rw [succ_eq_add_one]` to make the goal more like the hypothesis.":
|
||||
"Applicando $P\\implies Q$ al *goal* ci siamo mossi da $Q$ a $P$.\nOra esegui `rw [succ_eq_add_one]` per iniziare a portare il goal a una delle ipotesi.",
|
||||
"And now we've deduced what we wanted to prove: the goal is one of our assumptions.\nFinish the level with `exact h`.":
|
||||
"Abbiamo dedotto esattamente ciò che volevamo dimostrare: il goal coincide con una delle ipotesi.\nCompleta il livello con `exact h`.",
|
||||
"And now `rw [add_zero]`": "E ora `rw [add_zero]`",
|
||||
"And finally `rfl`.": "Infine, `rfl`.",
|
||||
"An algorithm for equality": "Un algoritmo per l'uguaglianza",
|
||||
"Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if\n$n$ is a successor.":
|
||||
"Sebbene definiamo $0^0=1$ in questo gioco, $0^n=0$ se $n>0$, ossia se\n$n$ è un successore.",
|
||||
"Algorithm World": "Mondo Algoritmi",
|
||||
"Advanced Multiplication World": "Mondo Moltiplicazione Avanzata",
|
||||
"Advanced Addition World": "Mondo Addizione Avanzata",
|
||||
"Advanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts about multiplication, such as `x * y = 1 → x = 1`, and\n`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.":
|
||||
"Nel Mondo *Addizione* Avanzata abbiamo dimostrato varie implicazioni\nsull'addizione, ad esempio `x + y = 0 → x = 0` e `x + y = x → y = 0`.\nIn seguito abbiamo usato questi lemmi per dimostrare fatti basilari su ≤ nel Mondo ≤.\n\nNel Mondo Moltiplicazione Avanzata dimostreremo dei fatti\nanaloghi sulla moltiplicazione, ad esempio `x * y = 1 → x = 1`, e\n`x * y = x → y = 1` (assumendo che `x ≠ 0` nel secondo enunciato). Questi saranno propedeutici\nper il Mondo Divisibilità.\n\nIl Mondo Moltiplicazione è più complesso del Mondo Addizione. Allo stesso modo,\nil Mondo Moltiplicazione Avanzata è più complesso del Mondo Addizione Avanzata.\nLa maggiore complessità di questo mondo è dovuta al fatto che certi teoremi valgono a condizione che una delle variabili non possa assumere il valore zero (sia non-nulla).\nQuesto ulteriore vincolo ha dei risvolti inaspettati.",
|
||||
"Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
|
||||
"L'addizione gode della proprietà distributiva sulla moltiplicazione.\nEquivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n$(a + b) \\times c = ac + bc$.",
|
||||
"Addition World": "Mondo Addizione",
|
||||
"Adding zero": "Sommare zero",
|
||||
"A two-line proof is\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nWe now have all the tools necessary to set up the basic theory of divisibility of naturals.":
|
||||
"Una dimostrazione di due righe è la seguente\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nOra abbiamo tutti gli strumenti necessari per costruire la teoria basilare della divisibilità dei numeri naturali.",
|
||||
"A proof that $a+b=0 \\implies b=0$.":
|
||||
"Una dimostrazione di $a+b=0 \\implies b=0$.",
|
||||
"A proof that $a+b=0 \\implies a=0$.":
|
||||
"Una dimostrazione di $a+b=0 \\implies a=0$.",
|
||||
"A passing mathematician remarks that with reflexivity and transitivity out of the way,\nyou have proved that `≤` is a *preorder* on `ℕ`.":
|
||||
"Un matematico di passaggio ti fa notare che avendo dimostrato le proprietà riflessiva e transitiva,\nhai dimostrato che `≤` è un *preordine* su `ℕ`.",
|
||||
"A passing mathematician notes that you've proved\nthat the natural numbers are a commutative semiring.\n\nIf you want to begin your journey to the final boss, head for Power World.":
|
||||
"Un matematico di passaggio nota che hai appena dimostrato\nche i numeri naturali sono un semianello commutativo.\n\nSe ti senti pronto per incamminarti verso il boss finale, dirigiti verso il Mondo Potenza.",
|
||||
"A passing mathematician congratulates you on proving that naturals\nare an additive commutative monoid.\n\nLet's practice using `add_assoc` and `add_comm` in one more level,\nbefore we leave addition world.":
|
||||
"Un matematico di passaggio si congratula con te per aver dimostrato che i naturali\nsono un monoide additivo commutativo.\n\nEsercitiamoci a usare `add_assoc` e `add_comm` in un ultimo livello,\nprima di lasciare il Mondo Addizione.",
|
||||
"2+2=4": "2+2=4",
|
||||
"2 + 2 ≠ 5 is boring to prove in full, given only the tools we have currently.\nTo make it a bit less painful, I have unfolded all of the numerals for you.\nSee if you can use `zero_ne_succ` and `succ_inj` to prove this.":
|
||||
"2 + 2 ≠ 5 è noioso da dimostrare per intero con le tattiche che abbiamo a disposizione al momento.\nPer salvarti un po' di lavoro, ho espanso in anticipo tutti i numeri per te.\nCompleta la dimostrazione utilizzando `zero_ne_succ` e `succ_inj`.",
|
||||
"2 + 2 ≠ 5": "2 + 2 ≠ 5",
|
||||
"1 ≠ 0": "1 ≠ 0",
|
||||
"0 ≤ x": "0 ≤ x",
|
||||
"*Game version: 4.2*\n\n*Recent additions: Inequality world, algorithm world*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
|
||||
"*Versione del gioco: 4.2*\n\n*Aggiunti di recente: Mondo Disequazioni, Mondo Algoritmi*\n\n## Salvataggio del gioco\n\nIl gioco salva il tuo progresso nella memoria locale del browser.\nSe cancelli la memoria, perderai anche i dati del gioco! (le tue preziose dimostrazioni!)\n\nAttenzione: nella maggior parte dei browser, cancellare i cookies cancella anche la memoria di un sito\n(o \"i dati locali del sito\"). In ogni caso, assicurati di esportare il tuo progresso del gioco!\n\n## Riconoscimenti\n\n* **Autori:** Kevin Buzzard, Jon Eugster\n* **Versione originale per Lean3:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Livelli extra:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Traduzione italiana**: Federico Dal Pio Luogo\n* **Grazie anche a:** Gli studenti che si sono offerti come beta testers, tutte le scuole\nche hanno invitato Kevin a parlare, e gli studenti che gli hanno fatto domande\nsul materiale.\n\n## Risorse\n\n* La [chat di Lean su Zulip](https://leanprover.zulipchat.com/)\n* Il [gioco originale per Lean3](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problemi?\n\nRivolgi le tue domande sul gioco nella\n[chat di Lean su Zulip](https://leanprover.zulipchat.com/), utilizzando\nlo stream \"New Members\". I membri della comunità sono felici di aiutare. Nota che\nla chat di Lean su Zulip è un forum professionale di ricerca.\nPerciò usa il tuo nome reale e per intero, rimani in tema, e sii cortese. Se cerchi\nun forum più informale (dove puoi ad esempio postare\ni meme sui numeri naturali) allora il [server Discord di Lean](https://discord.gg/WZ9bs9UCvx) fa per te.\n\nIn alternativa, se il gioco funziona male o dovessi trovare un bug puoi aprire una issue su github:\n\n* Per problemi relativi al game engine, apri una\n[issue sul repo lean4game](https://github.com/leanprover-community/lean4game/issues).\n* Per problemi relativi ai contenuti del the gioco, apri una\n[issue sul repo NNG](https://github.com/hhu-adam/NNG4/issues).",
|
||||
"$x=37\\implies x=37$.": "$x=37\\implies x=37$.",
|
||||
"$x+y=x\\implies y=0$.": "$x+y=x\\implies y=0$.",
|
||||
"$x+1=y+1 \\implies x=y$.": "$x+1=y+1 \\implies x=y$.",
|
||||
"$x + y = y\\implies x=0.$": "$x + y = y\\implies x=0.$",
|
||||
"$n+a=n+b\\implies a=b$.": "$n+a=n+b\\implies a=b$.",
|
||||
"$a+n=b+n\\implies a=b$.": "$a+n=b+n\\implies a=b$.",
|
||||
"$a+(b+0)+(c+0)=a+b+c.$": "$a+(b+0)+(c+0)=a+b+c.$",
|
||||
"$\\operatorname{succ}(a) \\neq 0$.": "$\\operatorname{succ}(a) \\neq 0$.",
|
||||
"$20+20=40$.": "$20+20=40$.",
|
||||
"$2+2≠5$.": "$2+2≠5$.",
|
||||
"$2+2=4$.": "$2+2=4$.",
|
||||
"$2+2 \\neq 5.$": "$2+2 \\neq 5.$",
|
||||
"$2$ is the number after the number after $0$.":
|
||||
"$2$ è il numero che viene dopo il numero che viene dopo $0$.",
|
||||
"$1\\neq0$.": "$1\\neq0$.",
|
||||
"$0\\neq1$.": "$0\\neq1$.",
|
||||
"$0 ^ 0 = 1$": "$0 ^ 0 = 1$",
|
||||
"## The birth of number.\n\nNumbers in Lean are defined by two rules.\n\n* `0` is a number.\n* If `n` is a number, then the *successor* `succ n` of `n` is a number.\n\nThe successor of `n` means the number after `n`. Let's learn to\ncount, and name a few small numbers.\n\n## Counting to four.\n\n`0` is a number, so `succ 0` is a number. Let's call this new number `1`.\nSimilarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.\nThis gives us plenty of numbers to be getting along with.\n\nThe *proof* that `2 = succ 1` is called `two_eq_succ_one`.\nCheck out the \"012\" tab in the list of lemmas on the right\nfor this and other proofs.\n\nLet's prove that $2$ is the number after the number after zero.":
|
||||
"## La nascita dei numeri\n\nI numeri in Lean sono definiti da due regole:\n\n* `0` è un numero.\n* Se `n` è un numero, allora il *successore* `succ n` di `n` è un numero.\n\nIl successore di `n` è il numero che viene dopo `n`. Impariamo a contare in questo sistema,\nprovando a scrivere alcuni numeri piccoli.\n\n## Contiamo fino a quattro\n\n`0` è un numero, e `succ 0` è un numero. Diamo a quest'ultimo numero il nome `1`.\nIn modo simile, definiamo `2 = succ 1`, `3 = succ 2` e `4 = succ 3`.\nQuesti primi quattro numeri sono più che sufficienti per proseguire il nostro ragionamento.\n\nLa *dimostrazione* di `2 = succ 1` si chiama `two_eq_succ_one`.\nPuoi trovarla cliccando sul tab \"012\" nella lista di lemmi a destra nell'interfaccia,\ndove vedrai lei e altre dimostrazioni.\n\nOra dimostriamo che $2$ è il numero che viene dopo il numero che viene dopo zero.",
|
||||
"## Summary\n\n`rfl` proves goals of the form `X = X`.\n\nIn other words, the `rfl` tactic will close any goal of the\nform `A = B` if `A` and `B` are *identical*.\n\n`rfl` is short for \\\"reflexivity (of equality)\\\".\n\n## Example:\n\nIf the goal looks like this:\n\n```\nx + 37 = x + 37\n```\n\nthen `rfl` will close it. But if it looks like `0 + x = x` then `rfl` won't work, because even\nthough $0+x$ and $x$ are always equal as *numbers*, they are not equal as *terms*.\nThe only term which is identical to `0 + x` is `0 + x`.\n\n## Details\n\n`rfl` is short for \\\"reflexivity of equality\\\".\n\n## Game Implementation\n\n*Note that our `rfl` is weaker than the version used in core Lean and `mathlib`,\nfor pedagogical purposes; mathematicians do not distinguish between propositional\nand definitional equality because they think about definitions in a different way\nto type theorists (`zero_add` and `add_zero` are both \\\"facts\\\" as far\nas mathematicians are concerned, and who cares what the definition of addition is).*":
|
||||
"## Riassunto\n\n`rfl` dimostra obiettivi della forma `X = X`.\n\nDetto in altre parole, la tattica `rfl` chiuderà qualsiasi goal della forma\nforma `A = B` se `A` e `B` sono termini *identici*, ovvero sono scritti nello stesso modo.\n\n`rfl` è l'abbreviazione di \"riflessività (di uguaglianza)\".\n\n## Esempio:\n\nSe questo è il goal:\n\n```\nx + 37 = x + 37\n```\n\nallora `rfl` lo chiuderà. Ma su questo `0 + x = x` `rfl` non funzionerà, perché sebbene $0+x$ e $x$ *rappresentino* lo stesso numero, non sono termini identici.\nPerciò, l'unico termine identico a `0 + x` è `0 + x`.\n\n## Nel dettaglio\n\n`rfl' è l'abbreviazione di `\"reflexivity of equality\".\n\n## Note di implementazione\n\n*Per motivi didattici questo gioco usa una versione di `rfl` più debole della versione di Lean e della sua libreria `mathlib`;\ninfatti nella matematica classica non vi è distinzione tra uguaglianza proposizionale e\ne uguaglianza denotazionale, questa distinzione è rilevante solo nella teoria dei tipi.\n(ad esempio, `zero_add` e `add_zero` sono entrambi dei \\\"fatti\\\" per quanto riguarda i matematici,\na loro non interessa quale sia la definizione precisa di addizione).*",
|
||||
"## Summary\n\n`repeat t` repeatedly applies the tactic `t`\nto the goal. You don't need to use this\ntactic, it just speeds things up sometimes.\n\n## Example\n\n`repeat rw [add_zero]` will turn the goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\ninto the goal\n`a = b`.\n\"\n\nTacticDoc nth_rewrite \"\n## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.":
|
||||
"## Descrizione\n\n`repeat t` applica la tattica `t`\nnel goal ripetitivamente. Non è necessario usare questa tattica\nper completare il gioco, ma a volte è utile nel rendere le dimostrazioni più succinte.\n\n## Esempio\n\n`repeat rw [add_zero]` trasformerà il goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\nnel nuovo goal\n`a = b`.\n\"\n\nTacticDoc nth_rewrite \"\n## Descrizione\n\nSe hai `h : X = Y` e ci sono diverse `X` nel goal, allora\n`nth_rewrite 3 [h]` sostituirà solo la terza `X` in `Y`.\n\n## Esempio\n\nSe nel goal hai `2 + 2 = 4` allora con `nth_rewrite 2 [two_eq_succ_one]`\nsostituisce la seconda occorrenza del lato sinistro di `two_eq_succ_one`, e il goal diventa `2 + succ 1 = 4`. Invece il normale `rw [two_eq_succ_one]`\nsostituira la prima occorrenza di `2` nel goal, che diventa `succ 1 + succ 1 = 4`.",
|
||||
"## Summary\n\n`repeat t` repeatedly applies the tactic `t`\nto the goal. You don't need to use this\ntactic, it just speeds things up sometimes.\n\n## Example\n\n`repeat rw [add_zero]` will turn the goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\ninto the goal\n`a = b`.":
|
||||
"## Descrizione\n\n`repeat t` applica la tattica `t`\nnel goal ripetitivamente. Non è strettamente necessaria al fine di\ncompletare il gioco, ma a volte è utile per velocizzare le dimostrazioni.\n\n## Esempio\n\n`repeat rw [add_zero]` trasformerà il goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\nnel nuovo goal\n`a = b`.",
|
||||
"## Summary\n\nThe `use` tactic makes progress with goals which claim something *exists*.\nIf the goal claims that some `x` exists with some property, and you know\nthat `x = 37` will work, then `use 37` will make progress.\n\nBecause `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\nyou can make progress on goals of the form `a ≤ b` by `use`ing the\nnumber which is morally `b - a`.":
|
||||
"## Descrizione\n\nLa tattica `use` permette di avanzare su goal che postulano l'*esistenza* di qualcosa.\nSe il goal afferma che esiste una certa `x`con qualche proprietà, e sei sicuro\nche `x = 37` la soddisfi, allora con `use 37` farai progresso nella dimostrazione.\n\nDato che `a ≤ b` è notazione per \\\"there exists `c` such that `b = a + c`\\\",\npuoi fare progresso su goal della forma `a ≤ b` passando a `use`\nquel numero che corrisponde a `b - a`, la distanza tra `a` e `b`.",
|
||||
"## Summary\n\nThe `symm` tactic will change a goal or hypothesis of\nthe form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\nand on `X ↔ Y`.\n\n### Example\n\nIf the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n\n### Example\n\nIf `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`.":
|
||||
"## Descrizione\n\nLa tattica `symm` trasformerà un goal o un'ipotesi della forma di\nun'uguaglianza `X = Y` in `Y = X`. Funziona anche sulla disuguaglianza `X ≠ Y`\ne sull'equivalenza `X ↔ Y`.\n\n### Esempio\n\nSe il goal è `2 + 2 = 4`, `symm` lo trasformerà in `4 = 2 + 2`.\n\n### Esempio\n\nSe hai `h : 2 + 2 ≠ 5` allora `symm at h` trasformerà `h` in `5 ≠ 2 + 2`.",
|
||||
"## Summary\n\nIf the goal is a statement `P`, then `exact h` will close the goal if `h` is a proof of `P`.\n\n### Example\n\nIf the goal is `x = 37` and you have a hypothesis `h : x = 37`\nthen `exact h` will solve the goal.\n\n### Example\n\nIf the goal is `x + 0 = x` then `exact add_zero x` will close the goal.\n\n### Exact needs to be exactly right\n\nNote that `exact add_zero` will *not work* in the previous example;\nfor `exact h` to work, `h` has to be *exactly* a proof of the goal.\n`add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,\na proof of `? + 0 = ?` where `?` needs to be supplied by the user.\nThis is in contrast to `rw` and `apply`, which will \\\"guess the inputs\\\"\nif necessary. If the goal is `x + 0 = x` then `rw [add_zero]`\nand `rw [add_zero x]` will both change the goal to `x = x`,\nbecause `rw` guesses the input to the function `add_zero`.":
|
||||
"## Descrizione\n\nSe il goal è una proposizione `P`, `exact h` lo risolverà se `h` è una dimostrazione di `P`.\n\n### Esempio\n\nSe il goal è `x = 37` e tra le ipotesi hai `h : x = 37`\ncon `exact h` chiuderai il goal.\n\n### Esempio\n\nSe il goal è `x + 0 = x`, `exact add_zero x` chiuderà il goal.\n\n### `exact` deve coincidere esattamente con il goal\n\nÈ bene notare che `exact add_zero` *non funzionerà* nell'esempio di prima;\ncome dice il nome, `exact h` ha successo solo se `h` coincide *esattamente* al goal.\n`add_zero` è la dimostrazione dell'enunciato più generale `∀ n, n + 0 = n` o, con notazione più intuitiva,\nalla dimostrazione di `? + 0 = ?` dove `?` deve essere fornito dall'utente.\nDiversamente da `rw` e `apply`, i quali tentano di \\\"indovinare i loro input\\\"\nquando essi sono assenti, `exact` vuole la pappa pronta. Ad esempio, se il goal è `x + 0 = x` sia `rw [add_zero]`\nche `rw [add_zero x]` porteranno il goal a `x = x`,\nperché `rw` è in grado di indovinare (o meglio, dedurre dal contesto) gli input della funzione `add_zero`.",
|
||||
"## Summary\n\nIf the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,\nand change the goal to `Q`. Mathematically, it says that to prove $P \\implies Q$,\nwe can assume $P$ and then prove $Q$.\n\n### Example:\n\nIf your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1 \\implies x=y$)\nthen `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal\nwill change to $x=y$.":
|
||||
"## Descrizione\n\nSe il goal è `P → Q`, allora `intro h` introdurrà `h : P` come ipotesi,\ne lascerà nel goal solo `Q`. Nella matematica, per dimostrare l'implicazione $P \\implies Q$,\npossiamo dare per vero $P$ e dimostrare $Q$.\n\n### Ad esempio:\n\nSe il goal è `x + 1 = y + 1 → x = y` (codice Lean per $x+1=y+1 \\implies x=y$)\nallora `intro h` creerà un'ipotesi $x+1=y+1$ con nome `h`, e il goal\ndiventerà $x=y$.",
|
||||
"## Summary\n\nIf `t : P → Q` is a proof that $P \\implies Q$, and `h : P` is a proof of `P`,\nthen `apply t at h` will change `h` to a proof of `Q`. The idea is that if\nyou know `P` is true, then you can deduce from `t` that `Q` is true.\n\nIf the *goal* is `Q`, then `apply t` will \\\"argue backwards\\\" and change the\ngoal to `P`. The idea here is that if you want to prove `Q`, then by `t`\nit suffices to prove `P`, so you can reduce the goal to proving `P`.\n\n### Example:\n\n`succ_inj x y` is a proof that `succ x = succ y → x = y`.\n\nSo if you have a hypothesis `h : succ (a + 37) = succ (b + 42)`\nthen `apply succ_inj at h` will change `h` to `a + 37 = b + 42`.\nYou could write `apply succ_inj (a + 37) (b + 42) at h`\nbut Lean is smart enough to figure out the inputs to `succ_inj`.\n\n### Example\n\nIf the goal is `a * b = 7`, then `apply succ_inj` will turn the\ngoal into `succ (a * b) = succ 7`.":
|
||||
"## Descrizione\n\nSe `t : P → Q` è una dimostrazione di $P \\implies Q$, e `h : P` è una dimostrazione di `P`,\nallora `apply t at h` trasformerà `h` in una dimostrazione di `Q`. L'idea alla base di questo è\nche se sai che `P` è vera, allora l'implicazione `t` ti permette di dedurre che `Q` è vera.\n\nAl contrario, se il *goal* è `Q`, allora `apply t` \\\"ragionerà all'indietro\\\" e trasformerà il\ngoal in `P`. È sempre l'implicazione che ci permette di farlo: `Q` è garantito da `t`\nse riesci a dimostrare `P`, quindi il goal si riduce a una dimostrazione di `P`.\n\n### Esempio:\n\n`succ_inj x y` è una dimostrazione di `succ x = succ y → x = y` (un'implicazione).\n\nQuindi, se hai l'ipotesi `h : succ (a + 37) = succ (b + 42)`\nallora con `apply succ_inj at h` trasformerai `h` in `a + 37 = b + 42`.\nPuoi anche fornire gli argomenti direttamente `apply succ_inj (a + 37) (b + 42) at h`\nma Lean fa questo lavoro per noi e capisce da solo cosa deve passare a `succ_inj`.\n\n### Esempio\n\nSe hai il goal `a * b = 7`, con `apply succ_inj` trasformerai il\ngoal in `succ (a * b) = succ 7`.",
|
||||
"## Summary\n\nIf `n` is a number, then `cases n with d` will break the goal into two goals,\none with `n = 0` and the other with `n = succ d`.\n\nIf `h` is a proof (for example a hypothesis), then `cases h with...` will break the\nproof up into the pieces used to prove it.\n\n## Example\n\nIf `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,\none with `n` replaced by 0 and the other with `n` replaced by `succ d`. This\ncorresponds to the mathematical idea that every natural number is either `0`\nor a successor.\n\n## Example\n\nIf `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal\ninto two goals, one with a hypothesis `hp : P` and the other with a\nhypothesis `hq : Q`.\n\n## Example\n\nIf `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,\nbecause there are no ways to make a proof of `False`! And if you have no goals left,\nyou have finished the level.\n\n## Example\n\nIf `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`\nand a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is\n`∃ c, b = a + c`.":
|
||||
"## Descrizione\n\nSe `n` è un numero, allora `cases n with d` spezzerà il goal in due goal,\nuno dove `n = 0` e un altro dove `n = succ d`.\n\nSe `h` è una dimostrazione (per esempio tra le ipotesi), allora `cases h with...` spezzerà\nla dimostrazione in tante parti quante quanti i modi di derivare `h`.\n\n## Esempio\n\nSe `n : ℕ` è un numero, allora `cases n with d` spezzerà il goal in due subgoal,\nuno dove `n` è stato rimpiazzato da 0 e l'altro dove `n` è stato rimpiazzato da `succ d`. Questo\ncorrisponde all'intuizione matematica che ogni numero naturale è o `0`\noppure un successore.\n\n## Esempio\n\nSe `h : P ∨ Q` è un'ipotesi, allora `cases h with hp hq` trasformerà il goal\nin due goal, uno con l'ipotesi `hp : P` e l'altro con\nl'ipotesi `hq : Q`.\n\n## Esempio\n\nSe `h : False` è un'ipotesi, allora `cases h` trasformerà il goal in zero goal,\nperché non vi è alcun modo di dimostrare `False`! E se rimani con zero cose da dimostrare\nvuol dire che hai completato il livello.\n\n## Esempio\n\nSe `h : a ≤ b` è un'ipotesi, allora `cases h with c hc` istanzierà un nuovo numero `c`\ne una dimostrazione di `hc : b = a + c`. Questo deriva dalla *definizione* di `a ≤ b`, che è\n`∃ c, b = a + c`.",
|
||||
"## Summary\n\nIf `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\nattempts to prove the goal by induction on `n`, with the inductive\nvariable in the successor case being `d`, and the inductive hypothesis being `hd`.\n\n### Example:\nIf the goal is\n```\n0 + n = n\n```\n\nthen\n\n`induction n with d hd`\n\nwill turn it into two goals. The first is `0 + 0 = 0`;\nthe second has an assumption `hd : 0 + d = d` and goal\n`0 + succ d = succ d`.\n\nNote that you must prove the first\ngoal before you can access the second one.":
|
||||
"## Descrizione\n\nSe `n : ℕ` è un oggetto, e il goal fa il nome di `n`, allora `induction n with d hd`\navvia la dimostrazione per induzione attorno alla variabile `n`, con la variabile\ninduttiva nel caso del successore chiamata `d` e l'ipotesi induttiva chiamata`hd`.\n\n### Esempio:\nSe il goal è\n```\n0 + n = n\n```\n\nallora\n\n`induction n with d hd`\n\nlo spezzerà in sue sotto-goal. Il primo è `0 + 0 = 0`;\nil secondo porta ha con sé un ipotesi `hd : 0 + d = d` e il goal\n`0 + succ d = succ d`.\n\nTieni presente che devi dimostrare il primo\ngoal prima di avere accesso al secondo.",
|
||||
"## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`'s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.":
|
||||
"## Descrizione\n\nSe `h` è una prova dell'uguaglianza `X = Y`, allora `rw [h]` scriverà\n`Y` al posto di ogni `X` nel goal. `rw` svolge l'operazione di \\\"sostituzione\\\".\n\n## Varianti di `rw`\n\n* `rw [← h]` (riscrive le `Y` con `X`; per avere la freccetta all'indietro si digita `\\left ` oppure `\\l`.)\n\n* `rw [h1, h2]` (sostituzioni in sequenza)\n\n* `rw [h] at h2` (riscrive le `X` in `Y` nell'ipotesi `h2`)\n\n* `rw [h] at h1 h2 ⊢` (riscrive le `X` in `Y` in due ipotesi e nel goal;\nper avere il simbolo `⊢` digita `\\|-`.)\n\n* `repeat rw [add_zero]` riscriverà continuamente `? + 0` in `?`\nfinché non riesce più a trovare espressioni della forma `? + 0`.\n\n* `nth_rewrite 2 [h]` riscriverà solo la seconda `X` nel goal in `Y`.\n\n### Esempio:\n\nSe hai l'ipotesi `h : x = y + y` e il goal è\n```\nsucc (x + 0) = succ (y + y)\n```\n\nallora il comando\n\n`rw [add_zero]`\n\nriscriverà il goal in `succ x = succ (y + y)`, e poi il comando\n\n`rw [h]`\n\nriscriverà il goal in `succ (y + y) = succ (y + y)`, il quale\npuò essere risolto con `rfl`.\n\n### Esempio:\n\n`rw` può anche riscrivere nelle ipotesi.\nAd esempio, se hai le seguenti due ipotesi:\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\neseguendo `rw [h1] at h2` sostituirà la `x` dentro `h2`, che diventerà `h2 : 2 * y = y + 3`.\n\n## Errori comuni\n\n* `rw` accetta una lista di teoremi, dunque le parentesi quadre sono sempre da mettere. Scrivere `rw h` è un errore di sintassi.\n\n* Inoltre, gli argomenti che passi a `rw` devono essere *prove* di *uguaglianza*, dunque dei teoremi che hai dimostrato in precedenza e che hanno la forma`A = B`).\nScrivere `rw [P = Q]` è sbagliato: `P = Q` è solo l'*affermazione* dell'uguaglianza,\nnon la sua dimostrazione. Se invece hai `h : P = Q` nel contesto, `h` è una dimostrazione di `P = Q` e allora potrai scrivere `rw [h]`.\n\n## Dettagli\n\n`rw` è la tattica che svolge la \\\"sostituzione\\\". Ci sono due casi in cui può\nessere usata:\n\n1) Uso basilare: se `h : A = B` è un'ipotesi del contesto\noppure la dimostrazione di un teorema, e se il goal contiene una o più `A`, allora `rw [h]`\nle sostituirà tutte con `B`. La tattica darà un errore\nse non ci sono `A` nel goal.\n\n2) Uso avanzato: certi teoremi hanno delle incognite.\n Ad esempio, `add_zero`\npuò essere trattato come un funzione il cui corpo è `? + 0 = ?`\ndove `?` è l'input. Applicando `rw` a `add_zero`, `rw` cercherà all'interno del goal\nun termine della forma `x + 0`; appena lo trova\nfissa l'incognita `?` a `x` e cambierà tutte le occorrenze di `x + 0` a `x`.\n\nEsercizio: prova a spiegare perché `rw [add_zero]` trasforma il termine\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` in\n`0 + (x + 0) + 0 + (x + 0)`\n\nSe non ti ricordi il nome di una dimostrazione di un'uguaglianza, puoi cercarlo\nnell'elenco di lemma sulla destra.\n\n## Uso mirato\n\nSe nel goal hai `b + c + a = b + (a + c)` e vuoi riscrivere solo il termine `a + c`\na `c + a`, invocare semplicemente `rw [add_comm]` non darà il risultato che ti aspetti perché Lean\napplica il teorema sulla prima espressione che ha un match con un'addizione. Puoi usare `rw [add_comm a c]` per\nfar sì che Lean riscriva `a + c` a `c + a`. In questo modo stai fissando le incognite del teorema:\n`add_comm` è la prova di `?1 + ?2 = ?2 + ?1`, `add_comm a` è la prova\ndi `a + ? = ? + a`, e infine `add_comm a c` è la prova di `a + c = c + a`.\n\nData la dimostrazione `h : X = Y`, `rw [h]` riscriverà tutte le `X` a `Y` nel goal.\nPer cambiare solo la trentasettesima occorrenza di `X`\na `Y`, il metodo giusto è `nth_rewrite 37 [h]`.",
|
||||
"## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.":
|
||||
"## Descrizione\n\nSe hai `h : X = Y` e nel goal ci sono diverse `X`, con\n`nth_rewrite 3 [h]` puoi cambiare solo la terza `X` in `Y`.\n\n## Esempio\n\nSe il goal è `2 + 2 = 4` allora `nth_rewrite 2 [two_eq_succ_one]`\nsostituirà la seconda occorrenza di `2`, e il goal diventerà `2 + succ 1 = 4`. Invece, il semplice `rw [two_eq_succ_one]`\nsostituirà tutte le occorrenze di `2` e il goal diventerà `succ 1 + succ 1 = 4`.",
|
||||
"## Precision rewriting\n\nIn the last level, there was `b + 0` and `c + 0`,\nand `rw [add_zero]` changed the first one it saw,\nwhich was `b + 0`. Let's learn how to tell Lean\nto change `c + 0` first by giving `add_zero` an\nexplicit input.":
|
||||
"## Rewriting mirato\n\nNell'ultimo livello vi erano sia `b + 0` che `c + 0` da riscrivere,\ne `rw [add_zero]` ha scelto il primo che ha trovato,\nossia `b + 0`. Impariamo come dire a Lean\ndi riscrivere `c + 0` per primo dando ad `add_zero` un\ninput esplicito.",
|
||||
"# Welcome to the Natural Number Game\n#### An introduction to mathematical proof.\n\nIn this game, we will build the basic theory of the natural\nnumbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\nthat `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\nAnd at the end we'll see if we can prove Fermat's Last Theorem.\nWe'll do this by solving levels of a computer puzzle game called Lean.\n\n# Read this.\n\nLearning how to use an interactive theorem prover takes time.\nTests show that the people who get the most out of this game are\nthose who read the help texts like this one.\n\nTo start, click on \"Tutorial World\".\n\nNote: this is a new Lean 4 version of the game containing several\nworlds which were not present in the old Lean 3 version. A new version\nof Advanced Multiplication World is in preparation, and worlds\nsuch as Prime Number World and more will be appearing during October and\nNovember 2023.\n\n## More\n\nClick on the three lines in the top right and select \"Game Info\" for resources,\nlinks, and ways to interact with the Lean community.":
|
||||
"# Benvenuto nel Gioco dei Numeri Naturali!\n#### Un'introduzione alla dimostrazione matematica.\n\nIn questo gioco costruiremo la teoria elementare dei numeri naturali\n`{0,1,2,3,4,...}` a partire da zero. Il nostro primo obiettivo è dimostrare\n`2 + 2 = 4`. Dopodiché dimostreremo `x + y = y + x`.\nInfine cercheremo di dimostrare l'Ultimo Teorema di Fermat.\nRisolveremo questi puzzle matematici in un ambiente interattivo chiamato Lean.\n\n# Leggi le istruzioni!\n\nImparare a usare un *interactive theorem prover* richiede tempo e impegno.\nLe statistiche mostrano che le persone che imparano di più da questo gioco sono\ncoloro che leggono attentamente il testo delle istruzioni, come questo.\n\nPer iniziare, clicca su \"Mondo Tutorial\".\n\nNota: questa è la versione del gioco per Lean 4 contenente diversi\nmondi che non erano presenti nella versione per Lean 3. Stiamo lavorando a una\nnuova versione del Mondo Moltiplicazione Avanzata e nuovi mondi\ntra cui Mondo Numeri Primi arriveranno durante Ottobre e\nNovembre 2023.\n\n## Altro\n\nClicca sulle tree lineette in alto a destra e seleziona \"Game Info\" per risorse,\nlink utili e vari modi per connetterti alla comunità di Lean.",
|
||||
"# Summary\nThe `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `Q` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $Q \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.":
|
||||
"# Descrizione\nLa tattica `right` trasforma un goal della forma `P ∨ Q` nel nuovo goal `Q`.\nUsala quando le tue ipotesi garantiscono che si può dedurre `P ∨ Q`\n\ndalla verità di `Q`.\n\nL'implementazione di Lean di questa tattica non fa altro che `apply` di un teorema\nche dice che $Q \\implies P \\lor Q.$\n\nNota bene che questa tattica può portare il tuo goal a uno stato irrisolvibile.",
|
||||
"# Summary\nThe `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `P` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $P \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.":
|
||||
"# Descrizione\nLa tattica `left` trasforma un goal della forma `P ∨ Q` nel nuovo goal `P`.\nUsala quando le tue ipotesi garantiscono che si può dedurre `P ∨ Q`\ndalla verità di `P`.\n\nL'implementazione di Lean di questa tattica non fa altro che l'`apply` di un teorema\nche dice $P \\implies P \\lor Q.$\n\nNota bene che questa tattica può portare il tuo goal a uno stato irrisolvibile.",
|
||||
"# Summary\n\n`trivial` will solve the goal `True`.":
|
||||
"# Descrizione\n\n`trivial` risolve il goal `True`.",
|
||||
"# Summary\n\n`decide` will attempt to solve a goal if it can find an algorithm which it\ncan run to solve it.\n\n## Example\n\nA term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\nare equal or different. Hence, once this term is made and made into an `instance`,\nthe `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.":
|
||||
"# Descrizione\n\nLa tattica `decide` cercherà di risolvere il goal se esiste un algoritmo\nche possiamo eseguire per risolverlo.\n\n## Esempio\n\nUn termine di tipo `DecidableEq ℕ` è un algoritmo che decide se due naturali\nsono uguali o diversi. Dunque, se abbiamo un'istanza di questo tipo,\nla tattica `decide` può usare la sua implementazione per risolvere i goal della forma `a = b` or `a ≠ b`.",
|
||||
"# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n\n## Example\n\nIf you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.":
|
||||
"# Descrizione\n\nLa tattica `tauto` risolverà qualsiasi goal che può essere tramite puro ragionamento logico (ossia, tramite le\ntavole di verità).\n\n## Esempio\n\nSe hai `False` come ipotesi, allora `tauto` risolverà\nil goal. Questo perché un'ipotesi false implica qualsiasi cosa.\n\n## Esempio\n\nSe hai il goal `True`, allora `tauto` risolverà il goal.\n\n## Esempio\n\nSe hai due ipotesi `h1 : a = 37` e `h2 : a ≠ 37` allora `tauto` risolverà\nsolve il goal perché può dedurre `False` dalle tue ipotesi, e quindi\ndimostrare il goal (dato che `False` implica qualsiasi cosa).\n\n## Esempio\n\nSe hai un'ipotesi `h : a ≠ a` allora `tauto` risolverà il goal perché\nè abbastanza intelligente da capire che `a = a` è vero, arrivando alla contraddizione che cerchiamo.\n\n## Esempio\n\nSe hai un'ipotesi della forma `a = 0 → a * b = 0` e hai il goal `a * b ≠ 0 → a ≠ 0`, allora\n`tauto` risolverà il goal, because esso è logicamente equivalente all'ipotesi.\nE se scambi il ruolo del goal e dell'ipotesi in questo esempio, `tauto` lo risolverebbe lo stesso.",
|
||||
"# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.":
|
||||
"# Descrizione\n\nLa tattica `have` può essere usata per aggiungere un'ipotesi a un livello, ma ovviamente ti chiede\ndi dimostrarla.\n\n\n## Esempio\n\nIl suo utilizzo più semplice e così. Se hai `a` nel contesto e vuoi eseguire\n\n`have ha : a = 0`\n\nallora otterrai un nuovo goal `a = 0` da dimostrare, e dopo che l'hai dimostrato\navrai l'ipotesi `ha : a = 0` nel contesto originale.\n\n## Esempio\n\nSe hai già pronta la dimostrazione di ciò che vuoi introdurre con `have`,\npuoi farlo in un unico comando. Ad esempio, se hai `a` e `b`\ncome numeri, allora\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\naggiungerà direttamente l'ipotesi `h2 : succ a = succ b → a = b`\nal contesto, dato che hai fornito assieme la sua dimostrazione (`succ_inj a b`).\n\n## Esempio\n\nSe hai in mano una dimostrazione, puoi omettere il lemma che vuoi introdurre (quello tra i simboli `:` e `:=`).\nAd esempio:\n\n`have h2 := succ_inj a b`\n\naggiungerà `h2 : succ a = succ b → a = b` come ipotesi.",
|
||||
"# Summary\n\nIf you have a hypothesis\n\n`h : a ≠ b`\n\nand goal\n\n`c ≠ d`\n\nthen `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\na hypothesis\n\n`h : c = d`\n\nand goal\n\n`a = b`.":
|
||||
"# Descrizione\n\nSe hai un'ipotesi\n\n`h : a ≠ b`\n\ne il goal\n\n`c ≠ d`\n\nallora `contrapose! h` cambierà l'impostazione con la cosiddetta \\\"contronominale\\\":\nun ipotesi\n\n`h : c = d`\n\ne il goal\n\n`a = b`.",
|
||||
"# Statement\n\nIf $a$ and $b$ are numbers, then\n`succ_inj a b` is the proof that\n$ (\\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\n## More technical details\n\nThere are other ways to think about `succ_inj`.\n\nYou can think about `succ_inj` itself as a function which takes two\nnumbers $$a$$ and $$b$$ as input, and outputs a proof of\n$ ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\nYou can think of `succ_inj` itself as a proof; it is the proof\nthat `succ` is an injective function. In other words,\n`succ_inj` is a proof of\n$\\forall a, b \\in \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\n`succ_inj` was postulated as an axiom by Peano, but\nin Lean it can be proved using `pred`, a mathematically\npathological function.":
|
||||
"# Enunciato\n\nSe $a$ e $b$ sono numeri, allora\n`succ_inj a b` è la dimostrazione che\n$ (\\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\n## Dettagli tecnici\n\nCi sono diversi modi di interpretare `succ_inj`.\n\nSi può pensare a `succ_inj` come una funzione che prende in input due\nnumeri $$a$$ e $$b$$, e restituisce una dimostrazione di\n$ ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\nMa `succ_inj` in sé e anche una dimostrazione; ovvero la dimostrazione\nche `succ` è una funzione iniettiva. In termini matematici,\n`succ_inj` è una dimostrazione di\n$\\forall a, b \\in \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\n`succ_inj` fu postulato da Peano come un'assioma, ma\nin Lean può essere dimostrato usando `pred`, una funzione che non va\nmolto d'accordo con i numeri naturali.",
|
||||
"# Read this first\n\nEach level in this game involves proving a mathematical theorem (the \"Goal\").\nThe goal will be a statement about *numbers*. Some numbers in this game have known values.\nThose numbers have names like $37$. Other numbers will be secret. They're called things\nlike $x$ and $q$. We know $x$ is a number, we just don't know which one.\n\nIn this first level we're going to prove the theorem that $37x + q = 37x + q$.\nYou can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`\nare numbers.\n\nWe solve goals in Lean using *Tactics*, and the first tactic we're\ngoing to learn is called `rfl`, which proves all theorems of the form $X = X$.\n\nProve that $37x+q=37x+q$ by executing the `rfl` tactic.":
|
||||
"# Leggi questo prima\n\nCiascun livello di questo gioco consiste nel dimostrare un teorema matematico (il cosiddetto \"goal\").\nIl goal è tipicamente un'affermazione che riguarda dei numeri. Certi numeri avranno dei valori ben precisi,\ncome $37$. Altri numeri saranno invece dati come incognite, e queste verranno denotate con delle lettere quali $x$ o $q$.\nPossiamo dire con certezza che $x$ è un numero, ma non sappiamo quale!\n\nIn questo primo livello dimostreremo il teorema $37x + q = 37x + q$.\nNella sezione *Oggetti* in basso puoi vedere `x q : ℕ`, che significa che `x` e `q`\nsono numeri naturali.\n\nPer risolvere i goal in Lean usiamo le *tattiche*. La prima tattica che vedremo si chiama `rfl`, che\ndimostra tutti i goal della forma $X = X$.\n\nAdesso tocca a te! Dimostra $37x+q=37x+q$ eseguendo la tattica `rfl`.",
|
||||
"# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
|
||||
"# Overview\n\nLa nostra tattica casalinga `simp_add` risolverà qualsiasi goal\ndel tipo `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
|
||||
"# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
|
||||
"# Overview\n\nIl semplificatore di Lean, `simp`, riscriverà ogni\nlemma con il tag `simp` e ogni lemma dato dall'utente, finché può.\nNon solo, cercherà di ordinare le variabili secondo la sua logica interna affinché non entri\nin un loop infinito quando utilizza lemmi come `add_comm`"}
|
||||
5450
.i18n/it/Game.po
Normal file
5450
.i18n/it/Game.po
Normal file
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user