% -----------------------------------------------------------------------------
%
% reasoning.txt
% Reasoning with the RISC ProofNavigator.
%
% (c) 2015, Wolfgang Schreiner: Thinking Programs.
%
% -----------------------------------------------------------------------------
newcontext "reasoning";

% -----------------------------------------------------------------------------
% Part 1: a direct proof
% -----------------------------------------------------------------------------

% an abstract type with some predicates
T: TYPE;
p: T -> BOOLEAN;
q: T -> BOOLEAN;
r: (T,T) -> BOOLEAN;

% a valid formula
F: FORMULA 
  (FORALL(x:T): p(x) OR r(x,x)) AND
  (FORALL(x:T): p(x) => (EXISTS(y:T): q(y))) AND
  (FORALL(x,y:T): p(x) AND q(y) => r(x,y)) =>
    (FORALL(x:T): EXISTS(y:T): r(x,y));

% -----------------------------------------------------------------------------
% Part 2: an indirect proof
% (Euclid's proof that there exist infinitely many primes)
% ----------------------------------------------------------------------------- 

% predicates "divides" and "isprime" 
divides:  (NAT,NAT)->BOOLEAN;
prime:    NAT->BOOLEAN;

% the product of all primes up to a given bound
pproduct: NAT->NAT;

% the knowledge needed for Euclid's proof
P1: AXIOM FORALL(n:NAT, m:NAT): n > 1 AND divides(n,m) => NOT divides(n,m+1);
P2: AXIOM prime(2) AND (FORALL(n:NAT): n < 2 => NOT prime(n));
P3: AXIOM FORALL(n:NAT): n > 1 => (EXISTS(p:NAT): prime(p) AND divides(p,n));
P4: AXIOM pproduct(2) = 2 AND (FORALL(n:NAT): n > 2 => pproduct(n) > n);
P5: AXIOM FORALL(n:NAT,p:NAT): p <= n AND prime(p) => divides(p,pproduct(n));
     
% there exist infinitely many prime numbers
P: FORMULA NOT (EXISTS(n:NAT): (FORALL(p:NAT): prime(p) => p <= n));

% -----------------------------------------------------------------------------
% Part 3: an induction proof
% ----------------------------------------------------------------------------- 

% the recursive definition of the sum from 0 to n
sum: NAT->NAT;
S1: AXIOM sum(0)=0;
S2: AXIOM FORALL(n:NAT): n>0 => sum(n)=n+sum(n-1);

% proof that explicit form is equivalent to recursive definition
S: FORMULA FORALL(n:NAT): sum(n) = (n+1)*n/2;
       
% -----------------------------------------------------------------------------
% end of file
% -----------------------------------------------------------------------------