## Stream: general

### Topic: Equality is not an equality or iff

#### Abhimanyu Pallavi Sudhir (Nov 23 2019 at 00:14):

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 (Nov 23 2019 at 00:19):

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

#### Kevin Buzzard (Nov 23 2019 at 08:27):

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 (Nov 23 2019 at 08:27):

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

#### Kevin Buzzard (Nov 23 2019 at 08:34):

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 (Nov 23 2019 at 09:46):

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

#### Mario Carneiro (Nov 23 2019 at 09:54):

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 (Nov 23 2019 at 10:06):

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

#### Mario Carneiro (Nov 23 2019 at 10:07):

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 (Nov 23 2019 at 10:15):

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 (Nov 23 2019 at 12:31):

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 (Nov 23 2019 at 12:33):

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

#### Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:38):

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

#### Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:43):

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

#### Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:44):

Weird error though.

#### Kevin Buzzard (Nov 23 2019 at 12:59):

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 (Nov 23 2019 at 12:59):

Ideally something I can reproduce in VS Code

#### Abhimanyu Pallavi Sudhir (Nov 23 2019 at 13:00):

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

#### Mario Carneiro (Nov 23 2019 at 14:07):

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

#### Mario Carneiro (Nov 23 2019 at 14:08):

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

#### Mario Carneiro (Nov 23 2019 at 14:11):

yep, this is the cause

example : 2 + 3 = 0 :=
begin
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 (Nov 23 2019 at 14:43):

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

#### Abhimanyu Pallavi Sudhir (Nov 23 2019 at 14:43):

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 (Nov 23 2019 at 14:47):

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

#### Mario Carneiro (Nov 23 2019 at 15:19):

yes, at least not without some hackery

#### Mario Carneiro (Nov 23 2019 at 15:28):

open tactic
example : 2 + 3 = 0 :=
begin
(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 (Nov 23 2019 at 15:30):

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

Last updated: May 12 2021 at 04:19 UTC