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

Question

此证明是 Avigad 等人 "Logic and Proof" 中的基于策略的版本

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 相同的错误，并且修复方法相同。

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

How to use `exists.elim` in Lean?

theorem-proving

lean