Skip to content

Commit

Permalink
More fixes to multiple-rebinds of theorems under same name
Browse files Browse the repository at this point in the history
  • Loading branch information
@mn200
mn200 committed Sep 17, 2023
1 parent b404802 commit 58d0603
Show file tree
Hide file tree
Showing 4 changed files with 82 additions and 138 deletions.
39 changes: 21 additions & 18 deletions examples/AKS/compute/computeBasicScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -972,32 +972,35 @@ val exp_mod_binary_eqn = store_thm(
= (a ** (2 * HALF n + 1)) MOD m by arithmetic
= (a ** n) MOD m by ODD_HALF
*)
val exp_mod_binary_eqn = store_thm(
"exp_mod_binary_eqn",
``!m n a. exp_mod_binary a n m = (a ** n) MOD m``,
Theorem exp_mod_binary_eqn[allow_rebind]:
!m n a. exp_mod_binary a n m = (a ** n) MOD m
Proof
ntac 2 strip_tac >>
Cases_on `m = 0` >-
Cases_on ‘m = 0’ >-
rw[Once exp_mod_binary_def] >>
Cases_on `m = 1` >-
Cases_on ‘m = 1’ >-
rw[Once exp_mod_binary_def] >>
`1 < m /\ 0 < m` by decide_tac >>
completeInduct_on `n` >>
‘1 < m /\ 0 < m’ by decide_tac >>
completeInduct_on ‘n’ >>
rpt strip_tac >>
Cases_on `n = 0` >-
Cases_on ‘n = 0’ >-
rw[exp_mod_binary_0, EXP] >>
`0 < m` by decide_tac >>
`HALF n < n` by rw[HALF_LT] >>
‘0 < m’ by decide_tac >>
‘HALF n < n’ by rw[HALF_LT] >>
rw[Once exp_mod_binary_def] >| [
`((a ** 2) ** HALF n) MOD m = (a ** (2 * HALF n)) MOD m` by rw[EXP_EXP_MULT] >>
`_ = (a ** n) MOD m` by rw[GSYM EVEN_HALF, EVEN_MOD2] >>
‘((a ** 2) ** HALF n) MOD m = (a ** (2 * HALF n)) MOD m’
by rw[EXP_EXP_MULT] >>
‘_ = (a ** n) MOD m’ by rw[GSYM EVEN_HALF, EVEN_MOD2] >>
rw[],
`ODD n` by rw[ODD_EVEN] >>
`(a * (a ** 2) ** HALF n) MOD m = (a * (a ** (2 * HALF n) MOD m)) MOD m` by rw[EXP_EXP_MULT] >>
`_ = (a * a ** (2 * HALF n)) MOD m` by metis_tac[MOD_TIMES2, MOD_MOD] >>
`_ = (a ** (2 * HALF n + 1)) MOD m` by rw[EXP_ADD] >>
`_ = a ** n MOD m` by metis_tac[ODD_HALF] >>
‘ODD n’ by rw[ODD_EVEN] >>
‘(a * (a ** 2) ** HALF n) MOD m = (a * (a ** (2 * HALF n) MOD m)) MOD m’
by rw[EXP_EXP_MULT] >>
‘_ = (a * a ** (2 * HALF n)) MOD m’ by metis_tac[MOD_TIMES2, MOD_MOD] >>
‘_ = (a ** (2 * HALF n + 1)) MOD m’ by rw[EXP_ADD] >>
‘_ = a ** n MOD m’ by metis_tac[ODD_HALF] >>
rw[]
]);
]
QED

