124 lines
3.8 KiB
Plaintext
124 lines
3.8 KiB
Plaintext
%% theorems.elf - Verified Computations and Theorem Summary
|
|
%%
|
|
%% This file demonstrates computational verification using %solve
|
|
%% and summarizes the proof status of all theorems.
|
|
|
|
%% ============================================================
|
|
%% COMPUTATIONAL VERIFICATIONS
|
|
%% ============================================================
|
|
|
|
%% Basic arithmetic
|
|
%solve add-2-3 : add two three N.
|
|
%% Result: N = five
|
|
|
|
%solve add-3-2 : add three two N.
|
|
%% Result: N = five (commutativity)
|
|
|
|
%solve mult-2-3 : mult two three N.
|
|
%% Result: N = s (s (s (s (s (s z))))) = 6
|
|
|
|
%solve mult-3-2 : mult three two N.
|
|
%% Result: N = 6 (commutativity)
|
|
|
|
%% Exponentiation
|
|
%solve exp-2-3 : exp two three N.
|
|
%% Result: N = 8
|
|
|
|
%solve exp-3-2 : exp three two N.
|
|
%% Result: N = 9
|
|
|
|
%% Factorial (defined in prime.elf)
|
|
%solve fact-3 : factorial three N.
|
|
%% Result: N = 6
|
|
|
|
%solve fact-4 : factorial four N.
|
|
%% Result: N = 24
|
|
|
|
%% Order relations
|
|
%solve two-lt-five : lt two five.
|
|
%% Result: lt/s (lt/s lt/z)
|
|
|
|
%solve three-le-three : le three three.
|
|
%% Result: le/s (le/s (le/s le/z))
|
|
|
|
%% Divisibility
|
|
%solve two-div-four : divides two four.
|
|
%% Result: divides/intro (mult two two four)
|
|
|
|
%% ============================================================
|
|
%% VERIFIED THEOREMS (Twelf %total checked)
|
|
%% ============================================================
|
|
|
|
%% From nat.elf:
|
|
%% nat-case-total: every nat is z or s of something
|
|
|
|
%% From add.elf:
|
|
%% add-total: addition always produces a result
|
|
%% add-right-z: N + 0 = N
|
|
%% add-right-s: M + (S N) = S(M + N)
|
|
%% add-comm: M + N = N + M
|
|
%% add-assoc: (A + B) + C = A + (B + C)
|
|
%% add-cancel-left: A + B = A + C implies B = C
|
|
%% add-func: addition is deterministic
|
|
|
|
%% From mult.elf:
|
|
%% mult-total: multiplication always produces a result
|
|
%% mult-right-z: N * 0 = 0
|
|
%% mult-left-one: 1 * N = N
|
|
%% mult-right-one: N * 1 = N
|
|
|
|
%% From exp.elf:
|
|
%% exp-total: exponentiation always produces a result
|
|
%% exp-one: N^1 = N
|
|
%% exp-base-one: 1^N = 1
|
|
%% exp-base-zero: 0^(S N) = 0
|
|
|
|
%% From order.elf:
|
|
%% le-refl: N <= N
|
|
%% le-trans: A <= B and B <= C implies A <= C
|
|
%% le-antisym: A <= B and B <= A implies A = B
|
|
%% lt-to-le: A < B implies A <= B
|
|
%% lt-s-to-le: A < S(B) implies A <= B
|
|
%% le-to-lt-s: A <= B implies A < S(B)
|
|
%% trichotomy-total: for all M, N: M < N or M = N or M > N
|
|
%% lt-trans: A < B and B < C implies A < C
|
|
|
|
%% From div.elf:
|
|
%% one-divides: 1 | N for all N
|
|
%% divides-zero: N | 0 for all N
|
|
%% divides-refl: N | N for all N
|
|
|
|
%% From prime.elf:
|
|
%% factorial-total: factorial always produces a result
|
|
|
|
%% ============================================================
|
|
%% THEOREMS STATED BUT NOT FULLY PROVEN
|
|
%% ============================================================
|
|
|
|
%% Multiplication:
|
|
%% mult-comm: M * N = N * M
|
|
%% (Requires mult-right-s lemma with careful
|
|
%% associativity/commutativity reasoning)
|
|
%%
|
|
%% mult-assoc: (A * B) * C = A * (B * C)
|
|
%% (Requires distributivity)
|
|
%%
|
|
%% mult-distrib-l: A * (B + C) = A*B + A*C
|
|
%% (Provable with induction on A)
|
|
|
|
%% Number theory:
|
|
%% has-prime-divisor-total: every N > 1 has a prime divisor
|
|
%% (Requires strong/well-founded induction)
|
|
%%
|
|
%% infinitude-of-primes: for any prime P, there exists prime Q > P
|
|
%% (Classic Euclidean proof using factorial)
|
|
%%
|
|
%% euclid-lemma: if P prime and P | AB then P | A or P | B
|
|
%% (Requires Bezout's identity or equivalent)
|
|
%%
|
|
%% fundamental-theorem-existence: every N > 1 has prime factorization
|
|
%% (Follows from has-prime-divisor with induction)
|
|
%%
|
|
%% fundamental-theorem-uniqueness: prime factorization is unique
|
|
%% (Requires Euclid's lemma)
|