Zulip Chat Archive

Stream: FLT-regular

Topic: may_assume and instances


Eric Rodriguez (Nov 08 2021 at 23:53):

with dependent instances, may_assume breaks, e.g.:

example {p : Type*} [nonempty p] : nonempty p :=
begin
  may_assume : true, { exact nonempty p },
  --resetI,
  have := classical.arbitrary p, --error
end

If you just make it nonempty empty, for example, this issue won't manifest though! Does anyone know the "correct" way to fix it? I'm sure as a shim you could just put resetI at the end of every may_assume call, but that is probably slow

Alex J. Best (Nov 09 2021 at 00:01):

Oh right, as it just uses intros if you have instances resetI seems necessary, does wlog' fare any better?

Eric Rodriguez (Nov 09 2021 at 00:10):

ooh, yes it does actually, but it doesn't generalize the statement enough so it doesn't work for my purposes. for example:

theorem flt_regular (p a b c : ) [fact p.prime] (hp : is_regular_number p) (hpne_two : p  2)
  (h : a ^ p + b ^ p = c ^ p) : a * b * c = 0 :=
begin
  wlog' hcoprime : set.pairwise {a, b, c} nat.coprime,
{  /-hcoprime: a^p + b^p = c^p → ... → a*b*c=0, without the ∀ a b c p -/
  sorry },
sorry
end

Alex J. Best (Nov 09 2021 at 00:17):

Yeah I think making may_assume do introsI instead of intros seems like the right solution

Eric Rodriguez (Nov 08 2021 at 23:53):

with dependent instances, may_assume breaks, e.g.:

example {p : Type*} [nonempty p] : nonempty p :=
begin
  may_assume : true, { exact nonempty p },
  --resetI,
  have := classical.arbitrary p, --error
end

If you just make it nonempty empty, for example, this issue won't manifest though! Does anyone know the "correct" way to fix it? I'm sure as a shim you could just put resetI at the end of every may_assume call, but that is probably slow

Alex J. Best (Nov 09 2021 at 00:01):

Oh right, as it just uses intros if you have instances resetI seems necessary, does wlog' fare any better?

Eric Rodriguez (Nov 09 2021 at 00:10):

ooh, yes it does actually, but it doesn't generalize the statement enough so it doesn't work for my purposes. for example:

theorem flt_regular (p a b c : ) [fact p.prime] (hp : is_regular_number p) (hpne_two : p  2)
  (h : a ^ p + b ^ p = c ^ p) : a * b * c = 0 :=
begin
  wlog' hcoprime : set.pairwise {a, b, c} nat.coprime,
{  /-hcoprime: a^p + b^p = c^p → ... → a*b*c=0, without the ∀ a b c p -/
  sorry },
sorry
end

Alex J. Best (Nov 09 2021 at 00:17):

Yeah I think making may_assume do introsI instead of intros seems like the right solution


Last updated: Dec 20 2023 at 11:08 UTC