(* Theorem: exp_mod_binary 0 n m = (if n = 0 then 1 else 0) MOD m *)
(* Proof:
Expand Down
57 changes: 20 additions & 37 deletions examples/algebra/polynomial/polyWeakScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2402,42 +2402,31 @@ val _ = export_rewrites ["weak_mult_of_rzero"];
- CONJ (weak_mult_of_lzero |> SPEC_ALL) (weak_mult_of_rzero |> SPEC_ALL) |> GEN_ALL;
> val it = |- !r q p. ([] o q = []) /\ (p o [] = []) : thm
*)
val weak_mult_of_zero = save_thm("weak_mult_of_zero",
CONJ (weak_mult_of_rzero |> SPEC_ALL) (weak_mult_of_lzero |> SPEC_ALL) |> GEN_ALL);
(* > val weak_mult_of_zero = |- !r q p. (p o [] = []) /\ ([] o q = []) : thm *)

(* This is better: no need for q *)

(* Theorem: (p o [] = []) /\ ([] o p = []) *)
(* Proof: by weak_mult_of_rzero, weak_mult_of_lzero *)
val weak_mult_of_zero = store_thm(
"weak_mult_of_zero",
``!r:'a ring. !p:'a poly. (p o [] = []) /\ ([] o p = [])``,
rw_tac std_ss[weak_mult_of_rzero, weak_mult_of_lzero]);
Theorem weak_mult_of_zero:
!r:'a ring. !p:'a poly. (p o [] = []) /\ ([] o p = [])
Proof
rw_tac std_ss[weak_mult_of_rzero, weak_mult_of_lzero]
QED

(* Theorem: |0| o q = |0| *)
(* Proof: by weak_mult_of_lzero and poly_zero. *)
val weak_mult_lzero = save_thm("weak_mult_lzero", weak_mult_of_lzero |> REWRITE_RULE [GSYM poly_zero]);
Theorem weak_mult_lzero = weak_mult_of_lzero |> REWRITE_RULE [GSYM poly_zero];
(* > val weak_mult_lzero = |- !r q. |0| o q = |0| : thm *)

(* Theorem: p o |0| = |0| *)
(* Proof: by weak_mult_of_rzero and poly_zero. *)
val weak_mult_rzero = save_thm("weak_mult_rzero", weak_mult_of_rzero |> REWRITE_RULE [GSYM poly_zero]);
Theorem weak_mult_rzero = weak_mult_of_rzero |> REWRITE_RULE [GSYM poly_zero];
(* > val weak_mult_rzero = |- !p. p o |0| = |0| : thm *)

(* Theorem: p o [] = [] /\ [] o q = [] *)
(* Proof: by weak_mult_of_zero and poly_zero. *)
val weak_mult_zero = save_thm("weak_mult_zero", weak_mult_of_zero |> REWRITE_RULE [GSYM poly_zero]);
(* > val weak_mult_zero = |- !r q p. (p o |0| = |0|) /\ ( |0| o q = |0|) : thm *)

(* This is better: no need for q. *)

(* Theorem: (p o |0| = |0|) /\ ( |0| o p = |0|) *)
(* Proof: by weak_mult_rzero, weak_mult_lzero *)
val weak_mult_zero = store_thm(
"weak_mult_zero",
``!r:'a ring. !p:'a poly. (p o |0| = |0|) /\ ( |0| o p = |0|)``,
rw_tac std_ss[weak_mult_rzero, weak_mult_lzero]);
Theorem weak_mult_zero:
!r:'a ring. !p:'a poly. (p o |0| = |0|) /\ ( |0| o p = |0|)
Proof rw_tac std_ss[weak_mult_rzero, weak_mult_lzero]
QED

