Stream: new members

Topic: How to increase memory threshold in code

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?

Yakov Pechersky (Dec 24 2020 at 00:22):

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

Yakov Pechersky (Dec 24 2020 at 00:22):

Lean: Memory Limit is the setting

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

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


Lars Ericson (Dec 24 2020 at 01:12):

Thanks @Mario Carneiro , I will refine.

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


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

Mario Carneiro (Dec 24 2020 at 01:20):

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


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

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.

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


Mario Carneiro (Dec 24 2020 at 02:06):

left_distrib_minus has a name, can you find it?

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.

Mario Carneiro (Dec 24 2020 at 02:40):

Recall the #naming convention

Mario Carneiro (Dec 24 2020 at 02:40):

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

Mario Carneiro (Dec 24 2020 at 02:42):

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

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

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.

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


Mario Carneiro (Dec 24 2020 at 03:34):

I'll look for add_neg names or plus_neg names.

Always add, never plus

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?

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.

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: Dec 20 2023 at 11:08 UTC