# Zulip Chat Archive

## 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
```

#### Mario Carneiro (Dec 24 2020 at 01:11):

your theorems need additional forall quantifications on each side

#### 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):

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
```

#### 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 02:54):

#### 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