Zulip Chat Archive

Stream: general

Topic: Equality is not an equality or iff


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 23 2019 at 00:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 23 2019 at 10:06):

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

view this post on Zulip 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)))

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:33):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:38):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:43):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 23 2019 at 12:44):

Weird error though.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 23 2019 at 12:59):

Ideally something I can reproduce in VS Code

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 23 2019 at 13:00):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 23 2019 at 14:11):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 23 2019 at 14:43):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 23 2019 at 15:19):

yes, at least not without some hackery

view this post on Zulip Mario Carneiro (Nov 23 2019 at 15:28):

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.

view this post on Zulip 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