La relación de divisibilidad es transitiva
Demostrar que la relación de divisibilidad es transitiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import tactic variables {a b c : ℕ} example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := sorry |
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 |
import tactic variables {a b c : ℕ} -- 1ª demostración -- =============== example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := begin rcases hab with ⟨d, hd : b = a * d⟩, rcases hbc with ⟨e, he : c = b * e⟩, have h1 : c = a * (d * e), calc c = b * e : he ... = (a * d) * e : congr_arg (* e) hd ... = a * (d * e) : mul_assoc a d e, show a ∣ c, by exact dvd.intro (d * e) (eq.symm h1), end -- 2ª demostración -- =============== example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := begin cases hab with d hd, cases hbc with e he, rw [he, hd], use (d * e), exact mul_assoc a d e, end -- 3ª demostración -- =============== example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := begin rcases hbc with ⟨e, rfl⟩, rcases hab with ⟨d, rfl⟩, use (d * e), ring, end -- 4ª demostración -- =============== example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := -- by library_search dvd_trans hab hbc |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 32.
