## Stream: new members

### Topic: Simple arithmetic statements: 1...4 divide 12

#### Laurent Bartholdi (Jun 23 2023 at 08:28):

Could some kind soul explain to me how to optimize the following:

example : ∀i ∈ ({1,2,3,4} : finset ℕ), ∃j : ℕ, i*j=12 := begin
intros i ih,
use 12/i,
finish,
end


? It takes for ages, and I'd like a 1-liner avoiding heavy-hitters like finish. I tried ring and its variants, without success, and case-by-case also seems not to work smoothly

#### Damiano Testa (Jun 23 2023 at 08:52):

First of all, rcases ih with rfl | rfl | rfl | rfl | ⟨⟨⟩⟩, helps! You can find out about it by using rcases? ih.

#### Damiano Testa (Jun 23 2023 at 08:54):

After that, norm_num works:

example : ∀i ∈ ({1,2,3,4} : finset ℕ), ∃j : ℕ, i*j=12 := begin
rintros i ih,
use 12/i,
rcases ih with rfl | rfl | rfl | rfl | ⟨⟨⟩⟩;
norm_num,
end


This is almost instant. Also the original version was not so bad, though...

#### Damiano Testa (Jun 23 2023 at 08:57):

Do you really need the ∃?

#### Damiano Testa (Jun 23 2023 at 08:57):

example : ∀i ∈ ({1,2,3,4} : finset ℕ), i*(12/i)=12 := by
rintros i (rfl | rfl | rfl | rfl | ⟨⟨⟩⟩); norm_num


#### Damiano Testa (Jun 23 2023 at 09:09):

Actually, with the last formulation, you can also prove it as: example : ∀i ∈ ({1,2,3,4} : finset ℕ), i*(12/i)=12 := by norm_num.

#### Laurent Bartholdi (Jun 23 2023 at 09:09):

Thanks a lot! Yes, I wrote a M(N)WE, but I need to get hold of the j. If you have improvement suggestions, here is where the code comes from:

variables {G : Type} [group G] (g : G) (foobar : G → set ℕ)
lemma l1 (j : ℕ) : foobar g ⊆ foobar (g^j) := sorry
lemma l2  : ∀i ∈ ({1,2,3,4} : finset ℕ), foobar (g^i) ⊆ foobar (g^12) := begin
intros i ih,
let j : ℕ := 12/i,
have div_12 : i*j = 12 := begin rcases ih with rfl | rfl | rfl | rfl | ⟨⟨⟩⟩; tauto end,
exact div_12 ▸ (pow_mul g i j).symm ▸ l1 (g^i) foobar j,
end


#### Anand Rao Tadipatri (Jun 23 2023 at 09:14):

Here is a (partial) solution using decide (this code snippet is in Lean4):

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Basic

class DecideForAllMemMem (F : Type _ → Type _) [∀ α, Membership α (F α)] where
decideForAllMem {P : α → Prop} [DecidablePred P] (l : F α) : Decidable (∀ a : α, a ∈ l → P a)

instance : DecideForAllMemMem List where
decideForAllMem := sorry

instance : DecideForAllMemMem Multiset where
decideForAllMem := sorry

instance : DecideForAllMemMem Finset where
decideForAllMem := sorry

attribute [instance] DecideForAllMemMem.decideForAllMem

example : ∀ i ∈ ({1,2,3,4} : Finset ℕ), i ∣ 12 := by
sorry -- decide


Lean already knows that a ∣ b is a decidable problem when a b : ℕ, and consequently for any l : Finset ℕ, the proposition ∀ i : ℕ, i ∈ l → i ∣ x should be decidable by enumeration. The code above is an (incomplete) attempt at getting Lean to perform decision by enumeration on Finsets. When all the sorrys are filled in, the proof should ideally just be by decide.

#### Damiano Testa (Jun 23 2023 at 09:43):

I do not know if this is any better for your application, but I find that the convert line let's me, as a human, know what is happening: we are applying l1; after that, it is just a case-check.

lemma l2  : ∀i ∈ ({1,2,3,4} : finset ℕ), foobar (g^i) ⊆ foobar (g^12) := begin
intros i ih,
convert l1 (g ^ i) foobar (12 / i) using 2,
rw ← pow_mul,
fin_cases ih;
norm_num,
end


Maybe this is more show-casing some of the automation that can be used, though...

The more I use Lean, the more I prefer writing proofs for humans, over highly-compressed machine-parseable code.

#### Laurent Bartholdi (Jun 25 2023 at 22:45):

If I dare, a followup question: how do I convert inequalities to a finset, as in

example (a : ℕ) (h : 1 ≤ a) (k : a ≤ 4) : a ∈ ({1,2,3,4} : finset ℕ) := sorry


?

#### Heather Macbeth (Jun 25 2023 at 22:50):

interval_cases a; tauto ? (Untested)

#### Damiano Testa (Jun 25 2023 at 22:53):

example (a : ℕ) (h : 1 ≤ a) (k : a ≤ 4) : a ∈ ({1,2,3,4} : finset ℕ) :=
begin
rcases a with _ | _ | _ | _ | _ | a;
try {linarith <|> simp, done},
change a + 5 ≤ 4 at k,
linarith,
end


#### Damiano Testa (Jun 25 2023 at 22:56):

Heather's suggestion is better though, but using simp instead of tauto.

#### Yakov Pechersky (Jun 26 2023 at 10:32):

If you're converting inequalities to a finset, then you should use a construction like Finset.range instead of a manual construction as you have now that is via Finset.insert

Last updated: Dec 20 2023 at 11:08 UTC