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 = ?
| 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