Zulip Chat Archive

Stream: new members

Topic: How to increase memory threshold in code


view this post on Zulip Lars Ericson (Dec 24 2020 at 00:18):

I am in code on ubuntu. I get this message:

excessive memory consumption detected at 'expression equality test' (potential solution: increase memory consumption threshold)

How do I increase the memory consumption threshold when lean is getting started up under the hood of code?

view this post on Zulip Yakov Pechersky (Dec 24 2020 at 00:22):

Ctrl-, to bring up settings. Search for Lean memory. Mine is set at 8K.

view this post on Zulip Yakov Pechersky (Dec 24 2020 at 00:22):

Lean: Memory Limit is the setting

view this post on Zulip Yakov Pechersky (Dec 24 2020 at 00:23):

but whatever term you're trying to #reduce, the amount you increase to might not be sufficient

view this post on Zulip Lars Ericson (Dec 24 2020 at 00:28):

Thanks @Yakov Pechersky I am trying to do a proof of the theorem that "The cancellation law of multiplication for integral domains is equivalent in a commutative ring to the assertion that a product of nonzero factors is not 0."

I am translating this as (c ≠ 0 → c*a = c*b → a = b) ↔ (a ≠ 0 → b ≠ 0 → a * b ≠ 0) . With this translation, at a certain point, library_search and suggest run out of memory. I don't know how to prove it from the comm_ring axioms:

import algebra.ring.basic
import tactic

universe u

variables {α : Type u} [comm_ring α] {a b c z x₁ x₂ :  α}

/- Theorem 1. The cancellation law of multiplication for integral domains
is equivalent in a commutative ring to the assertion that
a product of nonzero factors is not 0. -/

lemma lemma_1_LR: (c  0  c*a = c*b  a = b)   (a  0  b  0  a * b  0) :=
begin
  intro h1,
  intro h2,
  intro h3,
  intro h4,
  by_cases h5 : c  0,
  have h6 := h1 h5,
  by_cases h7 : c * a = c * b,
  have h8 := h6 h7,
  sorry,
  sorry,
  sorry,
end

lemma lemma_1_RL: (a  0  b  0  a * b  0)  (c  0  c*a = c*b  a = b)  :=
begin
  intro h1,
  intro h2,
  intro h3,
  by_cases h4 : a  0,
  have h5 := h1 h4,
  by_cases h6 : c*a = c*b,
  by_cases h7 : b  0,
  have h8 := h5 h7,
  sorry,
  sorry,
  sorry,
  sorry,
end

theorem theorem_1 : (c  0  c*a = c*b  a = b)  (a  0  b  0  a * b  0) :=
begin
  split,
  exact lemma_1_LR,
  exact lemma_1_RL,
end

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:11):

your theorems need additional forall quantifications on each side

view this post on Zulip Lars Ericson (Dec 24 2020 at 01:12):

Thanks @Mario Carneiro , I will refine.

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:12):

theorem theorem_1 :
  ( a b c : α, c  0  c*a = c*b  a = b) 
  ( a b : α, a  0  b  0  a * b  0) :=
sorry

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:13):

generally when it says you should increase your memory limit, you should ignore the suggestion because something else is going wrong

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:20):

Here's a partial proof to help you get started:

theorem theorem_1 :
  ( a b c : α, c  0  c*a = c*b  a = b) 
  ( a b : α, a  0  b  0  a * b  0) :=
begin
  split,
  { intros H a b ha hb ab,
    refine hb (H _ _ _ ha _),
    sorry },
  { intros H a b c hc e,
    rw  sub_eq_zero at e ,
    refine by_contra (λ h, _),
    refine H c (a - b) hc h _,
    sorry },
end

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:22):

For some reason using by_contra h instead of refine by_contra (λ h, _), is taking a really long time for me (but it doesn't time out or run out of memory). Possibly something weird ended up in the typeclass search for decidable_eq A

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:40):

minimized:

import algebra.ring.basic
import data.set.basic

lemma foo (p) [decidable p] : true := trivial