(*
Why is this true: weak p <> [], weak q <> [], p o q <> [].
Expand Down Expand Up @@ -3300,19 +3289,12 @@ val weak_mult_ladd = store_thm(

val _ = export_rewrites ["weak_mult_radd", "weak_mult_ladd"];

(* Theorem: p o (q || t) = p o q || p o t /\ (p || q) o t = p o t || q o t *)
(* Proof: by weak_mult_radd and weak_mult_ladd. *)
val weak_mult_add = save_thm("weak_mult_add",
CONJ (weak_mult_radd |> SPEC_ALL |> UNDISCH_ALL)
(weak_mult_ladd |> SPEC_ALL |> UNDISCH_ALL) |> DISCH_ALL |> GEN_ALL);
(* > val weak_mult_add =
|- !r. Ring r ==> (!p q t. weak p /\ weak q /\ weak t ==> (p o (q || t) = p o q || p o t) /\
!p q t. weak p /\ weak q /\ weak t ==> ((p || q) o t = p o t || q o t) : thm *)
val weak_mult_add = save_thm("weak_mult_add",
Theorem weak_mult_add =
CONJ (weak_mult_radd |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL |> UNDISCH_ALL)
(weak_mult_ladd |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL |> UNDISCH_ALL)
|> DISCH ``weak p /\ weak q /\ weak t`` |> GEN ``(t:'a poly)`` |> GEN ``(q:'a poly)`` |> GEN ``(p:'a poly)``
|> DISCH_ALL |> GEN_ALL);
|> DISCH “weak p /\ weak q /\ weak t” |> GEN “(t:'a poly)”
|> GEN “(q:'a poly)” |> GEN “(p:'a poly)”
|> DISCH_ALL |> GEN_ALL;
(* > val weak_mult_add = |- !r. Ring r ==> !p q t. weak p /\ weak q /\ weak t ==>
(p o (q || t) = p o q || p o t) /\ ((p || q) o t = p o t || q o t) : thm *)

Expand Down Expand Up @@ -4678,11 +4660,12 @@ val poly_deg_weak_neg = store_thm(
deg (neg (h::t)) = LENGTH (-t)
By weak_neg_map and LENGTH_MAP, they are equal.
*)
val poly_deg_weak_neg = store_thm(
"poly_deg_weak_neg",
``!r:'a ring. Ring r ==> !p. weak p ==> (deg (neg p) = deg p)``,
Theorem poly_deg_weak_neg[allow_rebind]:
!r:'a ring. Ring r ==> !p. weak p ==> (deg (neg p) = deg p)
Proof
metis_tac[poly_deg_cons_length, weak_neg_map, LENGTH_MAP,
weak_neg_weak, weak_neg_cons, weak_neg_of_zero, list_CASES]);
weak_neg_weak, weak_neg_cons, weak_neg_of_zero, list_CASES]
QED

(* Theorem: deg (c o p) = deg p *)
(* Proof:
Expand Down
12 changes: 7 additions & 5 deletions examples/algebra/ring/integralDomainScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,11 +252,13 @@ val integral_domain_nonzero_monoid = store_thm(
(4) x IN R+ ==> #1 * x = x, true by ring_mult_lone, ring_nonzero_eq
(5) x IN R+ ==> x * #1 = x, true by ring_mult_rone, ring_nonzero_eq
*)
val integral_domain_nonzero_monoid = store_thm(
"integral_domain_nonzero_monoid",
``!r:'a ring. IntegralDomain r ==> Monoid f*``,
rw_tac std_ss[IntegralDomain_def, Monoid_def, integral_domain_nonzero_mult_property] >>
fs[ring_nonzero_eq, ring_mult_assoc]);
Theorem integral_domain_nonzero_monoid[allow_rebind]:
!r:'a ring. IntegralDomain r ==> Monoid f*
Proof
rw_tac std_ss[IntegralDomain_def, Monoid_def,
integral_domain_nonzero_mult_property] >>
fs[ring_nonzero_eq, ring_mult_assoc]
QED

(* ring isomorphisms preserve domain properties *)

Expand Down
112 changes: 34 additions & 78 deletions examples/algebra/ring/ringInstancesScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -449,27 +449,28 @@ QED
But m MOD n = 0 means n divides m by DIVIDES_MOD_0
Therefore m = n by DIVIDES_ANTISYM
*)
val ZN_char = store_thm(
"ZN_char",
``!n. 0 < n ==> (char (ZN n) = n)``,
Theorem ZN_char[allow_rebind]:
!n. 0 < n ==> (char (ZN n) = n)
Proof
rpt strip_tac >>
`Ring (ZN n)` by rw_tac std_ss [ZN_ring] >>
`(ZN n).sum.id = 0` by rw[ZN_def, add_mod_def] >>
`(ZN n).sum.exp 1 n = 0` by rw[ZN_lemma2, ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >>
Cases_on `n = 1` >| [
`(ZN n).prod.id = 0` by rw[ZN_def, times_mod_def] >>
`(char (ZN n)) divides n` by rw[GSYM ring_char_divides] >>
‘Ring (ZN n)’ by rw_tac std_ss [ZN_ring] >>
‘(ZN n).sum.id = 0’ by rw[ZN_def, add_mod_def] >>
‘(ZN n).sum.exp 1 n = 0’ by rw[ZN_lemma2, ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >>
Cases_on ‘n = 1’ >| [
‘(ZN n).prod.id = 0’ by rw[ZN_def, times_mod_def] >>
‘(char (ZN n)) divides n’ by rw[GSYM ring_char_divides] >>
metis_tac[DIVIDES_ONE],
`(ZN n).prod.id = 1` by rw[ZN_def, times_mod_def] >>
`(ZN n).sum.exp 1 n = 0` by rw[ZN_lemma2, ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >>
`(char (ZN n)) divides n` by rw[GSYM ring_char_divides] >>
`(char (ZN n)) <= n` by rw[DIVIDES_LE] >>
qabbrev_tac `m = char (ZN n)` >>
`(ZN n).sum.exp 1 m = FUNPOW (\j. (j + 1) MOD n) m 0` by rw[ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >>
`_ = m MOD n` by rw[ZN_lemma1] >>
`n divides m` by metis_tac[char_property, DIVIDES_MOD_0] >>
‘(ZN n).prod.id = 1’ by rw[ZN_def, times_mod_def] >>
‘(ZN n).sum.exp 1 n = 0’ by rw[ZN_lemma2, ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >>
‘(char (ZN n)) divides n’ by rw[GSYM ring_char_divides] >>
‘(char (ZN n)) <= n’ by rw[DIVIDES_LE] >>
qabbrev_tac ‘m = char (ZN n)’ >>
‘(ZN n).sum.exp 1 m = FUNPOW (\j. (j + 1) MOD n) m 0’ by rw[ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >>
‘_ = m MOD n’ by rw[ZN_lemma1] >>
‘n divides m’ by metis_tac[char_property, DIVIDES_MOD_0] >>
metis_tac [DIVIDES_ANTISYM]
]);
]
QED

(* Theorem: 0 < n ==> !x k. (ZN n).prod.exp x k = (x ** k) MOD n *)
(* Proof:
Expand Down Expand Up @@ -683,14 +684,16 @@ QED
(y * (n MOD m)) MOD m = 1 by GCD_MOD_MULT_INV
and ((n MOD m) * y) MOD m = 1 by MULT_COMM
*)
val ZN_coprime_invertible = store_thm(
"ZN_coprime_invertible",
``!m n. 1 < m /\ coprime m n ==> (n MOD m) IN (Invertibles (ZN m).prod).carrier``,
rw_tac std_ss[Invertibles_def, monoid_invertibles_def, ZN_def, times_mod_def, GSPECIFICATION, IN_COUNT] >-
rw[] >>
`0 < m` by decide_tac >>
`(n MOD m) < m` by rw[] >>
metis_tac[MOD_NONZERO_WHEN_GCD_ONE, GCD_MOD_MULT_INV, coprime_mod, MULT_COMM]);
Theorem ZN_coprime_invertible[allow_rebind]:
!m n. 1 < m /\ coprime m n ==> (n MOD m) IN (Invertibles (ZN m).prod).carrier
Proof
rw_tac std_ss[Invertibles_def, monoid_invertibles_def, ZN_def, times_mod_def,
GSPECIFICATION, IN_COUNT]
>- rw[] >>
‘0 < m’ by decide_tac >>
‘(n MOD m) < m’ by rw[] >>
metis_tac[MOD_NONZERO_WHEN_GCD_ONE, GCD_MOD_MULT_INV, coprime_mod, MULT_COMM]
QED

(* Theorem: 1 < n ==> (Invertibles (ZN n).prod = Estar n) *)
(* Proof:
Expand Down Expand Up @@ -1253,43 +1256,6 @@ val ZN_not_coprime = store_thm(

(* Note: "Since ord k n > 1, there must exist a prime divisor p of n such that ord k p > 1." *)

(* Theorem: 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p *)
(* Proof:
By contradiction, suppose !p. prime p /\ p divides n /\ ~(1 < ordz m p).
Note ordz m n <> 0 by 1 < ordz m n
Thus coprime m n by ZN_order_eq_0, 0 < m
Note ordz m n <> 1 by 1 < ordz m n
so m <> 1 by ZN_order_mod_1
Now n <> 0 by GCD_0R, m <> 1
and n <> 1 by ZN_order_1, ordz m n <> 1
==> 1 < n
Note coprime m n by above
==> !p. prime p /\ p divides n
==> coprime m p by coprime_prime_factor_coprime, GCD_SYM, 1 < n
==> 0 < ordz m p by ZN_coprime_order, 0 < m
==> (ordz m p = 1) by ~(1 < ordz m p), NOT_LT_ONE, NOT_ZERO_LT_ZERO
Thus ordz m n = 1 by ZN_order_eq_1_by_prime_factors
This contradicts 1 < ordz m n in the premise.
*)
val ZN_order_gt_1_property = store_thm(
"ZN_order_gt_1_property",
``!m n. 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p``,
spose_not_then strip_assume_tac >>
`ordz m n <> 0 /\ ordz m n <> 1` by decide_tac >>
`coprime m n` by metis_tac[ZN_order_eq_0] >>
`m <> 1` by metis_tac[ZN_order_mod_1] >>
`n <> 0` by metis_tac[GCD_0R] >>
`n <> 1` by metis_tac[ZN_order_1] >>
`1 < n` by decide_tac >>
`!p. prime p /\ p divides n ==> (ordz m p = 1)` by
(rpt strip_tac >>
`coprime m p` by metis_tac[coprime_prime_factor_coprime, GCD_SYM] >>
`0 < ordz m p` by metis_tac[ZN_coprime_order] >>
metis_tac[NOT_LT_ONE, NOT_ZERO_LT_ZERO]) >>
metis_tac[ZN_order_eq_1_by_prime_factors]);

(* A better proof of the same theorem. *)

(* Theorem: 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p *)
(* Proof:
By contradiction, suppose !p. prime p /\ p divides n /\ ~(1 < ordz m p).
Expand Down Expand Up @@ -1796,24 +1762,14 @@ val symdiff_set_inter_def = Define`
x INTER (y SYM z) = (x INTER y) SYM (x INTER z)
first verify by Venn Diagram.
*)
val symdiff_set_inter_ring = store_thm(
"symdiff_set_inter_ring",
``Ring symdiff_set_inter``,
rw_tac std_ss[Ring_def, symdiff_set_inter_def] >-
rw[symdiff_set_abelian_group] >-
rw[set_inter_abelian_monoid] >-
rw[symdiff_set_def] >-
rw[set_inter_def] >>
rw[symdiff_set_def, set_inter_def, symdiff_def, EXTENSION] >>
metis_tac[]);
(* Michael's proof *)
val symdiff_set_inter_ring = store_thm(
"symdiff_set_inter_ring",
``Ring symdiff_set_inter``,
Theorem symdiff_set_inter_ring:
Ring symdiff_set_inter
Proof
rw_tac std_ss[Ring_def, symdiff_set_inter_def] >>
rw[symdiff_set_def, set_inter_def] >>
rw[EXTENSION, symdiff_def] >>
metis_tac[]);
metis_tac[]
QED

(* Theorem: symdiff UNIV UNIV = EMPTY` *)
(* Proof: by definition. *)
Expand Down

0 comments on commit 58d0603

Please sign in to comment.