Zulip Chat Archive

Stream: new members

Topic: let with proposition in tactic mode


view this post on Zulip Kenny Lau (Dec 13 2018 at 15:45):

import tactic.interactive

open function

meta def tactic.interactive.result : tactic unit :=
do e  tactic.result, tactic.trace e

theorem cantor_surjective
  (X : Type) (f : X  set X) (Hf : surjective f) : false :=
begin
  let H := Hf {x | x  f x},
  cases H with D e,
  result
  -- ⊢ (let H : ∃ (a : X), f a = {x : X | x ∉ f x} := Hf {x : X | x ∉ f x} in false) (Exists.intro D e)
end

/-
let H : ∃ (a : X), f a = {x : X | x ∉ f x} := _,
    H_1 : ∃ (a : X), f a = {x : X | x ∉ f x} := _
in Exists.dcases_on H_1 (λ (D : X) (e : f D = {x : X | x ∉ f x}), ?m_1[H, H_1, D, e])
-/

view this post on Zulip Kenny Lau (Dec 13 2018 at 15:45):

somehow there's a strange goal if we use let instead of have with a proposition in tactic mode

view this post on Zulip Kenny Lau (Dec 13 2018 at 15:46):

compare this:

view this post on Zulip Kenny Lau (Dec 13 2018 at 15:46):

import tactic.interactive

open function

meta def tactic.interactive.result : tactic unit :=
do e  tactic.result, tactic.trace e

theorem cantor_surjective
  (X : Type) (f : X  set X) (Hf : surjective f) : false :=
begin
  have H := Hf {x | x  f x},
  cases H with D e,
  result
  -- ⊢ false
end

/-
Exists.dcases_on (Hf {x : X | x ∉ f x})
  (λ (D : X) (e : f D = {x : X | x ∉ f x}), ?m_1[Hf {x : X | x ∉ f x}, Hf {x : X | x ∉ f x}, D, e])
-/

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 16:08):

Moral: don't use let with propositions?

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 16:08):

Background: Kenny just watched me giving a live Lean talk and I used let with a proposition :P


Last updated: May 09 2021 at 19:11 UTC