Skip to content

Instantly share code, notes, and snippets.

@gaxiiiiiiiiiiii
Created January 9, 2024 13:35
Show Gist options
  • Save gaxiiiiiiiiiiii/9331f4b598b5cd72220cd1dbb3d5fe88 to your computer and use it in GitHub Desktop.
Save gaxiiiiiiiiiiii/9331f4b598b5cd72220cd1dbb3d5fe88 to your computer and use it in GitHub Desktop.
function Pow(n:nat, k:nat) : (r:nat)
ensures n > 0 ==> r > 0
{
if k == 0 then 1
else if k == 1 then n
else
var p := k / 2;
var np := Pow(n,p);
if p*2 == k then np * np
else
np * np * n
}
lemma mul_assoc (x : nat, y : nat, z : nat)
ensures x * y * z == x * (y * z)
{}
lemma mul_comm (x : nat, y : nat)
ensures x * y == y * x
{}
lemma LemmaPow (n : nat, k : nat)
ensures Pow(n, k + 2) == n * n * Pow(n, k)
ensures Pow(n, k + 1) == n * Pow(n, k)
{
if k == 0 {}
else {
assert H0 : Pow(n,k) == n * Pow(n, k - 1) by {LemmaPow(n, k-1); }
calc {
Pow(n, k+1);
== {LemmaPow(n, k-1);}
n * n * Pow(n,k-1);
== {mul_assoc(n,n,Pow(n,k-1));}
n * (n * Pow(n,k-1));
== {reveal H0;}
n * Pow(n,k);
}
var x := Pow(n,k/2);
assert k/2 < k;
assert H1 : Pow(n, k/2 + 1) == n * x by {LemmaPow(n, k/2);}
if k % 2 == 0 {
assert H2 : Pow(n, k) == x * x;
calc {
Pow(n, k + 2);
==
Pow(n, k/2 + 1) * Pow(n, k/2 + 1) ;
== {reveal H1;}
(n * x) * (n * x);
== {mul_assoc((n * x), n, x);}
(n * x * n) * x;
== {mul_assoc(n,x,n);}
(n * (x * n)) * x;
== {mul_comm(x,n);}
(n * (n * x)) * x;
== {mul_assoc(n,n,x);}
((n * n) * x) * x;
== {mul_assoc(n * n, x, x);}
n * n * (x * x);
== {reveal H2;}
n * n * Pow(n,k);
}
} else {
assert H2 : Pow(n, k) == x * x * n;
calc {
Pow(n, k+2);
==
Pow(n,k/2 + 1) * Pow(n,k/2 + 1) * n;
== {reveal H1;}
(n * x) * (n * x) * n;
== {mul_assoc(n*x, n*x, n);}
((n * x) * (n * x)) * n;
== {mul_comm((n*x) * (n*x) ,n);}
n * ((n*x) * (n*x));
== {mul_assoc(n, x, n*x);}
n * (n * (x * (n * x)));
== {mul_comm(n,x);}
n * (n * (x * (x * n)));
== {mul_assoc(x,x,n);}
n * (n * (x * x * n));
== {reveal H2;}
n * (n * Pow(n,k));
== {mul_assoc(n,n,Pow(n,k));}
n * n * Pow(n,k);
}
}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment