may_assume and instances

Stream: FLT-regular

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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]

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