Skip to content

Commit

Permalink
Changes of examples/{AKS|fermat|simple_complexity} after src/algebra/…
Browse files Browse the repository at this point in the history 
…monoidThoery
  • Loading branch information
@binghe
binghe committed Apr 21, 2024
1 parent 6bd26f3 commit d9c4303
Show file tree
Hide file tree
Showing 68 changed files with 273 additions and 5,455 deletions.
4 changes: 1 addition & 3 deletions examples/AKS/compute/Holmakefile
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,2 @@
PRE_INCLUDES = ../../algebra/ring

ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield
ALGEBRA_INCLUDES = group ring field polynomial finitefield
INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES))
24 changes: 3 additions & 21 deletions examples/AKS/compute/computeAKSScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,12 @@ val _ = new_theory "computeAKS";

(* ------------------------------------------------------------------------- *)


(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
dividesTheory gcdTheory primeTheory;

(* Get dependent theories local *)
(* val _ = load "computeParamTheory"; *)
Expand All @@ -29,27 +30,8 @@ open computeRingTheory computePolyTheory;
open polyWeakTheory polyRingTheory;
open polyMonicTheory polyDivisionTheory;

(*
open helperFunctionTheory; (* for SQRT_LE *)
open logPowerTheory; (* for ulog *)
open ringTheory ringInstancesTheory; (* for ZN_coprime_order_alt *)
open monoidOrderTheory;
*)
open ringInstancesTheory; (* for ZN_ring *)

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
open helperNumTheory helperSetTheory;

(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory;
(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;
open logPowerTheory;


(* ------------------------------------------------------------------------- *)
(* AKS Computations Documentation *)
(* ------------------------------------------------------------------------- *)
Expand Down
30 changes: 5 additions & 25 deletions examples/AKS/compute/computeBasicScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,38 +12,18 @@ val _ = new_theory "computeBasic";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *)
(* val _ = load "logPowerTheory"; *)
open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory;
open pred_setTheory listTheory arithmeticTheory;

open logPowerTheory; (* for LOG2, SQRT, and Perfect Power, Power Free *)
open logrootTheory;

(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;

(* val _ = load "GaussTheory"; *)
open EulerTheory;
open GaussTheory;
open pred_setTheory listTheory arithmeticTheory logrootTheory dividesTheory
gcdTheory gcdsetTheory numberTheory combinatoricsTheory primeTheory;

(* val _ = load "whileTheory"; *)
open whileTheory;

val _ = temp_overload_on("SQ", ``\n. n * n``);
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
val _ = temp_overload_on("TWICE", ``\n. 2 * n``);

(* ------------------------------------------------------------------------- *)
(* Basic Computations Documentation *)
Expand Down
32 changes: 2 additions & 30 deletions examples/AKS/compute/computeOrderScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,46 +12,18 @@ val _ = new_theory "computeOrder";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)

(* open dependent theories *)
(* val _ = load "fieldInstancesTheory"; *)
open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
dividesTheory gcdTheory logrootTheory primeTheory;

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *)
open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory;
open pred_setTheory listTheory arithmeticTheory;

(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;

(* val _ = load "fieldInstancesTheory"; *)
open monoidInstancesTheory;
open groupInstancesTheory;
open ringInstancesTheory;
open fieldInstancesTheory;
open groupOrderTheory;
open monoidOrderTheory;

(* val _ = load "GaussTheory"; *)
open EulerTheory;
open GaussTheory;

(* val _ = load "computeBasicTheory"; *)
open computeBasicTheory;
open logrootTheory logPowerTheory;


(* ------------------------------------------------------------------------- *)
(* Order Computations Documentation *)
Expand Down
26 changes: 6 additions & 20 deletions examples/AKS/compute/computeParamScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,26 +14,17 @@ val _ = new_theory "computeParam";

open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory
dividesTheory gcdTheory numberTheory combinatoricsTheory primeTheory;

(* Get dependent theories local *)
open computeOrderTheory;
open helperFunctionTheory; (* for SQRT_LE *)
open logPowerTheory; (* for ulog *)
open ringTheory ringInstancesTheory; (* for ZN_coprime_order_alt *)
open monoidOrderTheory;

(* Get dependent theories in lib *)
open helperNumTheory helperSetTheory;

(* open dependent theories *)
open prim_recTheory pred_setTheory listTheory arithmeticTheory;
open dividesTheory gcdTheory;

open GaussTheory; (* for phi_pos *)
open EulerTheory; (* for residue_def *)
open triangleTheory; (* for list_lcm_pos *)
open monoidTheory;

val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
val _ = temp_overload_on("TWICE", ``\n. 2 * n``);

(* ------------------------------------------------------------------------- *)
(* AKS Parameter Documentation *)
Expand Down Expand Up @@ -67,7 +58,6 @@ open triangleTheory; (* for list_lcm_pos *)
coprime_candidates_ne_1 |- !n m. 1 < m ==> 1 NOTIN coprime_candidates n m
ZN_order_good_enough |- !n m. 1 < n /\ 1 < m ==> ?k. 1 < k /\ coprime k n /\ m <= ordz k n
Smallest Candidate
least_prime_candidates_property |- !n m. 1 < n /\ 0 < m ==> !h. prime h /\ coprime h n /\
h < MIN_SET (prime_candidates n m) ==>
Expand Down Expand Up @@ -278,10 +268,6 @@ open triangleTheory; (* for list_lcm_pos *)
param_good_range |- !n k. (param n = good k) ==> 1 < n /\ 1 < k /\ k < n
*)

(* ------------------------------------------------------------------------- *)
(* Helper Theorems *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* AKS Parameter *)
(* ------------------------------------------------------------------------- *)
Expand Down
29 changes: 5 additions & 24 deletions examples/AKS/compute/computePolyScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,27 +12,11 @@ val _ = new_theory "computePoly";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)

(* open dependent theories *)
(* val _ = load "fieldInstancesTheory"; *)

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
open helperNumTheory helperSetTheory helperListTheory;
open pred_setTheory listTheory arithmeticTheory;

(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;
open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory
combinatoricsTheory dividesTheory gcdTheory logrootTheory whileTheory;

(* val _ = load "polyFieldModuloTheory"; *)
open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
Expand All @@ -46,13 +30,10 @@ open ringBinomialTheory;

(* val _ = load "computeOrderTheory"; *)
open computeBasicTheory computeOrderTheory;
open logrootTheory logPowerTheory;

(* val _ = load "whileTheory"; *)
open whileTheory;

open rich_listTheory; (* for FRONT and LAST *)

val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
val _ = temp_overload_on("TWICE", ``\n. 2 * n``);

(* ------------------------------------------------------------------------- *)
(* Polynomial Computations Documentation *)
Expand Down
33 changes: 5 additions & 28 deletions examples/AKS/compute/computeRingScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,34 +12,11 @@ val _ = new_theory "computeRing";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)

(* open dependent theories *)
(* val _ = load "fieldInstancesTheory"; *)

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
open helperNumTheory helperSetTheory helperListTheory;
open pred_setTheory listTheory arithmeticTheory;

(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;

(*
polyBinomial.hol polyEval.hol polyGCD.hol polyRing.hol
polyDerivative.hol polyField.hol polyIrreducible.hol polyRoot.hol
polyDivides.hol polyFieldDivision.hol polyMonic.hol polyWeak.hol
polyDivision.hol polyFieldModulo.hol polyProduct.hol polynomial.hol
*)
open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory
combinatoricsTheory dividesTheory gcdTheory logrootTheory;

(* val _ = load "polyFieldModuloTheory"; *)
open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
Expand All @@ -53,11 +30,11 @@ open ringBinomialTheory;

(* val _ = load "computePolyTheory"; *)
open computeBasicTheory computeOrderTheory computePolyTheory;
open logrootTheory logPowerTheory;

open ringInstancesTheory;
open rich_listTheory; (* for FRONT and LAST *)

val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
val _ = temp_overload_on("TWICE", ``\n. 2 * n``);

(* ------------------------------------------------------------------------- *)
(* Modulo Polynomial Computations in (ZN n) Ring Documentation *)
Expand Down
4 changes: 1 addition & 3 deletions examples/AKS/machine/Holmakefile
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
PRE_INCLUDES = ../../algebra/ring

ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield
ALGEBRA_INCLUDES = group ring field polynomial finitefield
INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES)) \
../../simple_complexity/lib ../../simple_complexity/loop ../compute \
$(HOLDIR)/src/monad/more_monads
27 changes: 6 additions & 21 deletions examples/AKS/machine/countAKSScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ val _ = new_theory "countAKS";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory
rich_listTheory listRangeTheory numberTheory combinatoricsTheory
logrootTheory pairTheory optionTheory primeTheory;

(* Get dependent theories local *)
(* val _ = load "countParamTheory"; *)
Expand All @@ -35,29 +35,11 @@ open bitsizeTheory complexityTheory;
open loopIncreaseTheory loopDecreaseTheory;
open loopDivideTheory loopListTheory;

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
open helperNumTheory helperSetTheory helperListTheory;
open helperFunctionTheory;

(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open pred_setTheory listTheory arithmeticTheory;
open dividesTheory gcdTheory;
open rich_listTheory listRangeTheory;

(* (* val _ = load "logPowerTheory"; *) *)
open logrootTheory logPowerTheory;

(* (* val _ = load "monadsyntax"; *) *)
open monadsyntax;
open pairTheory optionTheory;

(* val _ = load "ringInstancesTheory"; *)
open ringInstancesTheory; (* for ZN order *)

(* val _ = load "computeAKSTheory"; *)
open computeParamTheory computeAKSTheory;
open computeBasicTheory; (* for power_free_check_eqn *)

Expand All @@ -70,6 +52,9 @@ open polynomialTheory polyWeakTheory;
val _ = monadsyntax.enable_monadsyntax();
val _ = monadsyntax.enable_monad "Count";

val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
val _ = temp_overload_on("TWICE", ``\n. 2 * n``);

(* ------------------------------------------------------------------------- *)
(* AKS computations in monadic style Documentation *)
Expand Down
Loading

0 comments on commit d9c4303

Please sign in to comment.