Paste: sqrt

Author: haaralld
Mode: haskell
Date: Fri, 3 Apr 2020 09:52:23
Plain Text |
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Data.Bool hiding (_<_; __)

infix 4 _sqrtof_
_sqrtof_ : ℕ → ℕ → Set _
_sqrtof_ x y = (x * x ≤ y) × (y < suc x * suc x)

⌊√_: ℕ → ℕ
⌊√ x ⌋ = f x x
  where
  f : ℕ → ℕ → ℕ
  f 0 _ = 0
  f (suc r) n with (r * r) <ᵇ suc n 
  ...      | true = r
  ...      | false = f r n

thm : ∀ x → ⌊√ x ⌋ sqrtof x
thm = ?

Annotation: jyg

Author: asd
Mode: haskell
Date: Fri, 3 Apr 2020 12:21:33
Plain Text |
thm : ∀ x → ⌊√ x ⌋ sqrtof x
thm 0 = z≤n , s≤s (z≤n)
thm (suc n) = thmˡ , thmʳ
  where
  x : ℕ
  x = ⌊√ suc n ⌋
  y : ℕ
  y = suc n

  ihˡ : ⌊√ n ⌋ * ⌊√ n ⌋ ≤ n
  ihˡ = proj₁ (thm n)

  thmˡ : x * x ≤ y
  thmˡ = ?


  thmʳ : y < suc x * suc x
  thmʳ = ?

New Annotation

Summary:
Author:
Mode:
Body: