%Patch files loaded: patch2 version 1.2.2.11 \$\$\$rsa.pvs rsa : THEORY BEGIN IMPORTING fermat, inverse_modulo p: prime_nat q: { x: prime_nat | p /= x } p1: posnat = p - 1 q1: posnat = q - 1 %------------------ % public modulus %------------------ N: posnat = p * q N_not_one: LEMMA N /= 1 m: posnat = p1 * q1 m_not_one: LEMMA m /= 1 %-------------------------------- % private and public exponents %-------------------------------- a: { x: posnat | prime(x, m) } b: { x: posnat | rem(m)(a * x) = 1} %--------------- % Main lemmas %--------------- x: VAR posnat prime_with_N: LEMMA prime(x, N) IFF prime(x, p) AND prime(x, q) fermat_p: LEMMA prime(x, p) IMPLIES rem(p)(expt(x, p1 * q1)) = 1 fermat_q: LEMMA prime(x, q) IMPLIES rem(q)(expt(x, p1 * q1)) = 1 rsa_aux1: LEMMA rem(p)(expt(x, a * b)) = rem(p)(x) rsa_aux2: LEMMA rem(q)(expt(x, a * b)) = rem(q)(x) rsa_prop: LEMMA rem(N)(expt(x, a * b)) = rem(N)(x) %------------------- % Encrypt/Decrypt %------------------- y: VAR mod(N) private(y): mod(N) = rem(N)(expt(y, a)) public(y): mod(N) = rem(N)(expt(y, b)) private_zero: LEMMA private(0) = 0 public_zero: LEMMA public(0) = 0 inverse_rsa1: LEMMA public(private(y)) = y inverse_rsa2: LEMMA private(public(y)) = y END rsa \$\$\$rsa.prf (|rsa| (|q_TCC1| "" (LEMMA "unbounded_primes" ("x" "p")) (("" (SKOLEM!) (("" (INST + "p!1") (("" (ASSERT) NIL))))))) (|p1_TCC1| "" (SUBTYPE-TCC) NIL) (|q1_TCC1| "" (SUBTYPE-TCC) NIL) (|N_not_one| "" (FLATTEN) (("" (EXPAND "N") (("" (REWRITE "product_one") (("" (GROUND) NIL))))))) (|m_not_one| "" (FLATTEN) (("" (EXPAND "m") (("" (REWRITE "product_one") (("" (EXPAND* "p1" "q1") (("" (GROUND) NIL))))))))) (|a_TCC1| "" (INST + "1 + m") (("" (REWRITE "mutual_primes_equiv") (("" (INST + "1" "-1") (("" (ASSERT) NIL))))))) (|b_TCC1| "" (LEMMA "rem_inverse2") (("" (INST - "m" "a") (("" (LEMMA "m_not_one") (("" (ASSERT) (("" (GROUND) (("" (SKOLEM!) (("" (INST + "py!1") NIL))))))))))))) (|prime_with_N_TCC1| "" (ASSERT) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|prime_with_N| "" (SKOLEM!) (("" (EXPAND "N") (("" (REWRITE "mutual_primes_commutes") (("" (REWRITE "mutual_prime_prod") (("" (USE "mutual_primes_commutes" ("a" "p")) (("" (USE "mutual_primes_commutes" ("a" "q")) (("" (REPLACE*) (("" (GROUND) NIL))))))))))))))) (|fermat_p| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_times_aux" "rem_one" "expt_1n_aux") (("" (FORWARD-CHAIN "fermat_theorem2") (("" (REWRITE "p1" :DIR RL) (("" (ASSERT) (("" (REWRITE "rem_expt1" 1 :DIR RL) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))))))) (|fermat_q_TCC1| "" (ASSERT) NIL) (|fermat_q| "" (SKOSIMP) (("" (AUTO-REWRITE "rem_one" "expt_1n_aux") (("" (FORWARD-CHAIN "fermat_theorem2") (("" (REWRITE "q1" :DIR RL) (("" (USE "expt_times_aux" ("m" "q1" "n" "p1")) (("" (REPLACE -1) (("" (REWRITE "rem_expt1" 1 :DIR RL) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))))))))) (|rsa_aux1| "" (SKOSIMP) (("" (USE "non_multiple_of_prime" ("p" "p" "a" "x!1")) (("" (GROUND) (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero") (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (CASE-REPLACE "rem(p)(x!1) = 0") (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL))))))) ("2" (REWRITE "mutual_primes_commutes") (("2" (TYPEPRED "b") (("2" (ASSERT) (("2" (REWRITE "rem_def") (("2" (SKOLEM!) (("2" (CASE "q!1 >= 0") (("1" (ASSERT) (("1" (REPLACE*) (("1" (DELETE -1 -2 -3) (("1" (AUTO-REWRITE "expt_1n_aux" "rem_one" "fermat_p") (("1" (EXPAND "expt") (("1" (REWRITE "expt_times_aux") (("1" (REWRITE "rem_prod2" :DIR RL) (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (EXPAND "m") (("1" (ASSERT) NIL))))))))))))))))))) ("2" (DELETE -3 2) (("2" (USE "pos_times_le" ("x" "m" "y" "q!1")) (("2" (GROUND) NIL))))))))))))))))))))))) (|rsa_aux2| "" (SKOSIMP) (("" (USE "non_multiple_of_prime" ("p" "q" "a" "x!1")) (("" (GROUND) (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero") (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (CASE-REPLACE "rem(q)(x!1) = 0") (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL))))))) ("2" (REWRITE "mutual_primes_commutes") (("2" (TYPEPRED "b") (("2" (ASSERT) (("2" (REWRITE "rem_def") (("2" (SKOLEM!) (("2" (CASE "q!1 >= 0") (("1" (ASSERT) (("1" (REPLACE*) (("1" (DELETE -1 -2 -3) (("1" (AUTO-REWRITE "expt_1n_aux" "rem_one" "fermat_q") (("1" (EXPAND "expt") (("1" (REWRITE "expt_times_aux") (("1" (REWRITE "rem_prod2" :DIR RL) (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (EXPAND "m") (("1" (ASSERT) NIL))))))))))))))))))) ("2" (DELETE -3 2) (("2" (USE "pos_times_le" ("x" "m" "y" "q!1")) (("2" (GROUND) NIL))))))))))))))))))))))) (|rsa_prop| "" (SKOLEM!) (("" (AUTO-REWRITE "same_remainder" "distinct_primes" "divides_zero") (("" (USE* "rsa_aux1" "rsa_aux2") (("" (ASSERT) (("" (EXPAND "N") (("" (REWRITE "common_multiple_primes") (("" (FLATTEN) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))))))))) (|private_zero_TCC1| "" (SUBTYPE-TCC) NIL) (|private_zero| "" (AUTO-REWRITE "private" "expt" "zero_times1" "rem_zero") (("" (ASSERT) (("" (ASSERT) NIL))))) (|public_zero| "" (AUTO-REWRITE "public" "expt" "zero_times1" "rem_zero") (("" (ASSERT) (("" (ASSERT) NIL))))) (|inverse_rsa1| "" (AUTO-REWRITE "private_zero" "public_zero" "rem_expt1" "rem_mod" "rsa_prop") (("" (SKOLEM!) (("" (CASE-REPLACE "y!1 = 0") (("1" (ASSERT) NIL) ("2" (EXPAND "public") (("2" (EXPAND "private") (("2" (ASSERT) (("2" (REWRITE "expt_times_aux" :DIR RL) (("2" (ASSERT) NIL))))))))))))))) (|inverse_rsa2| "" (AUTO-REWRITE "private_zero" "public_zero" "rem_expt1" "rem_mod" "rsa_prop") (("" (SKOLEM!) (("" (CASE-REPLACE "y!1 = 0") (("1" (ASSERT) NIL) ("2" (EXPAND "public") (("2" (EXPAND "private") (("2" (ASSERT) (("2" (REWRITE "expt_times_aux" :DIR RL) (("2" (REWRITE "commutative_mult") (("2" (ASSERT) NIL)))))))))))))))))) \$\$\$inverse_modulo.pvs inverse_modulo : THEORY BEGIN IMPORTING mutual_primes x, y: VAR int py, b: VAR posnat %------------------------------------ % Existence of an inverse modulo b %------------------------------------ rem_inverse: LEMMA (EXISTS y : rem(b)(x * y) = 1) IFF x /= 0 AND b /= 1 AND prime(x, b) rem_inverse2: LEMMA (EXISTS py: rem(b)(x * py) = 1) IFF x /= 0 AND b /= 1 AND prime(x, b) END inverse_modulo \$\$\$inverse_modulo.prf (|inverse_modulo| (|rem_inverse| "" (SKOLEM!) (("" (CASE-REPLACE "x!1=0") (("1" (AUTO-REWRITE "rem_zero") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (AUTO-REWRITE "mutual_primes_equiv" "rem_def") (("2" (ASSERT) (("2" (REDUCE :INSTANTIATOR INST!) (("1" (INST + "y!1" "-q!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "n!1") (("2" (INST + "- m!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rem_inverse2| "" (SKOLEM!) (("" (REWRITE "rem_inverse" :DIR RL) (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "rem_prod2" :DIR RL) (("2" (AUTO-REWRITE "rem_zero") (("2" (CASE-REPLACE "rem(b!1)(y!1) = 0") (("1" (ASSERT) NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$product_modulo.pvs product_modulo : THEORY BEGIN IMPORTING products u, v: VAR [nat -> nat] n, m: VAR nat p: VAR posnat equivalent_product: LEMMA n <= m AND (FORALL (i: idx(n, m)): rem(p)(u(i)) = rem(p)(v(i))) IMPLIES rem(p)(prod(n, m)(u)) = rem(p)(prod(n, m)(v)) END product_modulo \$\$\$product_modulo.prf (|product_modulo| (|equivalent_product_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|equivalent_product| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL (j : nat): j <= m!1 - n!1 IMPLIES rem(p!1)(prod(n!1, n!1 + j)(u!1)) = rem(p!1)(prod(n!1, n!1+j)(v!1))") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "rem_prod") NIL NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$parity.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A few lemmas about odd or even numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% parity : THEORY BEGIN i : VAR int incr_odd : LEMMA odd?(i + 1) IFF even?(i) incr_even : LEMMA even?(i + 1) IFF odd?(i) opposite_odd : LEMMA odd?(- i) IFF odd?(i) opposite_even : LEMMA even?(- i) IFF even?(i) parity1 : LEMMA odd?(i) OR odd?(i + 1) parity2 : LEMMA even?(i) OR even?(i + 1) odd_not_even : LEMMA odd?(i) IFF not even?(i) even_not_odd : LEMMA even?(i) IFF not odd?(i) even_2i : LEMMA even?(2 * i) odd_2i_plus1 : LEMMA odd?(2 * i + 1) odd_2i_minus1 : LEMMA odd?(2 * i - 1) %------------------------------------- % Rewrite rules for small constants %------------------------------------- parity_zero: LEMMA even?(0) parity_one: LEMMA odd?(1) parity_two: LEMMA even?(2) parity_three: LEMMA odd?(3) parity_minus_one: LEMMA odd?(-1) parity_minus_two: LEMMA even?(-2) parity_minus_three: LEMMA odd?(-3) END parity \$\$\$parity.prf (|parity| (|incr_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) NIL NIL) (|incr_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "j!1 - 1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "j!1 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1-1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "- j!1 -1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "-j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|parity1| (:NEW-GROUND? NIL) "" (CASE "FORALL (n : nat) : odd?(n) OR odd?(n + 1)") (("1" (SKOSIMP) (("1" (CASE "i!1 >= 0") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST - "- (1 + i!1)") (("2" (REWRITE "opposite_odd" 2 :DIR RL) (("2" (REWRITE "opposite_odd" 3 :DIR RL) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (GROUND) (("2" (DELETE 1) (("2" (EXPAND "odd?") (("2" (SKOLEM!) (("2" (INST + "j!2 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|parity2| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "incr_even") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "parity1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|odd_not_even| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_not_odd| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_2i| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|odd_2i_plus1| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|odd_2i_minus1| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (REWRITE "incr_even" :DIR RL) (("" (REWRITE "even_2i") NIL NIL)) NIL)) NIL) (|parity_zero| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|parity_one| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd") (("" (REWRITE "parity_zero") NIL NIL)) NIL) (|parity_two| (:NEW-GROUND? NIL) "" (REWRITE "incr_even") (("" (REWRITE "parity_one") NIL NIL)) NIL) (|parity_three| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd") (("" (REWRITE "parity_two") NIL NIL)) NIL) (|parity_minus_one_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_one| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd") (("" (REWRITE "parity_one") NIL NIL)) NIL) (|parity_minus_two_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_two| (:NEW-GROUND? NIL) "" (REWRITE "opposite_even") (("" (REWRITE "parity_two") NIL NIL)) NIL) (|parity_minus_three_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_three| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd") (("" (REWRITE "parity_three") NIL NIL)) NIL)) \$\$\$index_range.pvs index_range : THEORY BEGIN i, n, m: VAR nat idx(n, m): TYPE = {i | n <= i AND i <= m} END index_range \$\$\$nat_fun_props.pvs nat_fun_props : THEORY BEGIN n, m : VAR nat injection_n_to_m : THEOREM (EXISTS (f : [below(n) -> below(m)]) : injective?(f)) IMPLIES n <= m surjection_n_to_m : THEOREM (EXISTS (f : [below(n) -> below(m)]) : surjective?(f)) IMPLIES m <= n bijection_n_to_m : THEOREM (EXISTS (f : [below(n) -> below(m)]) : bijective?(f)) IFF n = m injection_n_to_m2: THEOREM (EXISTS (f : [upto(n) -> upto(m)]) : injective?(f)) IFF n <= m surjection_n_to_m2: THEOREM (EXISTS (f : [upto(n) -> upto(m)]) : surjective?(f)) IFF m <= n bijection_n_to_m2: THEOREM (EXISTS (f : [upto(n) -> upto(m)]) : bijective?(f)) IFF n = m surj_equiv_inj: THEOREM FORALL (f : [below(n) -> below(n)]) : surjective?(f) IFF injective?(f) inj_equiv_bij: THEOREM FORALL (f : [below(n) -> below(n)]) : bijective?(f) IFF injective?(f) surj_equiv_bij: THEOREM FORALL (f : [below(n) -> below(n)]) : bijective?(f) IFF surjective?(f) surj_equiv_inj2: THEOREM FORALL (f : [upto(n) -> upto(n)]) : surjective?(f) IFF injective?(f) inj_equiv_bij2: THEOREM FORALL (f : [upto(n) -> upto(n)]) : bijective?(f) IFF injective?(f) surj_equiv_bij2: THEOREM FORALL (f : [upto(n) -> upto(n)]) : bijective?(f) IFF surjective?(f) END nat_fun_props \$\$\$nat_fun_props.prf (|nat_fun_props| (|injection_n_to_m| "" (INDUCT "n") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "f!1(0)") (("2" (ASSERT) (("2" (HIDE -1) (("2" (INST -1 "m!1 - 1") (("2" (ASSERT) (("2" (DELETE 2) (("2" (INST + "LAMBDA (x : below(j!1)) : IF f!1(x) = m!1 - 1 THEN f!1(j!1) ELSE f!1(x) ENDIF") (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (INST-CP -2 "x1!1" "j!1") (("1" (INST-CP -2 "x2!1" "j!1") (("1" (INST -2 "x1!1" "x2!1") (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (EXPAND "injective?") (("3" (INST - "x!1" "j!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|surjection_n_to_m| "" (SKOSIMP*) (("" (COPY -1) (("" (REWRITE "injection_n_to_m") (("" (EXPAND "surjective?" -1) (("" (INST -1 "0") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST + "inverse(f!1)") (("1" (REWRITE "inj_inv") (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bijection_n_to_m| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "bijective?") (("1" (SKOSIMP) (("1" (LEMMA "injection_n_to_m" ("n" "n!1" "m" "m!1")) (("1" (LEMMA "surjection_n_to_m" ("n" "n!1" "m" "m!1")) (("1" (SPLIT) (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST 1 "LAMBDA (x : below(n!1)) : x") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|injection_n_to_m2| "" (SKOLEM!) (("" (GROUND) (("1" (LEMMA "injection_n_to_m" ("n" "n!1+1" "m" "m!1+1")) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST + "lambda (i : below(1 + n!1)) : f!1(i)") (("1" (GRIND :IF-MATCH NIL) (("1" (INST? :WHERE +) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i : upto(n!1)): i") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|surjection_n_to_m2| "" (SKOLEM!) (("" (GROUND) (("1" (LEMMA "surjection_n_to_m" ("n" "n!1+1" "m" "m!1+1")) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST + "lambda (i: below(1 + n!1)): f!1(i)") (("1" (GRIND :IF-MATCH NIL) (("1" (INST? -) (("1" (SKOLEM!) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i : upto(n!1)): IF i <= m!1 THEN i ELSE 0 ENDIF") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|bijection_n_to_m2| "" (SKOLEM!) (("" (GROUND) (("1" (EXPAND "bijective?") (("1" (SKOSIMP) (("1" (LEMMA "injection_n_to_m2" ("n" "n!1" "m" "m!1")) (("1" (LEMMA "surjection_n_to_m2" ("n" "n!1" "m" "m!1")) (("1" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i : upto(n!1)): i") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|surj_equiv_inj| "" (SKOLEM!) (("" (CASE "n!1 = 0") (("1" (GRIND) NIL NIL) ("2" (GROUND) (("1" (USE "surjection_n_to_m" ("n" "n!1 - 1" "m" "n!1")) (("1" (ASSERT) (("1" (EXPAND* "surjective?" "injective?") (("1" (SKOSIMP) (("1" (INST + "lambda (i : below(n!1 - 1)): IF i < x1!1 THEN f!1(i) ELSE f!1(i+1) ENDIF") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST - "y!1") (("1" (SKOLEM!) (("1" (CASE "x!1 = x1!1") (("1" (INST + "IF x2!1 < x!1 THEN x2!1 ELSE x2!1-1 ENDIF") (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL)) NIL) ("2" (INST + "IF x!1 < x1!1 THEN x!1 ELSE x!1 - 1 ENDIF") (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "injection_n_to_m" ("n" "n!1" "m" "n!1-1")) (("2" (ASSERT) (("2" (EXPAND* "injective?" "surjective?") (("2" (SKOLEM!) (("2" (INST + "lambda (i : below(n!1)) : IF f!1(i) = n!1 - 1 THEN y!1 ELSE f!1(i) ENDIF") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST? - :WHERE +) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST + "x2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (INST? +) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inj_equiv_bij| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL NIL)) NIL)) NIL)) NIL) (|surj_equiv_bij| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL NIL)) NIL)) NIL)) NIL) (|surj_equiv_inj2| "" (SKOLEM!) (("" (LEMMA "surj_equiv_inj" ("n" "n!1+1" "f" "lambda (i : below(n!1 + 1)): f!1(i)")) (("1" (EXPAND* "surjective?" "injective?") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST? -4 :WHERE +) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -2) (("2" (SKOLEM!) (("2" (INST? +) NIL NIL)) NIL)) NIL) ("3" (INST - "y!1") (("3" (SKOLEM!) (("3" (INST + "x!1") NIL NIL)) NIL)) NIL) ("4" (INST? - :WHERE +) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|inj_equiv_bij2| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL NIL)) NIL)) NIL)) NIL) (|surj_equiv_bij2| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL NIL)) NIL)) NIL)) NIL)) \$\$\$iterations.pvs iterations [ T : TYPE ] : THEORY BEGIN IMPORTING nat_fun_props, index_range f : VAR [T, T -> T] u, v: VAR [nat -> T] n, m, p, q, i, j, k: VAR nat x, y, z, t: VAR T %-------------------------------------------- % Iterated application of f to u(n)...u(m) %-------------------------------------------- iter(f, n, (m | n <= m), u): RECURSIVE T = IF n=m THEN u(n) ELSE f(iter(f, n, m-1, u), u(m)) ENDIF MEASURE m iter_once: LEMMA iter(f, n, n, u) = u(n) iter_induct: LEMMA FORALL n, (m | n <= m): iter(f, n, m + 1, u) = f(iter(f, n, m, u), u(m + 1)) iter_same_elements: LEMMA FORALL n, (m | n <= m): (FORALL i: n <= i AND i <= m IMPLIES u(i) = v(i)) IMPLIES iter(f, n, m, u) = iter(f, n, m, v) %---------------------------------------- % Iteration of an associative function %---------------------------------------- g : VAR { f | associative?(f) } associativity: LEMMA g(x, g(y, z)) = g(g(x, y), z) iter_assoc_split: LEMMA n <= m AND m < p IMPLIES g(iter(g, n, m, u), iter(g, m + 1, p, u)) = iter(g, n, p, u) %-------------------------------------------------------- % Iteration of an associative and commutative function %-------------------------------------------------------- h : VAR { g | commutative?(g) } commutativity: LEMMA h(x, y) = h(y, x) commut_assoc1: LEMMA h(h(x, y), h(z, t)) = h(h(x, z), h(y, t)) commut_assoc2: LEMMA h(h(x, y), z) = h(h(z, y), x) %-------------------------------------------- % iteration on h(u(n),v(n))...h(u(m),v(m)) %-------------------------------------------- iter_split: LEMMA FORALL n, (m | n <= m): iter(h, n, m, lambda i: h(u(i), v(i))) = h(iter(h, n, m, u), iter(h, n, m, v)) %------------------------------------------- % Invariance if two elements are swapped %------------------------------------------- swap(u, n, m)(i): T = IF i=m THEN u(n) ELSIF i=n THEN u(m) ELSE u(i) ENDIF swap_unchanged: LEMMA swap(u, n, n) = u swap_commutes: LEMMA swap(u, n, m) = swap(u, m, n) swap_inverse: LEMMA swap(swap(u, n, m), n, m) = u iter_swap_first_last: LEMMA n <= m IMPLIES iter(h, n, m, swap(u, n, m)) = iter(h, n, m, u) iter_swap_last: LEMMA n <= i AND i <= m IMPLIES iter(h, n, m, swap(u, i, m)) = iter(h, n, m, u) iter_swap: LEMMA n <= i AND i <= j AND j <= m IMPLIES iter(h, n, m, swap(u, i, j)) = iter(h, n, m, u) %-------------------------------------------- % IF u[n..m] is a permutation of v[p..q] % then iter(h, n, m, u) = iter(h, p, q, v) %-------------------------------------------- permutation(u, n, m, v, p, q): bool = EXISTS (a: [idx(n, m) -> idx(p, q)]): bijective?(a) AND FORALL (i: idx(n, m)): u(i) = v(a(i)) perm_range: LEMMA n <= m AND permutation(u, n, m, v, p, q) IMPLIES m - n = q - p perm_equiv: LEMMA permutation(u, n, n+m, v, p, p+m) IFF EXISTS (a: [idx(n, n+m) -> idx(p, p+m)]): injective?(a) AND FORALL (i: idx(n, n+m)): u(i) = v(a(i)) iter_permutation: LEMMA permutation(u, n, n + m, v, p, p + m) IMPLIES iter(h, n, n + m, u) = iter(h, p, p + m, v) iter_permutation2: LEMMA n <= m AND permutation(u, n, m, v, p, q) IMPLIES iter(h, n, m, u) = iter(h, p, q, v) iter_permutation3: LEMMA FORALL (a : [idx(n, n + m) -> idx(p, p + m)]): injective?(a) AND (FORALL (i: idx(n, n + m)): u(i) = v(a(i))) IMPLIES iter(h, n, n + m, u) = iter(h, p, p + m, v) END iterations \$\$\$iterations.prf (|iterations| (|iter_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_TCC2| "" (TERMINATION-TCC) NIL NIL) (|iter_once_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_once| "" (GRIND) NIL NIL) (|iter_induct_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_induct| "" (GRIND) NIL NIL) (|iter_same_elements| "" (SKOSIMP) (("" (CASE "FORALL (x: nat): n!1 + x <= m!1 IMPLIES iter(f!1, n!1, n!1 + x, u!1) = iter(f!1, n!1, n!1 + x, v!1)") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-SIMPLIFY "x") NIL NIL)) NIL)) NIL)) NIL) (|associativity| "" (SKOLEM-TYPEPRED) (("" (EXPAND "associative?") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|iter_assoc_split_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_assoc_split_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|iter_assoc_split| "" (SKOLEM + ("g!1" "m!1" "n!1" _ "u!1")) (("" (INDUCT-AND-REWRITE "p" 1 "iter") (("" (CASE "m!1 < j!1") (("1" (ASSERT) (("1" (REWRITE "associativity" 1) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (STOP-REWRITE "iter") (("2" (CASE-REPLACE "m!1 = j!1") (("1" (REWRITE "iter_once") NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|commutativity| "" (GRIND) NIL NIL) (|commut_assoc1| "" (SKOLEM!) (("" (NAME-REPLACE "x!2" "h!1(h!1(x!1, z!1), h!1(y!1, t!1))" :HIDE? NIL) (("" (REWRITE "associativity") (("" (REWRITE "associativity") (("" (REWRITE "associativity" :DIR RL) (("" (REWRITE "associativity" :DIR RL +) (("" (USE "commutativity" ("x" "z!1" "y" "y!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|commut_assoc2| "" (SKOLEM!) (("" (USE "commutativity" ("x" "z!1" "y" "y!1")) (("" (USE "commutativity" ("x" "x!1" "y" "y!1")) (("" (REPLACE*) (("" (DELETE -) (("" (REWRITE "associativity" :DIR RL) (("" (REWRITE "associativity" :DIR RL) (("" (USE "commutativity" ("x" "x!1" "y" "z!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_split| "" (SKOSIMP) (("" (CASE "FORALL (x: nat): iter(h!1, n!1, n!1 + x, lambda i: h!1(u!1(i), v!1(i))) = h!1(iter(h!1, n!1, n!1 + x, u!1), iter(h!1, n!1, n!1 + x, v!1))") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "iter") (("2" (INDUCT "x") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REPLACE*) (("2" (REWRITE "commut_assoc1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|swap_unchanged| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|swap_commutes| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|swap_inverse| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|iter_swap_first_last| "" (SKOSIMP) (("" (CASE-REPLACE "m!1 = n!1") (("1" (REWRITE "swap_unchanged") NIL NIL) ("2" (AUTO-REWRITE "iter_once" "iter" "swap") (("2" (ASSERT) (("2" (CASE-REPLACE "m!1 - 1 = n!1") (("1" (ASSERT) (("1" (REWRITE "commutativity") NIL NIL)) NIL) ("2" (STOP-REWRITE "iter") (("2" (USE "iter_assoc_split" ("m" "n!1" "u" "u!1")) (("2" (USE "iter_assoc_split" ("m" "n!1" "u" "swap(u!1, n!1, m!1)")) (("2" (ASSERT) (("2" (REPLACE -1 + RL) (("2" (REPLACE -2 + RL) (("2" (DELETE -1 -2) (("2" (CASE-REPLACE "iter(h!1, 1 + n!1, m!1 - 1, swap(u!1, n!1, m!1)) = iter(h!1, 1 + n!1, m!1 - 1, u!1)") (("1" (REWRITE "commut_assoc2") NIL NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE 2 5) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_swap_last_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_swap_last| "" (SKOSIMP) (("" (AUTO-REWRITE "iter_swap_first_last") (("" (CASE-REPLACE "i!1 = n!1") (("1" (ASSERT) NIL NIL) ("2" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "swap(u!1, i!1, m!1)")) (("1" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "u!1")) (("1" (ASSERT) (("1" (CASE-REPLACE "iter(h!1, n!1, i!1 - 1, swap(u!1, i!1, m!1)) = iter(h!1, n!1, i!1 - 1, u!1)") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|iter_swap_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_swap| "" (SKOSIMP) (("" (AUTO-REWRITE "iter_swap_last") (("" (CASE-REPLACE "j!1 = m!1") (("1" (ASSERT) NIL NIL) ("2" (USE "iter_assoc_split" ("m" "j!1" "u" "swap(u!1, i!1, j!1)")) (("2" (USE "iter_assoc_split" ("m" "j!1" "u" "u!1")) (("2" (ASSERT) (("2" (CASE-REPLACE "iter(h!1, 1 + j!1, m!1, swap(u!1, i!1, j!1)) = iter(h!1, 1+j!1, m!1, u!1)") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|perm_range| "" (EXPAND "permutation") (("" (SKOSIMP*) (("" (ASSERT) (("" (TYPEPRED "a!1(n!1)") (("" (ASSERT) (("" (DELETE -1 -2 -3 -5) (("" (REWRITE "bijection_n_to_m2" :DIR RL) (("" (INST + "lambda (i : upto(m!1 - n!1)): a!1(n!1 + i) - p!1") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -3 "p!1 + y!1") (("1" (SKOLEM!) (("1" (INST + "x!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST -3 "n!1 + x1!1" "n!1 + x2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|perm_equiv| "" (SKOSIMP) (("" (EXPAND "permutation") (("" (EXPAND "bijective?") (("" (GROUND) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (GROUND) (("2" (DELETE -2) (("2" (USE "surj_equiv_inj2" ("n" "m!1" "f" "lambda (i : upto(m!1)): a!1(i + n!1) - p!1")) (("1" (GRIND :IF-MATCH NIL) (("1" (INST - "y!1 - p!1") (("1" (SKOLEM!) (("1" (INST? +) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST - "n!1 + x1!1" "n!1 + x2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_permutation_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation| "" (SKOLEM 1 ("h!1" _ "n!1" "p!1" _ _)) (("" (AUTO-REWRITE "iter" "swap") (("" (INDUCT "m") (("1" (SKOSIMP) (("1" (EXPAND "permutation") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "perm_equiv") (("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST - "u!1" "swap(v!1, a!1(1 + j!1 + n!1), j!1 + 1 + p!1)") (("2" (GROUND) (("1" (USE "iter_swap_last" ("n" "p!1" "i" "a!1(1 + j!1 + n!1)" "m" "1 + j!1 + p!1")) (("1" (ASSERT) (("1" (REPLACE -1 + RL) (("1" (DELETE -1) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INST + "lambda (i : idx(n!1, j!1+n!1)): IF a!1(i) = 1 + j!1 + p!1 THEN a!1(1 + j!1 + n!1) ELSE a!1(i) ENDIF") (("1" (GROUND) (("1" (DELETE -2) (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (INST-CP - "x1!1" "x2!1") (("1" (INST-CP - "x1!1" "1+j!1+n!1") (("1" (INST - "x2!1" "1+j!1+n!1") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (LIFT-IF) (("2" (GROUND) (("1" (INST?) (("1" (EXPAND "swap") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (EXPAND "injective?") (("2" (INST - "i!1" "1 + j!1 + n!1") (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (GROUND) (("3" (EXPAND "injective?") (("3" (INST - "i!1" "1 + j!1 + n!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_permutation2_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation2| "" (SKOSIMP) (("" (FORWARD-CHAIN "perm_range") (("" (ASSERT) (("" (USE "iter_permutation" ("m" "m!1 - n!1" "p" "p!1" "v" "v!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|iter_permutation3_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation3_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation3| "" (SKOSIMP) (("" (REWRITE "iter_permutation") (("" (REWRITE "perm_equiv") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$products.pvs products : THEORY BEGIN IMPORTING iterations, parity i, j, n, m, p, q: VAR nat u, v : VAR [nat -> real] x, y, z: VAR real %-------------------------------------------------- % prod(n, m)(u) = u(n) * u(n+1) * ... * u(m) % (requires n <= m AND u: [nat -> real]) %-------------------------------------------------- f: VAR [real, real -> real] times_assoc_commutes: JUDGEMENT * HAS_TYPE { f | associative?(f) AND commutative?(f) } prod(n, (m | n <= m))(u): real = iter(*, n, m, u) prod_once: LEMMA prod(n, n)(u) = u(n) prod_step: LEMMA n <= m IMPLIES prod(n, m+1)(u) = prod(n, m)(u) * u(m+1) prod_same_elements: LEMMA n <= m AND (FORALL (i : idx(n, m)) : u(i) = v(i)) IMPLIES prod(n, m)(u) = prod(n, m)(v) prod_split: LEMMA n <= m AND m < p IMPLIES prod(n, m)(u) * prod(m+1, p)(u) = prod(n, p)(u) prod_split2: LEMMA n <= m IMPLIES prod(n, m)(lambda i : u(i) * v(i)) = prod(n, m)(u) * prod(n, m)(v) prod_permutation: LEMMA permutation(u, n, n + m, v, p, p + m) IMPLIES prod(n, n + m)(u) = prod(p, p + m)(v) prod_const: LEMMA prod(n, n + m)(lambda i: x) = expt(x, m + 1) %----------------------- % Sign of the product %----------------------- P: VAR { R: [real -> bool] | FORALL x, y: R(x) AND R(y) IMPLIES R(x * y) } prod_closure: LEMMA n <= m AND (FORALL (i: idx(n, m)): P(u(i))) IMPLIES P(prod(n, m)(u)) prod_positive: LEMMA n <= m AND (FORALL (i: idx(n, m)): u(i) > 0) IMPLIES prod(n, m)(u) > 0 prod_negative: LEMMA n <= m AND (FORALL (i: idx(n, m)): u(i) < 0) IMPLIES IF even?(m - n) THEN prod(n, m)(u) < 0 ELSE prod(n, m)(u) > 0 ENDIF prod_negative1: LEMMA n <= m AND even?(m - n) AND (FORALL (i: idx(n, m)): u(i) < 0) IMPLIES prod(n, m)(u) < 0 prod_negative2: LEMMA n <= m AND odd?(m - n) AND (FORALL (i: idx(n, m)): u(i) < 0) IMPLIES prod(n, m)(u) > 0 prod_null: LEMMA n <= m AND (EXISTS (i: idx(n, m)): u(i) = 0) IMPLIES prod(n, m)(u) = 0 prod_null2: LEMMA n <= m IMPLIES (prod(n, m)(u) = 0 IFF EXISTS (i: idx(n, m)): u(i) = 0) posu: VAR [nat -> posreal] nzu: VAR [nat -> nzreal] nnu: VAR [nat -> nonneg_real] prod_posreal_seq_is_posreal: JUDGEMENT prod(n, (m | n <= m))(posu) HAS_TYPE posreal prod_nzreal_seq_is_nzreal: JUDGEMENT prod(n, (m | n <= m))(nzu) HAS_TYPE nzreal prod_nnreal_seq_is_nnreal: JUDGEMENT prod(n, (m | n <= m))(nnu) HAS_TYPE nonneg_real ru: VAR [nat -> rat] posru: VAR [nat -> posrat] nzru: VAR [nat -> nzrat] nnru: VAR [nat -> nonneg_rat] prod_rat_seq_is_rat: JUDGEMENT prod(n, (m | n <= m))(ru) HAS_TYPE rat prod_posrat_seq_is_posrat: JUDGEMENT prod(n, (m | n <= m))(posru) HAS_TYPE posrat prod_nzrat_seq_is_nzrat: JUDGEMENT prod(n, (m | n <= m))(nzru) HAS_TYPE nzrat prod_nnrat_seq_is_nnrat: JUDGEMENT prod(n, (m | n <= m))(nnru) HAS_TYPE nonneg_rat iu: VAR [nat -> int] nu: VAR [nat -> nat] posnu: VAR [nat -> posnat] nziu: VAR [nat -> nzint] prod_int_seq_is_int: JUDGEMENT prod(n, (m | n <= m))(iu) HAS_TYPE int prod_posnat_seq_is_posnat: JUDGEMENT prod(n, (m | n <= m))(posnu) HAS_TYPE posnat prod_nzint_seq_is_nzint: JUDGEMENT prod(n, (m | n <= m))(nziu) HAS_TYPE nzint prod_nat_seq_is_nat: JUDGEMENT prod(n, (m | n <= m))(nu) HAS_TYPE nat %------------------------------------ % prod(n)(a) = a(0) * ... * a(n-1) % requires a : [below(n) -> real] %------------------------------------ prod(n)(a:[below(n) -> real]): RECURSIVE real = IF n=0 THEN 1 ELSE prod(n-1)(lambda (i: below(n-1)): a(i)) * a(n-1) ENDIF MEASURE n variant_prod_zero: LEMMA FORALL (a: [below(0) -> real]): prod(0)(a) = 1 variant_prod_one: LEMMA FORALL (a: [below(1) -> real]): prod(1)(a) = a(0) variant_prod_two: LEMMA FORALL (a: [below(2) -> real]): prod(2)(a) = a(0) * a(1) variant_prod_equiv: LEMMA FORALL (a: [below(n) -> real]): prod(n)(a) = prod(0, n)(lambda i: IF i real]): prod(n)(lambda (i: below(n)): a(i) * b(i)) = prod(n)(a) * prod(n)(b) variant_prod_permutation: LEMMA FORALL (a, b: [below(n) -> real]), (h: [below(n) -> below(n)]): injective?(h) AND a = b o h IMPLIES prod(n)(a) = prod(n)(b) variant_prod_cont: LEMMA prod(n)(lambda (i: below(n)): x) = expt(x, n) %-------- % Sign %-------- Q: VAR { R: [real -> bool] | R(1) AND FORALL x, y: R(x) AND R(y) IMPLIES R(x * y) } variant_prod_closure: LEMMA FORALL (a: [below(n) -> real]): (FORALL (i: below(n)): Q(a(i))) IMPLIES Q(prod(n)(a)) variant_prod_positive: LEMMA FORALL (a: [below(n) -> real]): (FORALL (i: below(n)): a(i) > 0) IMPLIES prod(n)(a) > 0 variant_prod_negative: LEMMA FORALL (a: [below(n) -> real]): (FORALL (i: below(n)): a(i) < 0) IMPLIES IF even?(n) THEN prod(n)(a) > 0 ELSE prod(n)(a) < 0 ENDIF variant_prod_negative1: LEMMA FORALL (a: [below(n) -> real]): even?(n) AND (FORALL (i: below(n)): a(i) < 0) IMPLIES prod(n)(a) > 0 variant_prod_negative2: LEMMA FORALL (a: [below(n) -> real]): odd?(n) AND (FORALL (i: below(n)): a(i) < 0) IMPLIES prod(n)(a) < 0 variant_prod_null: LEMMA FORALL (a: [below(n) -> real]): (EXISTS (i: below(n)): a(i) = 0) IMPLIES prod(n)(a) = 0 variant_prod_null2: LEMMA FORALL (a: [below(n) -> real]): prod(n)(a) = 0 IFF EXISTS (i: below(n)): a(i) = 0 on: VAR { n | odd?(n) } en: VAR { n | even?(n) } pn: VAR posnat varprod_posreal_seq: JUDGEMENT prod(n)(a: [below(n) -> posreal]) HAS_TYPE posreal varprod_nzreal_seq: JUDGEMENT prod(n)(a: [below(n) -> nzreal]) HAS_TYPE nzreal varprod_nnreal_seq: JUDGEMENT prod(n)(a: [below(n) -> nonneg_real]) HAS_TYPE nonneg_real varprod_negreal_seq1: JUDGEMENT prod(en)(a: [below(en) -> negreal]) HAS_TYPE posreal varprod_negreal_seq2: JUDGEMENT prod(on)(a: [below(on) -> negreal]) HAS_TYPE negreal varprod_rat_seq: JUDGEMENT prod(n)(a: [below(n) -> rat]) HAS_TYPE rat varprod_posrat_seq: JUDGEMENT prod(n)(a: [below(n) -> posrat]) HAS_TYPE posrat varprod_nzrat_seq: JUDGEMENT prod(n)(a: [below(n) -> nzrat]) HAS_TYPE nzrat varprod_nnrat_seq: JUDGEMENT prod(n)(a: [below(n) -> nonneg_rat]) HAS_TYPE nonneg_rat varprod_negrat_seq1: JUDGEMENT prod(en)(a: [below(en) -> negrat]) HAS_TYPE posrat varprod_negrat_seq2: JUDGEMENT prod(on)(a: [below(on) -> negrat]) HAS_TYPE negrat varprod_int_seq: JUDGEMENT prod(n)(a: [below(n) -> int]) HAS_TYPE int varprod_posint_seq: JUDGEMENT prod(n)(a: [below(n) -> posint]) HAS_TYPE posint varprod_nzint_seq: JUDGEMENT prod(n)(a: [below(n) -> nzint]) HAS_TYPE nzint varprod_nat_seq: JUDGEMENT prod(n)(a: [below(n) -> nat]) HAS_TYPE nat varprod_negint_seq1: JUDGEMENT prod(en)(a: [below(en) -> negint]) HAS_TYPE posint varprod_negint_seq2: JUDGEMENT prod(on)(a: [below(on) -> negint]) HAS_TYPE negint END products \$\$\$products.prf (|products| (|times_assoc_commutes| "" (GRIND) NIL NIL) (|prod_once_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_once| "" (GRIND) NIL NIL) (|prod_step_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_step| "" (AUTO-REWRITE "prod" "iter_induct[real]" "mult") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_same_elements| "" (EXPAND "prod") (("" (SKOSIMP) (("" (REWRITE "iter_same_elements") (("" (DELETE 2) (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_split_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_split_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|prod_split| "" (SKOSIMP) (("" (EXPAND "prod") (("" (USE "iter_assoc_split[real]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|prod_split2| "" (SKOSIMP) (("" (AUTO-REWRITE "prod") (("" (ASSERT) (("" (USE "iter_split" ("u" "u!1" "v" "v!1")) NIL NIL)) NIL)) NIL)) NIL) (|prod_permutation_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_permutation_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|prod_permutation| "" (SKOSIMP) (("" (EXPAND "prod") (("" (REWRITE "iter_permutation") NIL NIL)) NIL)) NIL) (|prod_const_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_const| "" (SKOLEM + (_ "n!1" "x!1")) (("" (INDUCT-AND-REWRITE "m" 1 "prod_once" "prod_step" "expt") NIL NIL)) NIL) (|prod_closure| "" (SKOSIMP) (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES P!1(prod(n!1, n!1+i)(u!1))") (("1" (INST - "m!1 -n!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step") (("2" (TYPEPRED "P!1") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_positive| "" (SKOSIMP) (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES prod(n!1, n!1 + i)(u!1) > 0") (("1" (INST - "m!1 -n!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step" "pos_times_gt") NIL NIL)) NIL)) NIL)) NIL) (|prod_negative| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES IF even?(i) THEN prod(n!1, n!1 + i)(u!1) < 0 ELSE prod(n!1, n!1 + i)(u!1) > 0 ENDIF") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod_once" "prod_step" "pos_times_gt" "neg_times_lt" "parity_zero") (("2" (INDUCT "i") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP) (("2" (REWRITE "incr_even" +) (("2" (REWRITE "odd_not_even" +) (("2" (ASSERT) (("2" (STOP-REWRITE "prod_step") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_negative1| "" (SKOSIMP) (("" (USE "prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_negative2| "" (SKOSIMP) (("" (REWRITE "odd_not_even") (("" (USE "prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|prod_null| "" (SKOSIMP*) (("" (EXPAND "prod") (("" (ASSERT) (("" (USE "iter_swap_last[real]" ("i" "i!1")) (("" (ASSERT) (("" (REPLACE -1 + RL) (("" (DELETE -1) (("" (AUTO-REWRITE "iter" "swap") (("" (CASE "n!1 = m!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_null2| "" (SKOSIMP) (("" (GROUND) (("1" (USE "prod_closure" ("P" "lambda x: x /= 0")) (("1" (GROUND) (("1" (DELETE -) (("1" (SKOSIMP) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REWRITE "zero_times3") NIL NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "prod_null") NIL NIL)) NIL)) NIL) (|prod_posreal_seq_is_posreal| "" (SKOLEM!) (("" (USE "prod_positive") (("" (SPLIT -) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (DELETE 2) (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prod_nzreal_seq_is_nzreal| "" (SKOSIMP) (("" (REWRITE "prod_null2") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|prod_nnreal_seq_is_nnreal| "" (SKOSIMP) (("" (USE* "prod_positive" "prod_null") (("" (GROUND) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_rat_seq_is_rat| "" (SKOLEM!) (("" (AUTO-REWRITE "rationals.closed_times") (("" (REWRITE "prod_closure") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prod_posrat_seq_is_posrat| "" (SKOLEM!) (("" (USE* "prod_rat_seq_is_rat" "prod_posreal_seq_is_posreal") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_nzrat_seq_is_nzrat| "" (SKOLEM!) (("" (USE* "prod_rat_seq_is_rat" "prod_nzreal_seq_is_nzreal") NIL NIL)) NIL) (|prod_nnrat_seq_is_nnrat| "" (SKOLEM!) (("" (USE* "prod_rat_seq_is_rat" "prod_nnreal_seq_is_nnreal") NIL NIL)) NIL) (|prod_int_seq_is_int| "" (SKOLEM!) (("" (ASSERT) (("" (USE "prod_closure" ("P" "lambda x: rational_pred(x) AND integer_pred(x)")) (("1" (ASSERT) NIL NIL) ("2" (AUTO-REWRITE "closed_times") (("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_posnat_seq_is_posnat| "" (SKOLEM!) (("" (USE* "prod_int_seq_is_int" "prod_posreal_seq_is_posreal") (("" (GROUND) NIL NIL)) NIL)) NIL) (|prod_nzint_seq_is_nzint| "" (SKOLEM!) (("" (USE* "prod_int_seq_is_int" "prod_nzreal_seq_is_nzreal") NIL NIL)) NIL) (|prod_nat_seq_is_nat| "" (SKOLEM!) (("" (USE* "prod_int_seq_is_int" "prod_nnreal_seq_is_nnreal") NIL NIL)) NIL) (|prod_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|prod_TCC3| "" (TERMINATION-TCC) NIL NIL) (|prod_TCC4| "" (SUBTYPE-TCC) NIL NIL) (|variant_prod_zero| "" (GRIND) NIL NIL) (|variant_prod_one_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|variant_prod_one| "" (GRIND) NIL NIL) (|variant_prod_two_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|variant_prod_two_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|variant_prod_two| "" (GRIND) NIL NIL) (|variant_prod_equiv| "" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (CASE-REPLACE "j!1 = 0") (("1" (DELETE -) (("1" (GRIND) NIL NIL)) NIL) ("2" (AUTO-REWRITE "prod_step") (("2" (ASSERT) (("2" (EXPAND "prod" 2 1) (("2" (INST?) (("2" (CASE "prod(0, j!1 - 1)((LAMBDA (i: nat): IF i < j!1 THEN a!1(i) ELSE 1 ENDIF)) = prod(0, j!1 - 1)(LAMBDA (i: nat): IF i < 1 + j!1 THEN a!1(i) ELSE 1 ENDIF)") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 3) (("2" (REWRITE "prod_same_elements") NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|variant_prod_split| "" (INDUCT-AND-REWRITE "n" 1 "prod") NIL NIL) (|variant_prod_permutation| "" (SKOSIMP) (("" (REWRITE "variant_prod_equiv") (("" (REWRITE "variant_prod_equiv") (("" (USE "prod_permutation" ("n" "0" "m" "n!1")) (("" (GROUND) (("" (DELETE 2) (("" (USE "perm_equiv[real]") (("" (ASSERT) (("" (DELETE 2) (("" (INST + "lambda (i: idx(0, n!1)): IF i y!1") (("1" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) NIL NIL) ("2" (REWRITE "divides_opposite" :DIR RL) (("2" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) NIL NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "divides_zero") (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|aux_prop| "" (SKOSIMP*) (("" (GROUND) (("" (REWRITE "same_remainder") (("" (USE "divides_prod_prime1" ("b" "x!1 - y!1")) (("" (ASSERT) (("" (REWRITE "div_diff_mod") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|equal_products| "" (SKOSIMP) (("" (EXPAND* "G" "F") (("" (ASSERT) (("" (USE "prod_permutation" ("m" "n!1 - 2")) (("" (GROUND) (("" (DELETE 2) (("" (USE "perm_equiv[real]" ("m" "n!1 - 2")) (("" (ASSERT) (("" (DELETE 2) (("" (FORWARD-CHAIN "aux_prop") (("" (INST + "lambda (i: idx(1, n!1 - 1)): rem(n!1)(a!1 * i)") (("1" (GROUND) (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST - "0" "i!1") (("2" (AUTO-REWRITE "rem_zero") (("2" (ASSERT) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fact_prime_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|fact_prime| "" (SKOLEM!) (("" (EXPAND "F") (("" (NAME-REPLACE "u!1" "lambda i: i" :HIDE? NIL) (("" (CASE "FORALL (j: nat): j <= p!1 - 2 IMPLIES prod(1, 1 + j)(u!1) > 0 AND prime(prod(1, 1 + j)(u!1), p!1)") (("1" (INST - "p!1-2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "pos_times_gt" "smaller_than_prime") (("1" (REPLACE -2 + RL) (("1" (ASSERT) NIL NIL)) NIL) ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL NIL)) NIL) ("3" (REWRITE "mutual_prime_prod") (("1" (REPLACE -4 + RL) (("1" (ASSERT) NIL NIL)) NIL) ("2" (REPLACE -4 + RL) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (REPLACE -4 + RL) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fermat_theorem1_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|fermat_theorem1| "" (AUTO-REWRITE "fact_prime" "equal_products" "fact_prime_TCC1") (("" (SKOSIMP) (("" (USE "decomp_G" ("n" "p!1")) (("" (ASSERT) (("" (ASSERT) (("" (REWRITE "same_remainder") (("" (USE "divides_prod_prime1" ("a" "F(p!1)" "b" "1 - expt(a!1, p!1 - 1)")) (("1" (ASSERT) (("1" (REWRITE "divides_opposite" :DIR RL +) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fermat_theorem2| "" (AUTO-REWRITE "rem_one") (("" (SKOSIMP :PREDS? T) (("" (GROUND) (("" (DELETE -1 -2 -3 1) (("" (FORWARD-CHAIN "fermat_theorem1") (("" (REWRITE "same_remainder" :DIR RL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fermat_theorem3| "" (SKOLEM!) (("" (USE "non_multiple_of_prime" ("p" "p!1" "a" "a!1")) (("" (GROUND) (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero") (("1" (CASE-REPLACE "rem(p!1)(a!1) = 0") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "rem_def2") NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "mutual_primes_commutes") (("2" (EXPAND "expt") (("2" (REWRITE "rem_prod2" :DIR RL) (("2" (REWRITE "fermat_theorem2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))