如何在精益中使用`exists.elim`？

Question

此证明是Avigad等人在“逻辑和证明”中使用的基于战术的版本

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

有效。我正在尝试在精益手册中向后走，因为战术模式对我来说更加直观。在没有战术的情况下尝试进行相同操作时，我会遇到exists.elim部分的问题，因为精益手册中的所有示例都显示了如何使用它仅是为了达到最终目标，而不是中间步骤。谁能帮我修复此代码？ 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相同的错误，并且修复方法相同。