Cómo probar que x < y → x ≤ y - 2 si ambos son impares o ambos son pares en Lean?

Answer

1. 

   davy.ai

   July 12, 2023 at 9:17 pm

   Para probar que si dos números ℤ son ambos pares o ambos impares, lo más cercanos que pueden estar si no son iguales es a una distancia de 2, podemos utilizar la siguiente demostración:

   import data.int.basic
   import data.int.parity
   
   theorem even_even_at_least_two_apart { x y : ℤ } : even x ∧ even y → x < y → x ≤ y - 2 :=
   begin
     intros hx hy hlt,
     rw int.even_iff at hx hy,
     rcases hx with ⟨k, rfl⟩,
     rcases hy with ⟨l, rfl⟩,
     have hdiff : l - k ≥ 2,
     { cases hlt with h h,
       { rw [← even_iff_sub_two_right, even_iff] at h,
         rw [even_iff_sub_two_right, even_iff],
         exact h },
       { exact h } },
     rw ← sub_le_iff_le_add',
     rw ← sub_add_cancel y k,
     rw ← sub_add_cancel (l - 2) k,
     apply sub_le_sub,
     { rw [mul_sub_right_distrib, mul_one],
       rw add_sub_add_left,
       exact le_refl k },
     { rw [mul_sub_right_distrib, mul_one],
       rw sub_sub_sub_right,
       rw add_sub_add_left,
       exact hdiff },
   end
   

   Comenzamos introduciendo las suposiciones hx y hy, las cuales afirman que x e y son ambos pares. También introducimos la suposición hlt, la cual establece que x < y.

   Luego, utilizamos el lema even_iff para reescribir hx y hy como afirmaciones sobre sus cocientes correspondientes, k y l. Hacemos esto emparejando los lados derechos del lema even_iff con hx y hy, y emparejando los lados izquierdos con ⟨k, rfl⟩ y ⟨l, rfl⟩, respectivamente.

   A continuación, utilizamos una declaración cases en hlt para considerar dos casos: o bien x es dos unidades menor que y, o es menor que dos unidades menor que y. En el primer caso, utilizamos nuevamente el lema even_iff para reescribir hx como una afirmación sobre k - 1 y hy como una afirmación sobre l - 1. Luego podemos deducir que k y l son iguales o difieren al menos por 2. En el segundo caso, la diferencia entre k y l ya es al menos 2 según la suposición.

   Luego, utilizamos álgebra para reescribir la desigualdad x ≤ y - 2 como una desigualdad equivalente y - k ≥ 2. Primero restamos k de ambos lados, luego sumamos y restamos l - 2 en el lado derecho. Luego podemos aplicar el lema sub_le_sub para mostrar que k ≤ l - 2, lo cual se sigue de que la diferencia entre k y l es al menos 2. La demostración del lema se obtiene a través de manipulación algebraica de la desigualdad resultante.

   En general, esta demostración es bastante directa, aunque requiere un poco de manipulación algebraica hacia el final.

Comments are closed.