%% div.elf - Divisibility on Natural Numbers
%%
%% We define:
%%   - divides D N: D divides N (D | N), meaning N = D * K for some K

%% ============================================================
%% DIVISIBILITY
%% ============================================================

%% D divides N if there exists K such that D * K = N
divides : nat -> nat -> type.

divides/intro : divides D N
                 <- mult D K N.

%% ============================================================
%% BASIC DIVISIBILITY FACTS
%% ============================================================

%% 1 divides everything: 1 | N
one-divides : {N:nat} divides (s z) N -> type.
%mode one-divides +N -D.

one-divides/base : one-divides N (divides/intro Dmult)
                    <- mult-left-one N Dmult.

%worlds () (one-divides _ _).
%total {} (one-divides _ _).

%% Everything divides 0: N | 0
divides-zero : {N:nat} divides N z -> type.
%mode divides-zero +N -D.

%% For any N, mult N z z holds (mult/z pattern doesn't work here)
%% We need to use mult-right-z
divides-zero/base : divides-zero N (divides/intro D)
                     <- mult-right-z N D.

%worlds () (divides-zero _ _).
%total {} (divides-zero _ _).

%% N divides itself: N | N (reflexivity)
divides-refl : {N:nat} divides N N -> type.
%mode divides-refl +N -D.

divides-refl/base : divides-refl N (divides/intro Dmult)
                     <- mult-right-one N Dmult.

%worlds () (divides-refl _ _).
%total {} (divides-refl _ _).

%% ============================================================
%% DIVISION WITH REMAINDER (EUCLIDEAN DIVISION)
%% ============================================================

%% For D > 0 and any N, there exist unique Q, R with N = D*Q + R and R < D
%% We represent this as: divmod N D Q R means N = D*Q + R and R < D

divmod : nat -> nat -> nat -> nat -> type.

%% Base case: if N < D, then Q = 0, R = N
divmod/lt : divmod N D z N
             <- lt N D.

%% Recursive case: if N >= D, we need to compute (N - D) div D
%% This requires a subtraction relation, which we'll define

%% Subtraction: sub A B C means A = B + C (so C = A - B when B <= A)
sub : nat -> nat -> nat -> type.
sub/z : sub N z N.
sub/s : sub (s A) (s B) C
         <- sub A B C.

%% Now we can define divmod for the recursive case
divmod/ge : divmod N D (s Q) R
             <- le D N                    %% D <= N
             <- sub N D M                 %% M = N - D
             <- divmod M D Q R.           %% M = D*Q + R, so N = D*(Q+1) + R

%% ============================================================
%% GCD (Greatest Common Divisor)
%% ============================================================

%% Euclidean algorithm: gcd(A, 0) = A, gcd(A, B) = gcd(B, A mod B)
%% We define gcd using the Euclidean algorithm

%% gcd A B G means G is the GCD of A and B
gcd : nat -> nat -> nat -> type.

gcd/z : gcd A z A.                       %% gcd(A, 0) = A

gcd/s : gcd A (s B) G
         <- divmod A (s B) Q R           %% A = (s B)*Q + R with R < s B
         <- gcd (s B) R G.               %% G = gcd(s B, R)

%% ============================================================
%% COPRIMALITY
%% ============================================================

%% A and B are coprime if gcd(A, B) = 1
coprime : nat -> nat -> type.
coprime/intro : coprime A B
                 <- gcd A B (s z).