Commit 056832f1 authored by MARCHE Claude's avatar MARCHE Claude

Example hamming_sequence in progress + realization of number.Coprime

parent e25459b0
......@@ -839,7 +839,7 @@ COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES))
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
......
......@@ -14,34 +14,75 @@ module HammingSequence
use import int.Int
use import int.MinMax
use import number.Divisibility
use import number.Prime
use import number.Coprime (* for Euclid's lemma *)
function hamming (n:int) : int
predicate is_hamming (n:int) =
forall d:int. prime d /\ divides d n -> d = 2 \/ d = 3 \/ d = 5
lemma is_hamming_times2 :
forall n:int. n >= 1 -> is_hamming n -> is_hamming (2*n)
lemma is_hamming_times3 :
forall n:int. n >= 1 -> is_hamming n -> is_hamming (3*n)
lemma is_hamming_times5 :
forall n:int. n >= 1 -> is_hamming n -> is_hamming (5*n)
use import array.Array
use import ref.Ref
let hamming (n:int) : array int
requires { n >= 1 }
ensures { forall k:int. 0 <= k < n -> result[k] = hamming k }
ensures { forall k:int. 0 <= k < n -> is_hamming result[k] }
ensures { forall k:int. 0 < k < n -> result[k-1] < result[k] }
ensures { forall k m:int. 0 < k < n ->
result[k-1] < m < result[k] -> not (is_hamming m) }
= let t = make n 0 in
t[0] <- 1;
let x2 = ref 2 in let j2 = ref 0 in
let x3 = ref 3 in let j3 = ref 0 in
let x5 = ref 5 in let j5 = ref 0 in
for i=0 to n-1 do
invariant {
!x2 = 2*t[!j2] /\
!x3 = 3*t[!j3] /\
!x5 = 5*t[!j5] /\
!x2 > t[i] /\
!x3 > t[i] /\
!x5 > t[i]
}
for i=1 to n-1 do
invariant { forall k:int. 0 <= k < i -> t[k] > 0 }
invariant { forall k:int. 0 < k < i -> t[k-1] < t[k] }
invariant { forall k:int. 0 <= k < i -> is_hamming t[k] }
invariant { 0 <= !j2 < i }
invariant { 0 <= !j3 < i }
invariant { 0 <= !j5 < i }
invariant { !x2 = 2*t[!j2] }
invariant { !x3 = 3*t[!j3] }
invariant { !x5 = 5*t[!j5] }
invariant { !x2 > t[i-1] }
invariant { !x3 > t[i-1] }
invariant { !x5 > t[i-1] }
let next = min !x2 (min !x3 !x5) in
t[i] <- next;
while !x2 <= next do j2 := !j2+1; x2 := 2*t[!j2] done;
while !x3 <= next do j3 := !j3+1; x3 := 3*t[!j3] done;
while !x5 <= next do j5 := !j5+1; x5 := 5*t[!j5] done
while !x2 <= next do
invariant { 0 <= !j2 <= i }
invariant { !x2 = 2*t[!j2] }
variant { next - !x2 }
assert { !j2 < i };
j2 := !j2+1; x2 := 2*t[!j2]
done;
while !x3 <= next do
invariant { 0 <= !j3 <= i }
invariant { !x3 = 3*t[!j3] }
variant { next - !x3 }
assert { !j3 < i };
j3 := !j3+1; x3 := 3*t[!j3]
done;
while !x5 <= next do
invariant { 0 <= !j5 <= i }
invariant { !x5 = 5*t[!j5] }
variant { next - !x5 }
assert { !j5 < i };
j5 := !j5+1; x5 := 5*t[!j5]
done
done;
t
let test () = hamming 30
end
......@@ -430,6 +430,10 @@ let built_in_theories =
"infix >", None, eval_int_rel Big_int.gt_big_int;
"infix >=", None, eval_int_rel Big_int.ge_big_int;
] ;
["int"],"MinMax", [],
[ "min", None, eval_int_op Big_int.min_big_int;
"max", None, eval_int_op Big_int.max_big_int;
] ;
["int"],"ComputerDivision", [],
[ "div", None, eval_int_op computer_div_big_int;
"mod", None, eval_int_op computer_mod_big_int;
......
......@@ -189,4 +189,12 @@ theory Coprime
forall p: int.
prime p <-> 2 <= p && forall n:int. 1 <= n < p -> coprime n p
lemma Gauss:
forall a b c:int. divides a (b*c) /\ coprime a b -> divides a c
lemma Euclid:
forall p a b:int.
prime p /\ divides p (a*b) -> divides p a \/ divides p b
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment