Equality is not an equality or iff

Stream: general

[Abhimanyu Pallavi Sudhir]

Unfortunately it's hard to strip this down to a MWE -- this is the code.

The error is in forced_sum_val. Apparently Hs₃ : ⇑(linear_independent.repr H) ⟨s, Hs₂⟩ = finsupp.single 0 1, is not an equality or iff. Am I making an obvious mistake?

[Kevin Buzzard]

On modern mathlib I get time-outs in forced_sum :-/

[Kevin Buzzard]

So I can only reproduce this in the lean web editor. I would recommend that that you try this in VS Code Abhi. I know you said that VS Code was slow but the Lean Web Editor is necessarily slower because it's running the same underlying code in a more inefficient way (a javascript translation of the C++ instead of the C++). The error message is completely bonkers. If you write set_option pp.all true in front of forced_sum_val and then wait forever you might be able to find out why the rewrite fails -- perhaps the terms look equal but are not precisely equal.

[Kevin Buzzard]

With VS Code you get problems earlier in the file which might indicate where things are actually going wrong.

[Kevin Buzzard]

I'm looking at the actual terms and superficially it looks like they should match, but they are really huge. You might need some expert advice about how to make the terms more compact. This might be the actual problem -- the code you're writing is producing mega-large terms for some reason.

[Mario Carneiro]

You shouldn't be using if-then in forced_sum, it's a Prop and it's not decidable

[Mario Carneiro]

But for me the problem seems to be that linear_independent ℝ (λ m n : ℕ, s (n + m)) takes forever to elaborate, because module ℝ (ℕ → ℝ) takes forever to synthesize, because of some instances in ring_theory.algebra_operations. I think we need to take another look at these instances, this isn't the first time they have caused trouble

[Mario Carneiro]

setting priorities helped, so probably this is fixed with #1724

[Mario Carneiro]

In any case, the right definition of forced_sum is

def forced_sum (s : ℕ → ℝ) (H : linear_independent ℝ (λ m n : ℕ, s (n + m))) (S : ℝ) (t : ℕ → ℝ) (T : ℝ) : Prop :=
∃ Ht : t ∈ span ℝ (set.range (λ m n : ℕ, s (n + m))),
T = finsupp.sum (linear_independent.repr H ⟨t, Ht⟩)
  (λ n r, r * (S - finset.univ.sum (λ k : fin n, s k.val)))

[Mario Carneiro]

The sum over fin n isn't necessary, you can sum a finset of nats instead, and this makes forced_sum_val easier:

def forced_sum (s : ℕ → ℝ) (H : linear_independent ℝ (λ m n : ℕ, s (n + m))) (S : ℝ) (t : ℕ → ℝ) (T : ℝ) : Prop :=
∃ Ht : t ∈ span ℝ (set.range (λ m n : ℕ, s (n + m))),
T = finsupp.sum (linear_independent.repr H ⟨t, Ht⟩)
  (λ n r, r * (S - (finset.range n).sum s))

lemma forced_sum_val (s : ℕ → ℝ) (H : linear_independent ℝ (λ m n : ℕ, s (n + m))) (S : ℝ) :
  forced_sum s H S s S :=
begin
  have Hs₁ : s ∈ set.range (λ m n : ℕ, s (n + m)) := set.mem_range.mpr ⟨0, rfl⟩,
  have Hs₂ : s ∈ span ℝ (set.range (λ m n : ℕ, s (n + m))) := spanning_set_subset_span Hs₁,
  have Hs₃ := linear_independent.repr_eq_single H 0 ⟨s, Hs₂⟩ rfl,
  use Hs₂, simp [Hs₃, finsupp.sum_single_index]
end

[Abhimanyu Pallavi Sudhir]

Thanks -- it turns out i don't need ring_theory.algebra_operations -- it's much faster now without it.

I'm surprised it doesn't accidentally get imported through data.real.basic or something though.

[Abhimanyu Pallavi Sudhir]

Wait a minute -- the rewrite/simp still doesn't work though.

[Abhimanyu Pallavi Sudhir]

I think it genuinely thinks Hs₃ is not an equality.

[Abhimanyu Pallavi Sudhir]

OK, It works if I specify the type of Hs3.

[Abhimanyu Pallavi Sudhir]

Weird error though.

[Kevin Buzzard]

I've seen this once before, quite recently. Can you minimise? Or at least show me an example of it failing and not taking a long time to fail?

[Kevin Buzzard]

Ideally something I can reproduce in VS Code

[Abhimanyu Pallavi Sudhir]

If you remove the import ring_theory.algebra_operations, it happens quickly.

[Mario Carneiro]

It's probably because you have an assigned metavariable caused by the tactic that created the hypothesis

[Mario Carneiro]

I don't think have h : _ := ... will cause this, but you will notice that my code used have h := ... instead

[Mario Carneiro]

yep, this is the cause

example : 2 + 3 = 0 :=
begin
  have := add_comm 2 3,
  rw this, -- no problem
  sorry,
end

example : 2 + 3 = 0 :=
begin
  have : _ := add_comm 2 3,
  rw this, -- rewrite tactic failed, lemma is not an equality nor a iff
  sorry,
end

example : 2 + 3 = 0 :=
begin
  have : _ = _ := add_comm 2 3,
  rw this, -- rewrite tactic failed, lemma lhs is a metavariable
  sorry,
end

example : 2 + 3 = 0 :=
begin
  have : _ + _ = _ := add_comm 2 3,
  rw this, -- no problem
  sorry,
end

[Abhimanyu Pallavi Sudhir]

Huh. I don't think I'd ever seen this happen before.

[Abhimanyu Pallavi Sudhir]

I'm still not sure I understand. Why does Lean care how I defined the have statement? The statement introduced to the environment is still the same -- no metavariables. Right?

[Kevin Buzzard]

Is this one of those things where the end user can't see what's going on?

[Mario Carneiro]

yes, at least not without some hackery

[Mario Carneiro]

open tactic
example : 2 + 3 = 0 :=
begin
  have := add_comm 2 3,
  (do get_local `this >>= infer_type >>= trace ∘ expr.to_raw_fmt),
  -- (app (app (app (const eq [1]) ... (fully elaborated)
end

example : 2 + 3 = 0 :=
begin
  have : _ := add_comm 2 3,
  (do get_local `this >>= infer_type >>= trace ∘ expr.to_raw_fmt),
  -- (mvar ...)
end

example : 2 + 3 = 0 :=
begin
  have : _ = _ := add_comm 2 3,
  (do get_local `this >>= infer_type >>= trace ∘ expr.to_raw_fmt),
  -- (app (app (app (const eq [?_mlocal._fresh.1485.2073]) (mvar) (mvar)) (mvar))
end

example : 2 + 3 = 0 :=
begin
  have : _ + _ = _ := add_comm 2 3,
  (do get_local `this >>= infer_type >>= trace ∘ expr.to_raw_fmt),
  -- (app (app (app (const eq [?_mlocal._fresh.1599.1006+1]) (mvar))
    -- (app (app (app (app (const has_add.add) (mvar)) (mvar)) (mvar)) (mvar))) (mvar))
end

This shows the actual type of the this variable after each call. The mvars normally appear as ?m_1 when printed, but these are mvars that have already been assigned, so the pretty printer goes ahead and shows the assignment. But several uncarefully written tactics match directly on this type rather than unfolding metavariables first, and rw's equality check is one of these. It just says "is this expr an eq application? If not, fail" and so it fails because it is actually an mvar which is an eq application if lean were to check the metavariable assignment.

[Mario Carneiro]

Basically, the type of the first this is 2 + 3 = 3 + 2, and the type of the second is ?m_1 where ?m_1 := 2 + 3 = 3 + 2