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