Help/suggestions

Stream: new members

[Newell Jensen]

I am stuck at a certain part of a proof and can't figure out how to get past this:

import Mathlib.Tactic

open List

-- Uncomment to test different values
-- #eval (fun a n l =>  map (fun x => decide (n ∣ x) || List.any l fun b => decide (b ∣ x)) (range' (1 + n * prod l * (a + 1)) (n * prod l)) = map (fun x => decide (n ∣ x) || List.any l fun b => decide (b ∣ x)) (range' 1 (n * prod l))) 0 0 []

lemma foo (a n : ℕ) (l : List ℕ)
    : map (fun x => decide (n ∣ x) || List.any l fun b => decide (b ∣ x))
      (range' (1 + n * prod l * (a + 1)) (n * prod l)) =
      map (fun x => decide (n ∣ x) || List.any l fun b => decide (b ∣ x))
      (range' 1 (n * prod l)) := by
  sorry

Now, I believe this to be true since n and any element of l will be a factor in n * prod l and therefore both the range's will give the same pattern from what I can see due to the fact that each factor will show up in these range's at prescribed locations due to their multiples within this range. I don't know how to show this though in a concrete way (by concrete I mean I don't know exactly what the pattern of true and falses will be in the resulting list since l is arbitrary) but I believe this to be a true statement that should be able to be proved and wondering if anyone has any ideas on how to break up the form of this statement into something that can actually show this?

It might be obvious but I am just not seeing how to progress from here due to my ignorance. I have tried many different approaches such as using zipWith (or \. \. ) to try and overlay the different patterns but either I messed up somehow or this wasn't the right approach. Please someone enlighten me and save me from banging my head on this for any longer :upside_down: :working_on_it:

I am not looking for anyone to fill in the proof but if anyone has a good idea about how to potentially progress from here in the right direction, that would be greatly appreciated. Currently I am trying to see if there is a way to write some lemmas of list membership in a form that I could use to progress from the above position but at this point I am just trying to throw the kitchen sink at the problem instead of knowing what should be done.

[Tomas Skrivan]

What about spiting it up like this?

def bar (n : ℕ) (l : List ℕ) (x : ℕ) := decide (n ∣ x) || List.any l fun b => decide (b ∣ x)

theorem bar_identity (n : ℕ) (l : List ℕ)
  : ∀ a x, bar n l x = bar n l (x +  n * prod l * (a + 1)) :=
by
  sorry

theorem list_map_shift {α}
  (f : ℕ → α) (c : ℕ) (hf : ∀ x, f x = f (x + c))
  (l : List ℕ) (start step : ℕ)
  : map f (range' start step) = map f (range' (start + c) step) := sorry


theorem foo' (a n : ℕ) (l : List ℕ)
  : map (bar n l) (range' 1 (n * prod l))
    =
    map (bar n l) (range' (1 + n * prod l * (a + 1)) (n * prod l)) :=
by
  apply list_map_shift (bar n l) (n * prod l * (a + 1)) (bar_identity n l a) l 1 (n * prod l)

both bar_identity and list_map_shift should be provable

[Newell Jensen]

Thanks Tomas, will try that. I appreciate the feedback.

[Newell Jensen]

@Tomas Skrivan Took me a bit to get it but thanks again for the hint. Cheers.

import Mathlib.Tactic

open List Function

def bar (n : ℕ) (l : List ℕ) (x : ℕ) := decide (n ∣ x) || List.any l fun b => decide (b ∣ x)

lemma l1 {a n x : ℕ} {l : List ℕ} (h : n ∣ x + n * prod l * (a + 1)) : n ∣ x := by
  match a with
  | 0 =>
    rw [zero_add, mul_one] at h
    exact Iff.mp (Nat.dvd_add_left <| Nat.dvd_mul_right n (prod l)) h
  | a + 1 =>
    have h1 : n ∣ n * prod l * (a + 1 + 1) := by
      rw [mul_assoc]
      exact Nat.dvd_mul_right n (prod l * (a + 1 + 1))
    exact Iff.mp (Nat.dvd_add_left h1) h

lemma l2 {a n x : ℕ} (h : n ∣ x) : n ∣ x + n * prod l * (a + 1) := by
  match a with
  | 0 =>
    rw [zero_add, mul_one]
    exact Nat.dvd_add h <| Nat.dvd_mul_right n (prod l)
  | a + 1 =>
    have h1 : n ∣ n * prod l * (a + 1 + 1) := by
      rw [mul_assoc]
      exact Nat.dvd_mul_right n (prod l * (a + 1 + 1))
    exact Nat.dvd_add h h1

lemma l3 (a n x : ℕ) (l : List ℕ)
    : decide (n ∣ x + n * prod l * (a + 1)) ↔ decide (n ∣ x) := by
  constructor
  · intro h
    simp only [decide_eq_true_eq] at *
    exact l1 h
  · intro h
    simp only [decide_eq_true_eq] at *
    exact l2 h

lemma l4 (a n x : ℕ) (l : List ℕ)
    : decide (n ∣ x + n * prod l * (a + 1)) = decide (n ∣ x) := by
  have h1 := l3 a n x l
  simp at *
  exact h1

lemma l5 (a n x : ℕ) (l : List ℕ) (h : (any l fun b => decide (b ∣ x + n * prod l * (a + 1))))
    : (any l fun b => decide (b ∣ x)) := by
  simp only [Nat.isUnit_iff, any_eq_true, decide_eq_true_eq] at h
  obtain ⟨b, hb, hbd⟩ := h
  simp; use b
  exact ⟨hb, Iff.mp (Nat.dvd_add_left (Dvd.dvd.mul_right (Dvd.dvd.mul_left (dvd_prod hb) n) (a + 1))) hbd⟩

lemma l6 (a n x : ℕ) (l : List ℕ) (h : (any l fun b => decide (b ∣ x)))
    : (any l fun b => decide (b ∣ x + n * prod l * (a + 1))) := by
  simp at *
  obtain ⟨b, hb, hbd⟩ := h
  use b
  exact ⟨hb, Nat.dvd_add hbd <| Dvd.dvd.mul_right (Dvd.dvd.mul_left (dvd_prod hb) n) (a + 1)⟩

lemma l7 (a n x : ℕ) (l : List ℕ)
    : (any l fun b => decide (b ∣ x + n * prod l * (a + 1))) ↔ (any l fun b => decide (b ∣ x)) :=
  ⟨fun h => l5 a n x l h, fun h => l6 a n x l h⟩

lemma l8 (a n x : ℕ) (l : List ℕ)
    : (any l fun b => decide (b ∣ x + n * prod l * (a + 1))) = (any l fun b => decide (b ∣ x)) := by
  have h := l7 a n x l
  exact Iff.mpr Bool.eq_iff_iff h

theorem bar_identity (n : ℕ) (l : List ℕ)
    : ∀ a x, bar n l (x + n * prod l * (a + 1)) = bar n l x := by
  intro a x
  simp_rw [bar]
  have h1 := l4 a n x l
  simp_rw [h1]
  have h2 := l8 a n x l
  rw [h2]

theorem list_map_shift {α} (f : ℕ → α) (c : ℕ) (hf : ∀ x, f (x + c) = f x) (l : List ℕ) (start step : ℕ)
    :  map f (range' (start + c) step) = map f (range' start step) := by
  match step with
  | 0 => simp
  | s + 1 =>
    simp
    constructor
    · specialize hf start
      exact hf
    · have ih := list_map_shift f c hf l (start + 1) s
      rw [add_assoc, add_comm c 1, ← add_assoc]
      exact ih

theorem foo' (a n : ℕ) (l : List ℕ)
  : map (bar n l) (range' (1 + n * prod l * (a + 1)) (n * prod l)) =
    map (bar n l) (range' 1 (n * prod l)) := by
  exact list_map_shift (bar n l) (n * prod l * (a + 1)) (bar_identity n l a) l 1 (n * prod l)

[Tomas Skrivan]

Good job, nicely done!