## Stream: new members

### Topic: Help/suggestions

#### Newell Jensen (Sep 05 2023 at 18:04):

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 (Sep 05 2023 at 19:23):

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 (Sep 05 2023 at 19:25):

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

#### Newell Jensen (Sep 06 2023 at 05:48):

@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 =>
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))

lemma l2 {a n x : ℕ} (h : n ∣ x) : n ∣ x + n * prod l * (a + 1) := by
match a with
| 0 =>
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))

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
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 (Sep 06 2023 at 05:56):

Good job, nicely done!

Last updated: Dec 20 2023 at 11:08 UTC