Potencias de potencias en monoides
En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se caracteriza por los siguientes lemas:
1 2 |
pow_zero : x^0 = 1 pow_succ' : x^(succ n) = x * x^n |
Demostrar que si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces
1 |
a^(m * n) = (a^m)^n |
Indicación: Se puede usar el lema
1 |
pow_add : a^(m + n) = a^m * a^n |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 |
import algebra.group_power.basic open monoid nat variables {M : Type} [monoid M] variable a : M variables (m n : ℕ) set_option pp.structure_projections false example : a^(m * n) = (a^m)^n := sorry |
[expand title=»Soluciones con Lean»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 |
import algebra.group_power.basic open monoid nat variables {M : Type} [monoid M] variable a : M variables (m n : ℕ) -- Para que no use la notación con puntos set_option pp.structure_projections false -- 1ª demostración -- =============== example : a^(m * n) = (a^m)^n := begin induction n with n HI, { calc a^(m * 0) = a^0 : congr_arg ((^) a) (nat.mul_zero m) ... = 1 : pow_zero a ... = (a^m)^0 : (pow_zero (a^m)).symm }, { calc a^(m * succ n) = a^(m * n + m) : congr_arg ((^) a) (nat.mul_succ m n) ... = a^(m * n) * a^m : pow_add a (m * n) m ... = (a^m)^n * a^m : congr_arg (* a^m) HI ... = (a^m)^(succ n) : (pow_succ' (a^m) n).symm }, end -- 2ª demostración -- =============== example : a^(m * n) = (a^m)^n := begin induction n with n HI, { calc a^(m * 0) = a^0 : by simp only [nat.mul_zero] ... = 1 : by simp only [pow_zero] ... = (a^m)^0 : by simp only [pow_zero] }, { calc a^(m * succ n) = a^(m * n + m) : by simp only [nat.mul_succ] ... = a^(m * n) * a^m : by simp only [pow_add] ... = (a^m)^n * a^m : by simp only [HI] ... = (a^m)^succ n : by simp only [pow_succ'] }, end -- 3ª demostración -- =============== example : a^(m * n) = (a^m)^n := begin induction n with n HI, { calc a^(m * 0) = a^0 : by simp [nat.mul_zero] ... = 1 : by simp ... = (a^m)^0 : by simp }, { calc a^(m * succ n) = a^(m * n + m) : by simp [nat.mul_succ] ... = a^(m * n) * a^m : by simp [pow_add] ... = (a^m)^n * a^m : by simp [HI] ... = (a^m)^succ n : by simp [pow_succ'] }, end -- 4ª demostración -- =============== example : a^(m * n) = (a^m)^n := begin induction n with n HI, { by simp [nat.mul_zero] }, { by simp [nat.mul_succ, pow_add, HI, pow_succ'] }, end -- 5ª demostración -- =============== example : a^(m * n) = (a^m)^n := begin induction n with n HI, { rw nat.mul_zero, rw pow_zero, rw pow_zero, }, { rw nat.mul_succ, rw pow_add, rw HI, rw pow_succ', } end -- 6ª demostración -- =============== example : a^(m * n) = (a^m)^n := begin induction n with n HI, { rw [nat.mul_zero, pow_zero, pow_zero] }, { rw [nat.mul_succ, pow_add, HI, pow_succ'] } end -- 7ª demostración -- =============== example : a^(m * n) = (a^m)^n := pow_mul a m n |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 |
(* Potencias_de_potencias_en_monoides.thy theory Potencias_de_potencias_en_monoides imports Main begin context monoid_mult begin (* 1ª demostración *) lemma "a^(m * n) = (a^m)^n" proof (induct n) have "a ^ (m * 0) = a ^ 0" by (simp only: mult_0_right) also have "… = 1" by (simp only: power_0) also have "… = (a ^ m) ^ 0" by (simp only: power_0) finally show "a ^ (m * 0) = (a ^ m) ^ 0" by this next fix n assume HI : "a ^ (m * n) = (a ^ m) ^ n" have "a ^ (m * Suc n) = a ^ (m + m * n)" by (simp only: mult_Suc_right) also have "… = a ^ m * a ^ (m * n)" by (simp only: power_add) also have "… = a ^ m * (a ^ m) ^ n" by (simp only: HI) also have "… = (a ^ m) ^ Suc n" by (simp only: power_Suc) finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n" by this qed (* 2ª demostración *) lemma "a^(m * n) = (a^m)^n" proof (induct n) have "a ^ (m * 0) = a ^ 0" by simp also have "… = 1" by simp also have "… = (a ^ m) ^ 0" by simp finally show "a ^ (m * 0) = (a ^ m) ^ 0" . next fix n assume HI : "a ^ (m * n) = (a ^ m) ^ n" have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp also have "… = a ^ m * a ^ (m * n)" by (simp add: power_add) also have "… = a ^ m * (a ^ m) ^ n" using HI by simp also have "… = (a ^ m) ^ Suc n" by simp finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n" . qed (* 3ª demostración *) lemma "a^(m * n) = (a^m)^n" proof (induct n) case 0 then show ?case by simp next case (Suc n) then show ?case by (simp add: power_add) qed (* 4ª demostración *) lemma "a^(m * n) = (a^m)^n" by (induct n) (simp_all add: power_add) (* 5ª demostración *) lemma "a^(m * n) = (a^m)^n" by (simp only: power_mult) end end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]