%% order.elf - Ordering Relations on Natural Numbers
%%
%% We define:
%%   - lt (less than): M < N
%%   - le (less than or equal): M <= N

%% ============================================================
%% LESS THAN
%% ============================================================

%% M < N is defined inductively:
%% - 0 < S(N) for any N
%% - S(M) < S(N) if M < N

lt : nat -> nat -> type.

lt/z : lt z (s N).                    %% 0 < S(N) for any N
lt/s : lt (s M) (s N)                 %% S(M) < S(N) if M < N
        <- lt M N.

%% ============================================================
%% LESS THAN OR EQUAL
%% ============================================================

le : nat -> nat -> type.

le/z : le z N.                        %% 0 <= N for any N
le/s : le (s M) (s N)                 %% S(M) <= S(N) if M <= N
        <- le M N.

%% le is reflexive
le-refl : {N:nat} le N N -> type.
%mode le-refl +N -D.
le-refl/z : le-refl z le/z.
le-refl/s : le-refl (s N) (le/s D)
             <- le-refl N D.
%worlds () (le-refl _ _).
%total N (le-refl N _).

%% le is transitive
le-trans : le A B -> le B C -> le A C -> type.
%mode le-trans +D1 +D2 -D3.

le-trans/z : le-trans le/z _ le/z.
le-trans/s : le-trans (le/s D1) (le/s D2) (le/s D3)
              <- le-trans D1 D2 D3.

%worlds () (le-trans _ _ _).
%total D (le-trans D _ _).

%% Helper: equality lifts through successor
nat-eq-s' : nat-eq M N -> nat-eq (s M) (s N) -> type.
%mode nat-eq-s' +E1 -E2.
nat-eq-s'/refl : nat-eq-s' nat-eq/refl nat-eq/refl.
%worlds () (nat-eq-s' _ _).
%total {} (nat-eq-s' _ _).

%% le is antisymmetric: if M <= N and N <= M then M = N
le-antisym : le M N -> le N M -> nat-eq M N -> type.
%mode le-antisym +D1 +D2 -E.

le-antisym/z : le-antisym le/z le/z nat-eq/refl.
le-antisym/s : le-antisym (le/s D1) (le/s D2) E
                <- le-antisym D1 D2 E'
                <- nat-eq-s' E' E.

%worlds () (le-antisym _ _ _).
%total D (le-antisym D _ _).

%% ============================================================
%% RELATIONSHIPS BETWEEN lt AND le
%% ============================================================

%% lt implies le: if M < N then M <= N
lt-to-le : lt M N -> le M N -> type.
%mode lt-to-le +D1 -D2.

lt-to-le/z : lt-to-le lt/z le/z.
lt-to-le/s : lt-to-le (lt/s D1) (le/s D2)
              <- lt-to-le D1 D2.

%worlds () (lt-to-le _ _).
%total D (lt-to-le D _).

%% M < S(N) iff M <= N
lt-s-to-le : lt M (s N) -> le M N -> type.
%mode lt-s-to-le +D1 -D2.

lt-s-to-le/z : lt-s-to-le lt/z le/z.
lt-s-to-le/s : lt-s-to-le (lt/s D1) (le/s D2)
                <- lt-s-to-le D1 D2.

%worlds () (lt-s-to-le _ _).
%total D (lt-s-to-le D _).

le-to-lt-s : le M N -> lt M (s N) -> type.
%mode le-to-lt-s +D1 -D2.

le-to-lt-s/z : le-to-lt-s le/z lt/z.
le-to-lt-s/s : le-to-lt-s (le/s D1) (lt/s D2)
                <- le-to-lt-s D1 D2.

%worlds () (le-to-lt-s _ _).
%total D (le-to-lt-s D _).

%% ============================================================
%% TRICHOTOMY
%% ============================================================

%% For any M, N: exactly one of M < N, M = N, M > N holds

trichotomy : nat -> nat -> type.
trichotomy/lt : trichotomy M N <- lt M N.
trichotomy/eq : trichotomy M N <- nat-eq M N.
trichotomy/gt : trichotomy M N <- lt N M.

%% Helper to lift trichotomy through successor
trichotomy-lift : trichotomy M N -> trichotomy (s M) (s N) -> type.
%mode trichotomy-lift +T1 -T2.

trichotomy-lift/lt : trichotomy-lift (trichotomy/lt D) (trichotomy/lt (lt/s D)).
trichotomy-lift/eq : trichotomy-lift (trichotomy/eq nat-eq/refl)
                      (trichotomy/eq nat-eq/refl).
trichotomy-lift/gt : trichotomy-lift (trichotomy/gt D) (trichotomy/gt (lt/s D)).

%worlds () (trichotomy-lift _ _).
%total {} (trichotomy-lift _ _).

trichotomy-total : {M:nat} {N:nat} trichotomy M N -> type.
%mode trichotomy-total +M +N -T.

trichotomy-total/zz : trichotomy-total z z (trichotomy/eq nat-eq/refl).
trichotomy-total/zs : trichotomy-total z (s N) (trichotomy/lt lt/z).
trichotomy-total/sz : trichotomy-total (s M) z (trichotomy/gt lt/z).
trichotomy-total/ss : trichotomy-total (s M) (s N) T'
                       <- trichotomy-total M N T
                       <- trichotomy-lift T T'.

%worlds () (trichotomy-total _ _ _).
%total M (trichotomy-total M _ _).

%% ============================================================
%% BASIC LEMMAS
%% ============================================================

%% lt is transitive
lt-trans : lt A B -> lt B C -> lt A C -> type.
%mode lt-trans +D1 +D2 -D3.

lt-trans/zs : lt-trans lt/z (lt/s _) lt/z.
lt-trans/ss : lt-trans (lt/s D1) (lt/s D2) (lt/s D3)
               <- lt-trans D1 D2 D3.

%worlds () (lt-trans _ _ _).
%total D (lt-trans D _ _).

%% lt is irreflexive: not (N < N)
%% We express this as: lt N N implies any conclusion
%% (In Twelf, we can't directly state "not", but we can show
%% there's no derivation of lt N N)

%% N is not less than zero - this is witnessed by the fact that
%% there is no constructor for lt that produces lt _ z.
%% We cannot state "lt N z -> void" directly in Twelf since void
%% isn't a built-in. Instead, the absence of matching cases proves it.