Library hydras.solutions_exercises.isqrt
From hydras Require Import primRec extEqualNat ssrnat_extracts.
From Coq Require Import Min ArithRing Lia Compare_dec Arith Lia.
Returns smallest value of x less or equal than b such that (P b x).
Otherwise returns b
Check boundedSearch.
Search boundedSearch.
Lemma boundedSearch3 :
∀ (P : naryRel 2) (b : nat), boundedSearch P b ≤ b.
Lemma boundedSearch4 :
∀ (P : naryRel 2) (b : nat),
P b b = true →
P b (boundedSearch P b) = true.
Definition isqrt_spec n r := r × r ≤ n < r.+1 × r.+1.
Section sqrtIsPR.
Let P (n r: nat) := Nat.ltb n (S r × S r).
Definition isqrt := boundedSearch P.
Section Proof_isqrt.
Variable n: nat.
Remark R00 : P n (isqrt n) = true.
Lemma R01 : n < (isqrt n).+1 × (isqrt n).+1.
Lemma R02 : isqrt n × isqrt n ≤ n.
End Proof_isqrt.
Lemma sqrt_correct (n: nat) : isqrt_spec n (isqrt n).
#[export] Instance issqrtIsPR : isPR 1 isqrt.
End sqrtIsPR.
Search boundedSearch.
Lemma boundedSearch3 :
∀ (P : naryRel 2) (b : nat), boundedSearch P b ≤ b.
Lemma boundedSearch4 :
∀ (P : naryRel 2) (b : nat),
P b b = true →
P b (boundedSearch P b) = true.
Definition isqrt_spec n r := r × r ≤ n < r.+1 × r.+1.
Section sqrtIsPR.
Let P (n r: nat) := Nat.ltb n (S r × S r).
Definition isqrt := boundedSearch P.
Section Proof_isqrt.
Variable n: nat.
Remark R00 : P n (isqrt n) = true.
Lemma R01 : n < (isqrt n).+1 × (isqrt n).+1.
Lemma R02 : isqrt n × isqrt n ≤ n.
End Proof_isqrt.
Lemma sqrt_correct (n: nat) : isqrt_spec n (isqrt n).
#[export] Instance issqrtIsPR : isPR 1 isqrt.
End sqrtIsPR.
Extra work :
Define a faster implementation of sqrt_spec, and prove your function is
extensionnaly equal to isqrt (hence PR!)