set_option trace.class_instances true
example {α} [semigroup α] (a : α) : a = a :=
by do
  tgt  tactic.target,
  tactic.mk_mapp `foo [some tgt, none]

You can also play with the import set to make it take longer; import tactic is quite bad.

@Gabriel Ebner Could you take a look at whether the typeclass problem is reasonably sized here? It seems like the decision to make linear_order inherit from decidable_eq means that the decidability problem gets quite large, and while caching seems to help I see a lot of repetition from a cursory glance at the log.

view this post on Zulip Lars Ericson (Dec 24 2020 at 02:04):

Thanks again @Mario Carneiro here is the finished Theorem 1:

/- Theorem 1. The cancellation law of multiplication for integral domains
is equivalent in a commutative ring to the assertion that
a product of nonzero factors is not 0. -/

lemma left_distrib_minus : c * a - c * b = c * (a - b) :=
begin
  ring,
end

theorem theorem_1 :
  ( a b c : α, c  0  c*a = c*b  a = b) 
  ( a b : α, a  0  b  0  a * b  0) :=
begin
  split,
  { intros H a b ha hb ab,
    refine hb (H _ _ _ ha _),
    have hc := mul_zero a,
    rw hc,
    rw ab,
  },
  { intros H a b c hc e,
    rw  sub_eq_zero at e ,
    refine by_contra (λ h, _),
    refine H c (a - b) hc h _,
    rw left_distrib_minus at e,
    exact e,
  },
end

view this post on Zulip Mario Carneiro (Dec 24 2020 at 02:06):

left_distrib_minus has a name, can you find it?

view this post on Zulip Lars Ericson (Dec 24 2020 at 02:39):

@Mario Carneiro left_distrib doesn't quite fit because it is phrased for a+b and this is a-b and if you instantiate it you get a+(-b) which doesn't quite match the hypothesis set. I played around with it and ended up having to use a different lemma which instead of sugaring ring, sugars rfl:

lemma deminus_plus (a b : α): a + -b = a - b := rfl

theorem theorem_1 :
  ( a b c : α, c  0  c*a = c*b  a = b) 
  ( a b : α, a  0  b  0  a * b  0) :=
begin
  split,
  { intros H a b ha hb ab,
    refine hb (H _ _ _ ha _),
    have hc := mul_zero a,
    rw hc,
    rw ab,
  },
  { intros H a b c hc e,
    rw  sub_eq_zero at e ,
    refine by_contra (λ h, _),
    refine H c (a - b) hc h _,
    have hd := left_distrib c a (-b),
    have he := deminus_plus a b,
    rw he at hd,
    have hf := norm_num.mul_pos_neg c b (c * b) rfl,
    rw hf at hd,
    have hg := deminus_plus (c*a) (c*b),
    rw hg at hd,
    rw hd,
    exact e,
  },
end

I don't know how to make use of rfl "inline" as a tactic in this case. If you can help me rewrite one of the deminus_plus lines to use rfl then I can finish it.

view this post on Zulip Mario Carneiro (Dec 24 2020 at 02:40):

Recall the #naming convention

view this post on Zulip Mario Carneiro (Dec 24 2020 at 02:40):

what would be the name of a lemma that combines multiplication and subtraction?

view this post on Zulip Mario Carneiro (Dec 24 2020 at 02:42):

deminus_plus also has a name that the naming convention will guide you to

view this post on Zulip Mario Carneiro (Dec 24 2020 at 02:43):

If you want to prove the have he := deminus_plus ... lines using rfl you will have to state the expected type as in have he : <type> := rfl

view this post on Zulip Lars Ericson (Dec 24 2020 at 02:46):

I have one hypotheses I need to edit:

hd: c * (a + -b) = c * a + c * -b

to become

hd: c * (a - b) = c * a - c * b

I'll look for add_neg names or plus_neg names.

view this post on Zulip Lars Ericson (Dec 24 2020 at 02:54):

Ah docs#sub_eq_add_neg.

view this post on Zulip Lars Ericson (Dec 24 2020 at 03:02):

DONE:

import algebra.ring.basic
import tactic

universe u

variables {α : Type u} [comm_ring α]

/- Theorem 1. The cancellation law of multiplication for integral domains
is equivalent in a commutative ring to the assertion that
a product of nonzero factors is not 0. -/

theorem theorem_1 :
  ( a b c : α, c  0  c*a = c*b  a = b) 
  ( a b : α, a  0  b  0  a * b  0) :=
begin
  split,
  { intros H a b ha hb ab,
    refine hb (H _ _ _ ha _),
    have hc := mul_zero a,
    rw hc,
    rw ab,
  },
  { intros H a b c hc e,
    rw  sub_eq_zero at e ,
    refine by_contra (λ h, _),
    refine H c (a - b) hc h _,
    have hd := left_distrib c a (-b),
    have he := sub_eq_add_neg a b,
    rw  he at hd,
    have hf := norm_num.mul_pos_neg c b (c * b) rfl,
    rw hf at hd,
    have hg := sub_eq_add_neg (c*a) (c*b),
    rw  hg at hd,
    rw hd,
    exact e,
  },
end

view this post on Zulip Mario Carneiro (Dec 24 2020 at 03:34):

I'll look for add_neg names or plus_neg names.

Always add, never plus

view this post on Zulip Mario Carneiro (Dec 24 2020 at 03:36):

Your original proof used a theorem a * (b - c) = a * b - a * c. Have you found that lemma yet?

view this post on Zulip Lars Ericson (Dec 24 2020 at 04:06):

The code underneath DONE above is pure matlib, there is no extra lemma. I use the built-in left_distrib and built-in sub_eq_add_neg.

view this post on Zulip Mario Carneiro (Dec 24 2020 at 06:20):

You are proving this fact a * (b - c) = a * b - a * c in the middle of your proof, and you don't need to. It's good to get a sense for what to expect in the library, and a distribution lemma like this will certainly be in there. (Since you missed the naming hints, the name is docs#mul_sub.)


Last updated: May 13 2021 at 18:26 UTC