Dealing with multiple goals

Stream: mathlib4

[Gareth Ma]

Hi, is there any way to make this less tedious:

example {P : Nat → Prop} {f : Nat → Nat}
    (h1 : 1 ≤ n) (h2 : n ≤ 2)
    (p1 : P 7) (p2 : P 9)
    (f1 : f 1 = 7) (f2 : f 2 = 9):
    ∃ (s : Finset Nat), n ∈ s ∧ s.card = n ∧ P (f n) := by
  interval_cases n
  · use {1}    ; constructor ; trivial ; constructor ; trivial ; rwa [f1]
  · use {1, 2} ; constructor ; trivial ; constructor ; trivial ; rwa [f2]

You can see there is a lot of repetition in the middle (constructor ; trivial ; constructor ; trivial), but they are also surrounded by other commands so I can't use <;> at the start.

[Gareth Ma]

I came up with something like this:

example {P : Nat → Prop} {f : Nat → Nat}
    (h1 : 1 ≤ n) (h2 : n ≤ 2)
    (p1 : P 7) (p2 : P 9)
    (f1 : f 1 = 7) (f2 : f 2 = 9):
    ∃ (s : Finset Nat), n ∈ s ∧ s.card = n ∧ P (f n) := by
  interval_cases n
  use {1}
  rotate_left
  use {1, 2}
  all_goals
    constructor
    trivial
    constructor
    trivial
    simp only [*]

But the rotate_left still feels a bit annoying to use.

[Gareth Ma]

(Sorry if I sound like I am just complaining, I don't mean it that way :D)

[Kyle Miller]

How about this?

import Mathlib.Tactic.IntervalCases
import Mathlib.Data.Finset.Card

set_option autoImplicit true

example {P : Nat → Prop} {f : Nat → Nat}
    (h1 : 1 ≤ n) (h2 : n ≤ 2)
    (p1 : P 7) (p2 : P 9)
    (f1 : f 1 = 7) (f2 : f 2 = 9):
    ∃ (s : Finset Nat), n ∈ s ∧ s.card = n ∧ P (f n) := by
  interval_cases n <;> simp only [f1, f2, p1, p2, and_true]
  · use {1}; simp
  · use {1, 2}; simp

[Gareth Ma]

Ahh that works for this case, but not for my actual use case (I simplified too much :joy:) Let me simplify and share mine real quick

[Kyle Miller]

This is sort of silly, but just to mention this feature you can also use the discharger for use

example {P : Nat → Prop} {f : Nat → Nat}
    (h1 : 1 ≤ n) (h2 : n ≤ 2)
    (p1 : P 7) (p2 : P 9)
    (f1 : f 1 = 7) (f2 : f 2 = 9):
    ∃ (s : Finset Nat), n ∈ s ∧ s.card = n ∧ P (f n) := by
  interval_cases n
  · use (discharger := simp [*]) {1}
  · use (discharger := simp [*]) {1, 2}

The use (discharger := simp [*]) {1} is roughly the same as use {1} <;> simp [*]

[Gareth Ma]

Gareth Ma said:

Ahh that works for this case, but not for my actual use case (I simplified too much :joy:) Let me simplify and share mine real quick

Actually, maybe a better idea is for me to finish my proof in the tedious way, then ask for golfing :)

[Gareth Ma]

It's here. This is quite long, but making it shorter kinda risk losing the idea.
I am trying to prove A11, which asks to construct a $B \subseteq X$ such that some condition holds.
My construction depends on hm1 and hm2 on line 26, but it's always either $B$ or $$B \union \{m\}$$, both of which is always a subset of $X$. As annotated with (1) and (3), there's a lot of repetition in the proof, and I was wondering if that's necessary

[Gareth Ma]

If you don't have time for it, it's fine and not urgent, I just copy and paste a few times for now :D

[Gareth Ma]

Screenshot-2023-10-26-at-20.02.12.png
Here's the proof being formalised, specifically the part with "For each element $x \in X$, ..., this procedure will not change the divisibility condition of $x$".

[Kyle Miller]

A very small thing: if you want to save a constructor here and there, you can do use B' ∪ {m}, ?_, ?_ for example.

[Kyle Miller]

Here's a bit of deduplication:

code

theorem A11 (hX : 0 ∉ X) (hA : A ⊆ X) : ∃ B, B ⊆ X ∧ Pred B X = A := by
  induction' X using ind_min with m X hm hind generalizing A
  · use ∅ ; simp [Pred, subset_empty.mp hA]
  · set A' := A.filter (fun x ↦ x ≠ m) with hA'
    let ⟨B', ⟨hB'₁, hB'₂⟩⟩ := hind A' (by sorry) (by sorry)
    /- We construct B as B' or B' ∪ {m} -/
    rw [Pred] at hB'₂
    have hB' := subset_trans hB'₁ $ subset_cons $ min_not_mem hm
    by_cases hm₁ : m ∈ A <;> by_cases hm₂ : (PredElement B' m)
    · use B', hB'
      /- (2) -/
      simp only [Pred, filter_cons, hm₂, ite_true, hB'₂, disjUnion_eq_union]
      nth_rewrite 2 [←filter_union_filter_neg_eq (fun x => x = m) A]
      congr
      simp only [filter_eq', hm₁, ite_true]
    · use B' ∪ {m}, ?_, ?_
      /- (3) = (1) + (3)' -/
      · apply union_subset hB'
        rw [singleton_subset_iff]
        apply mem_cons_self
      · sorry
    · use B' ∪ {m}, ?_, ?_
      /- (3) = (1) + (3)' -/
      · apply union_subset hB'
        rw [singleton_subset_iff]
        apply mem_cons_self
      · sorry
    · use B', hB'
      /- (2) but with ite_true -> ite_false -/
      simp only [Pred, filter_cons, hm₂, ite_false, hB'₂, disjUnion_eq_union]
      nth_rewrite 2 [←filter_union_filter_neg_eq (fun x => x = m) A]
      congr
      simp only [filter_eq', hm₁, ite_false]

[Kyle Miller]

I'd say don't worry about duplication of tactic scripts, since they mean different things each time. I wouldn't recommend doing this since it makes the proof unreadable, but just to mention it you could use all_goals and first, assuming that sorry really will be the same script between the two cases:

theorem A11 (hX : 0 ∉ X) (hA : A ⊆ X) : ∃ B, B ⊆ X ∧ Pred B X = A := by
  induction' X using ind_min with m X hm hind generalizing A
  · use ∅ ; simp [Pred, subset_empty.mp hA]
  · set A' := A.filter (fun x ↦ x ≠ m) with hA'
    let ⟨B', ⟨hB'₁, hB'₂⟩⟩ := hind A' (by sorry) (by sorry)
    /- We construct B as B' or B' ∪ {m} -/
    rw [Pred] at hB'₂
    have hB' := subset_trans hB'₁ $ subset_cons $ min_not_mem hm
    by_cases hm₁ : m ∈ A <;> by_cases hm₂ : (PredElement B' m)
    all_goals
      first
      | · use B', hB'
          simp only [Pred, filter_cons, hm₂, ite_true, hB'₂, disjUnion_eq_union]
          nth_rewrite 2 [←filter_union_filter_neg_eq (fun x => x = m) A]
          congr
          simp only [filter_eq', hm₁, ite_true]
      | · use B' ∪ {m}, ?_, ?_
          · apply union_subset hB'
            rw [singleton_subset_iff]
            apply mem_cons_self
          · sorry

[Gareth Ma]

Ah, your point about code readability is also true. I will worry less about it then! I will study your code. Thanks!

[Gareth Ma]

I got the final proof, it's pretty terrible :P