Simple arithmetic statements: 1...4 divide 12

Stream: new members

[Laurent Bartholdi]

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]

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

[Damiano Testa]

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]

Do you really need the ∃?

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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]

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]

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]

interval_cases a; tauto ? (Untested)

[Damiano Testa]

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]

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

[Yakov Pechersky]

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