1

这个证明是 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
4

1 回答 1

2

我移动了一个支架来固定证明。通常当你使用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并且修复是相同的。

于 2020-02-21T02:35:20.507 回答