How to preserve intermediate results

Stream: lean4

[Stuart Geipel]

Hey everyone, I am learning Lean. I wrote a simple loop to find the sqrt of a number:

def is_sqrt (n r : Nat) := n ∈ [r^2 : (r+1)^2]

-- used because Exists hides the witness
structure Sqrt (n : Nat) where
  r : Nat
  is_valid : is_sqrt n r

def sqrt' (n i : Nat) (le : i^2 ≤ n) : Sqrt n :=
  sorry -- recursive - details not relevant
def sqrt (n : Nat) :=
  let ⟨r, _⟩ := sqrt' n 0 (by simp)
  r

theorem sqrt_valid (n r: Nat) (h : r = sqrt n) : is_sqrt n r := by
  rw [sqrt] at h
  -- how to extract is_valid from inside the match here?
  sorry

I'm returning a Sqrt (which has the result and proof of correctness) from the helper sqrt'. I use that in sqrt which just returns the Nat and then try to conventionally prove it with sqrt_valid, but I'm not sure how. Two questions:

1. How can I "extract" the is_valid Prop before sqrt throws it away for my sqrt_valid proof?
2. Is it considered bad practice to mix the program and the proof like I did in the signature of sqrt'?

[Marcus Rossel]

You could do something like this:

def IsSqrt (n r : Nat) := n ∈ [r^2 : (r+1)^2]

def sqrt' (n i : Nat) (le : i^2 ≤ n) : { r // IsSqrt n r } :=
  sorry -- recursive - details not relevant

def sqrt (n : Nat) := sqrt' n 0 (Nat.zero_le n) |>.val

theorem IsSqrt.sqrt (n : Nat) : IsSqrt n (sqrt n) := by
  rw [sqrt]
  exact (sqrt' n 0 _).property

Note that I renamed is_sqrt to IsSqrt (as Lean 4 convention is to use UpperCamelCase for propositions) and replaced your Sqrt type with the subtype { r // IsSqrt n r }.

Generally I wouldn't say that it's bad practice to mix programs and proofs like this. Though in this case it feels kind of awkward to have sqrt wrapping sqrt' like that. Also, separating programs and proofs to some degree can help with avoiding "dependent type hell".

[Stuart Geipel]

This is really helpful, thank you! Subtype was what I was actually looking for.
Something I realized from this was, you don't have to find a "reference" to the .property from the original invocation of sqrt. You can just invoke it again as sqrt' n, it's taking in the same n as a parameter, so the result will be definitionally equal for exact. (Like, n is a sort of unique "binding", although I'm still wrapping my head around exactly what that means lol)