## 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