about the sigma type mismatch

Stream: new members

[Isaac Li]

Probably a dumb question:

-- current i, prime list primes, sieve f
-- linear sieve from i to n
def linearSieveAux (n i : Nat) (ps : List Nat) (f : Nat → Nat)
  (hi : 2 ≤ i) (hiub : i ≤ n + 1)
  (hps : list_sorted ps)
  (hinps₁ : ∀ x ∈ ps, x < i) (hinps₂ : ∀ x ∈ ps, 2 ≤ x) :
  (Nat → Nat) × { l : List Nat // (list_sorted l) ∧ (∀ x, x ∈ l → 2 ≤ x ∧ x ≤ n) } :=
if heq : i = n + 1 then
  have hinps' : ∀ x, x ∈ ps → 2 ≤ x ∧ x ≤ n := by
    intros x hx
    constructor
    · exact hinps₂ x hx
    · have h : x ≤ i - 1 := by
        apply Nat.lt_succ_iff.mp
        aesop
      rw [heq] at h
      exact h
  (f, ⟨ps, hps, hinps'⟩) -- end of recursion
--rest of the code

I defined this funcition and it returns (f, ⟨ps, hps, hinps'⟩), everything is just fine.
but when I want to record the output of linearSieveAux, something went wrong:

lemma linearSieveAux_preserves {n : Nat} {f : Nat → Nat} {ps : List Nat}
  (hn : 2 ≤ n) (hi : 2 ≤ i) (hiub : i ≤ n + 1) (hge: ∀ prime ∈ ps, 2 ≤ prime)
  (hps: list_sorted ps) (hinps₁ : ∀ x ∈ ps, x < i) (hinps₂ : ∀ x ∈ ps, 2 ≤ x)
  /-
  application type mismatch
    ⟨hps', hinps'⟩
  argument
    hinps'
  has type
    ?m.454529 : Sort ?u.454528
  but is expected to have type
    ∀ x ∈ ps', 2 ≤ x ∧ x ≤ n : Prop
  -/
  (hpre : linearSieveAux n i ps f hi hiub hps hinps₁ hinps₂ = (f', ⟨ps', hps', hinps'⟩)) :
  linearSieveAux (n + 1) i ps f hi (by linarith) hps hinps₁ hinps₂ =
  linearSieveAux (n + 1) (n + 1) ps' f' (by linarith) (by linarith) hps' (sorry) (sorry):= by
  sorry

I know I should attach a mwe but I havent quite figure out how to minimize my work, so I just upload my full file. I am a beginner and i am truely sorry for that :smiling_face_with_tear:
linear sieve.lean

[Kyle Miller]

My best guess is that hinps' is not defined

[Isaac Li]

But how should I define it here? I want to use it to simplify the goal statement, or else the lemma will be a mess like this:

-- linearSieveAux preserves states
lemma linearSieveAux_preserves {n : Nat} {f : Nat → Nat} {ps : List Nat}
  (hn : 2 ≤ n) (hi : 2 ≤ i) (hiub : i ≤ n + 1) (hge: ∀ prime ∈ ps, 2 ≤ prime)
  (hps: list_sorted ps) (hinps₁ : ∀ x ∈ ps, x < i) (hinps₂ : ∀ x ∈ ps, 2 ≤ x):
  linearSieveAux (n + 1) i ps f hi (by linarith) hps hinps₁ hinps₂ =
  linearSieveAux (n + 1) (n + 1) (linearSieveAux n i ps f hi hiub hps hinps₁ hinps₂).2.1 (linearSieveAux n i ps f hi hiub hps hinps₁ hinps₂).1
   (by linarith) (by linarith) (linearSieveAux n i ps f hi hiub hps hinps₁ hinps₂).2.2.left (fun x hx => Nat.lt_of_le_of_lt (((linearSieveAux n i ps f hi hiub hps hinps₁ hinps₂).2.2.right) x hx).right (Nat.lt_succ_self n))
    (fun x hx => (((linearSieveAux n i ps f hi hiub hps hinps₁ hinps₂).2.2.right) x hx).left)
  := by
  sorry

[Kyle Miller]

I would add an argument like (hinps' : ∀ x ∈ ps', 2 ≤ x ∧ x ≤ n)