lean - TPIL 3.6：示例：¬（p ↔ ¬p）

Question

标签： lean

Answer 1

这是玩这些谜题的互动方式： https ://leanprover-community.github.io/lean-web-editor/#code=example%20%28p%20%3A%20Prop%29%20%3A% 20%C2%AC%28p%20%E2%86%94%20%C2%ACp%29%20%3A%3D%0Abegin%0A%20%20assume%20H%2C%0A%20%20have%20hp% 20%3A%20p%20%3A%3D%20H.mpr%20%28%CE%BB%20hp%2C%20_%29%2C%0A%20%20all_goals%0A%20%20%7B%20have% 20hp_copy%20%3A%3D%20hp%2C%0A%20%20%20%20rw%20H%20at%20hp_copy%2C%0A%20%20%20%20矛盾%20%7D%2C%0Aend

example (p : Prop) : ¬(p ↔ ¬p) :=
begin
  assume H,
  have hp : p := H.mpr (λ hp, _),
  all_goals
  { have hp_copy := hp,
    rw H at hp_copy,
    contradiction },
end