How to increase memory threshold in code

Stream: new members

[Lars Ericson]

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]

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

[Yakov Pechersky]

Lean: Memory Limit is the setting

[Yakov Pechersky]

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

[Lars Ericson]

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]

your theorems need additional forall quantifications on each side

[Lars Ericson]

Thanks @Mario Carneiro , I will refine.

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

left_distrib_minus has a name, can you find it?

[Lars Ericson]

@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]

Recall the #naming convention

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

Ah docs#sub_eq_add_neg.

[Lars Ericson]

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]

I'll look for add_neg names or plus_neg names.

Always add, never plus

[Mario Carneiro]

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

[Lars Ericson]

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]

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.)