Initial introduction of Legendre Symbol

diff --git a/numbertheory.txt b/numbertheory.txt
index db634d8..11702c3 100644 (file)
--- a/numbertheory.txt
+++ b/numbertheory.txt
@@ -4,10 +4,11 @@ val N: ℕ;
 val M: ℕ;
 val K: ℕ;
 
-type Base   = ℕ[N];
-type Exp    = ℕ[M];
-type Result = ℕ[N^M];
-type nat    = ℕ[K];
+type Base    = ℕ[N];
+type Exp     = ℕ[M];
+type Result  = ℕ[N^M];
+type nat     = ℕ[K];
+type integer = ℤ[-K,K];
 
 // Elementary division
 pred divides(m:nat,n:nat) ⇔ ∃p:nat. m*p = n;
@@ -98,8 +99,28 @@ proc isquadraticresidue(a:nat,p:nat): Bool
 // ==  0   divides(p,a)
 // ==  1   a is quadratic residue modulo p
 // == -1   a is NOT quadratic residue modulo p
+// ==  2   if p is not prime
 ////////////////////////////////////////////////////////////////////
+proc legendre(a:nat,p:nat): integer
+   ensures (((result =  0) ∧ divides(p,a)) ∨
+            ((result =  1) ∧ isquadraticresidue(p,a)) ∨
+            ((result = -1) ∧ ~isquadraticresidue(p,a)) ∨
+            ((result =  2) ∧ ~isprime(p)));
+{
+   var res:integer = 0;
 
+   if isprime(p) then
+      if divides(p,a) then
+         res = 0;
+      else if isquadraticresidue(p,a) then
+         res = 1;
+      else
+         res = -1;
+   else
+      res = 2;
+
+   return res;
+}
 
 ////////////////////////////////////////////////////////////////////
 // Algorithm: Calculate x^n by Right-To-Left Exponentation
@@ -131,7 +152,7 @@ proc xpowern(x:Base,n:Exp): Result
   ensures result = x^n;
 {
    var res:Result = 1;
-   var i:Nat[M+1] = 0;
+   var i:ℕ[M+1] = 0;
    while i < n do
      invariant 0 ≤ i ∧ i ≤ n ∧ res = x^i;
      decreases n-i+1;