Zulip Chat Archive

Stream: new members

Topic: Specializing weak implicit arguments


view this post on Zulip Li Yao'an (Nov 21 2019 at 09:36):

I'm trying to work with the inductive definition in mathlib. If I didn't misinterpret the notation, it uses weak implicit arguments in the forall quantifier, which I am having trouble trying to specialize, since unlike normal arguments, h a does not specialize the hypothesis with argument a. The exact example I'm trying to do is below. How does one deal with these weak implicit arguments?

def bijective' {α β} (f : α → β) : Prop :=
    ∃ f' : β → α, (∀ a : α, f' (f a) = a) ∧ (∀ b : β, f (f' b) = b)

theorem bijective_iff_bijective' {α β} (f : α → β) : bijective f ↔ bijective' f :=
begin
    dunfold bijective bijective' surjective injective, split,
        {intro h, cases h with h1 h2, existsi λ b, classical.some (h2 b), simp, split,
            {intro a, have h3 := some_spec (h2 (f a)), sorry}, -- How to resolve this?
            {sorry}},
        {sorry},
    done
end

view this post on Zulip Mario Carneiro (Nov 21 2019 at 11:55):

You don't really need to in this case, you can just fill the sorry with exact h1 h3

view this post on Zulip Mario Carneiro (Nov 21 2019 at 11:56):

but you can apply a weak implicit using @h1 (some _) a

view this post on Zulip Kevin Buzzard (Nov 21 2019 at 13:35):

Note also the choose tactic:

import tactic.interactive

open function

def bijective' {α β} (f : α  β) : Prop :=
     f' : β  α, ( a : α, f' (f a) = a)  ( b : β, f (f' b) = b)

theorem bijective_iff_bijective' {α β} (f : α  β) : bijective f  bijective' f :=
begin
  split,
  { intro h,
    choose f' h' using h.2,
    use f',
    split,
      sorry,
    exact h',
  },
  sorry
end

Last updated: May 08 2021 at 17:33 UTC