Как использовать `существующие.elim` в Lean?

Question

Это доказательство является версией, основанной на тактике, в версии "Logi c and Proof" Avigad et al.

import data.nat.prime
open nat

theorem sqrt_two_irrational_V2 {a b : ℕ} (co : gcd a b = 1) : a^2 ≠ 2 * b^2 :=
begin
    intro h,
    have h1 : 2 ∣ a^2, by simp [h],
    have h2 : 2 ∣ a, from prime.dvd_of_dvd_pow prime_two h1,
    cases h2 with c aeq,
    have h3 : 2 * (2 * c^2) = 2 * b^2,
        by simp [eq.symm h, aeq];
            simp [nat.pow_succ, mul_comm, mul_assoc, mul_left_comm],
    have h4 : 2 * c^2 = b^2,
        from eq_of_mul_eq_mul_left dec_trivial h3,
    have h5 : 2 ∣ b^2,
        by simp [eq.symm h4],
    have hb : 2 ∣ b,
        from prime.dvd_of_dvd_pow prime_two h5,
    have h6 : 2 ∣ gcd a b, from dvd_gcd (exists.intro c aeq) hb,
    have habs : 2 ∣ (1:ℕ), by simp * at *,
    exact absurd habs dec_trivial, done
end

, которая работает. Я пытаюсь вернуться назад в руководстве по Lean, потому что тактический режим гораздо более интуитивен для меня. Когда я пытаюсь сделать то же самое без тактики, у меня возникают проблемы с частью exists.elim, поскольку все примеры в руководстве по Lean показывают, как использовать ее только для того, чтобы получить конечную цель, а не промежуточный шаг. Может кто-нибудь помочь мне исправить этот код? Может ли let или match также использоваться для той же цели?

theorem sqrt_two_irrational_V1 {a b : ℕ} (co : gcd a b = 1) : a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
    by simp [h],
have ha : 2 ∣ a,
    from prime.dvd_of_dvd_pow prime_two this,
-- this line below is wrong
exists.elim ha (assume c : ℕ, assume aeq : a = 2 * c), 
-- also tried "let" and "match"
--let ⟨c, aeq⟩ := ha,
-- match ha with ⟨(c : ℕ), (aeq : a = 2 * c)⟩,
have 2 * (2 * c^2) = 2 * b^2,
    by simp [eq.symm h, aeq]; 
       simp [nat.pow_succ, mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
    from eq_of_mul_eq_mul_left dec_trivial this,
have 2 ∣ b^2, 
    by simp [eq.symm this],
have hb : 2 ∣ b,
    from prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
    from dvd_gcd ha hb,
have habs : 2 ∣ (1:ℕ), 
    by simp * at *,
show false, from absurd habs dec_trivial

Answer 1

Я переместил одну скобку, чтобы исправить доказательство. Обычно, когда вы используете exists.elim, все остальные доказательства должны быть в скобках.

theorem sqrt_two_irrational_V1 {a b : ℕ} (co : gcd a b = 1) : a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
    by simp [h],
have ha : 2 ∣ a,
    from prime.dvd_of_dvd_pow prime_two this,
-- this line below is wrong
exists.elim ha (assume c : ℕ, assume aeq : a = 2 * c, 
-- also tried "let" and "match"
--let ⟨c, aeq⟩ := ha,
-- match ha with ⟨(c : ℕ), (aeq : a = 2 * c)⟩,
have 2 * (2 * c^2) = 2 * b^2,
    by simp [eq.symm h, aeq]; 
       simp [nat.pow_succ, mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
    from eq_of_mul_eq_mul_left dec_trivial this,
have 2 ∣ b^2, 
    by simp [eq.symm this],
have hb : 2 ∣ b,
    from prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
    from dvd_gcd ha hb,
have habs : 2 ∣ (1:ℕ), 
    by simp * at *,
show false, from absurd habs dec_trivial)

Я обычно использую let вместо exists.elim. Синтаксис let ⟨c, aeq⟩ := ha in ... Это фактически вызывает ошибку в вашем текущем доказательстве, это связано с ошибкой, которая означает, что let вводит гипотезу под названием _let_match в ваш контекст, которая вызывает ошибку, если вы ее используете. simp * at * использует его в своем доказательстве, но если вы замените его на by clear_aux_decl; simp * at *, доказательство сработает.

Вы также можете написать match ha with | ⟨c, aeq⟩ := вместо let ⟨c, aeq⟩ := ha in, но на этот раз вы должны поставить end в конце доказательства. Это будет иметь ту же ошибку, что и с let, и исправление будет таким же.