%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Short course on
% Interactively Proving Mathematical Theorems
% Summer Workshop in Mathematics UnB, 2020
%
% Exercise set on Classical HO deduction
%
% Thaynara Arielly de Lima UFG
% Mauricio Ayala-Rincon UnB
% Last modified: March 2 2020
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
pred_algebra [T:TYPE+,*:[T,T->T],e:T]
: THEORY
BEGIN
G, H: VAR set[T]
a, x, y: VAR T
n,m: nat
%---------------------------------- Basic definitions -------------------------%
closed?(G): bool = FORALL (x,y:(G)): member(x*y,G)
inv_exists?(G): bool = FORALL (x:(G)): EXISTS (y:(G)): x * y = e AND y * x = e
group?(G): bool = closed?(G) AND
associative?[(G)](*) AND
member(e,G) AND identity?[(G)](*)(e) AND
inv_exists?(G)
id_charac: CONJECTURE % Sec. 02 example
FORALL (G:(group?), x:(G)): x = e IFF x * x = x
left_cancellative: CONJECTURE % Sec. 02 exercise
FORALL (G:(group?), x,y,z:(G)): x * y = x * z IFF y = z
right_cancellative: CONJECTURE % Sec. 02 ev. exercise/HW
FORALL (G:(group?), x,y,z:(G)): y * x = z * x IFF y = z
right_unicity_id: CONJECTURE
FORALL (G: (group?), x:(G)): exists1!(y:(G)): x * y = x % HW
left_unicity_id: CONJECTURE % HW
FORALL (G: (group?), x:(G)): exists1!(y:(G)): y * x = x
abelian_group?(G): bool = group?(G) AND commutative?[(G)](*);
^(y : T ,n : nat) : RECURSIVE T =
IF n = 0 THEN e
ELSE y * ^(y, n - 1) ENDIF
MEASURE n
;
power_set(x:T): set[T] = { y: T | EXISTS (n:nat) : y = x^n }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Inductive properties of power_set (Induction Exs. for the third section)
%
%
power_closed: CONJECTURE % Sec. 03 example
FORALL (G: (group?), y: (G), n: nat): member(^(y,n),G)
power_add: CONJECTURE % Sec. 03 exercise
FORALL (G: (group?), y: (G), n,m: nat): ^(y,n) * ^(y,m) = ^(y, n+m)
power_mult: CONJECTURE % Sec. 03 Ev. exercise
FORALL (G:(group?), y:(G), m,n: nat): (y^n)^m = y^(n*m)
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
cyclic?(G): bool = group?(G) AND EXISTS (y: (G)): FORALL(x:(G)): EXISTS (n: nat): y^n = x
cyc_abel: CONJECTURE % Sec. 02 exercise
cyclic?(G) IMPLIES abelian_group?(G)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Third section on mathematical formalization
%% Classical HO deduction
%% Thaynara Arielly de Lima and Mauricio Ayala-Rincon
%% Summer Workshop in Mathematics UnB, 2020
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Revisit first inductive deductions in power_closed and power_add
% Check theory symmetric
torsion?(G): bool = group?(G) AND FORALL (y:(G)): EXISTS (n: posnat) : y^n = e
finite_torsion: CONJECTURE % Homework
FORALL (G: (group?)): is_finite(G) IMPLIES torsion?(G)
subgroup?(H:set[T],G:(group?)): bool = subset?(H,G) AND group?(H)
END pred_algebra