Natural numbers with inequality

A signature for natural numbers, adapted from a number of sources, in particular the TALT project. There is no arithmetic, just the theory of inequality. This code uses an uninhabited type, “void”, in order to express proofs by reductio ad absurdum.

Syntax

Natural numbers

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.

The uninhabited type

%sort void %.
%freeze void %.

Constants

%define 0 z %.
%define 1 s 0 %.

… and continuing on to 25

Equality and inequality

Definitions

%% equality
%sort id-nat {_ nat} {_ nat} %.
%term id-nat/refl id-nat N N %.
%% less than
%sort lt-nat {_ nat} {_ nat} %.
%term lt-nat/z lt-nat z (s N) %.
%term lt-nat/s %pi (lt-nat (s N1) (s N2)) %<- (lt-nat N1 N2) %.
%% less than or equal to
%sort leq-nat {_ nat} {_ nat} %.
%term leq-nat/eq %pi (leq-nat N1 N2) %<- (id-nat N1 N2) %.
%term leq-nat/lt %pi (leq-nat N1 N2) %<- (lt-nat N1 N2) %.
%% not equal
%sort neq-nat {_ nat} {_ nat} %.
%term neq-nat/gt %pi (neq-nat N1 N2) %<- (lt-nat N2 N1) %.
%term neq-nat/lt %pi (neq-nat N1 N2) %<- (lt-nat N1 N2) %.

Theorems

False implies anything

%sort false-imp-id-nat {_ void} {N1} {N2} {_ id-nat N1 N2} %.
%mode false-imp-id-nat %in %in %in %out %.
%worlds () (false-imp-id-nat _ _ _ _) %.
%total {} (false-imp-id-nat _ _ _ _) %.
%sort false-imp-neq-nat {_ void} {N1} {N2} {_ neq-nat N1 N2} %.
%mode false-imp-neq-nat %in %in %in %out %.
%worlds () (false-imp-neq-nat _ _ _ _) %.
%total {} (false-imp-neq-nat _ _ _ _) %.
%sort false-imp-lt-nat {_ void} {N1} {N2} {_ lt-nat N1 N2} %.
%mode false-imp-lt-nat %in %in %in %out %.
%worlds () (false-imp-lt-nat _ _ _ _) %.
%total {} (false-imp-lt-nat _ _ _ _) %.
%sort false-imp-leq-nat {_ void} {N1} {N2} {_ leq-nat N1 N2} %.
%mode false-imp-leq-nat %in %in %in %out %.
%worlds () (false-imp-leq-nat _ _ _ _) %.
%total {} (false-imp-leq-nat _ _ _ _) %.

Basic properties

%sort lt-nat-succ {N} {_ lt-nat N (s N)} %.
%mode lt-nat-succ %in %out %.
%term _ lt-nat-succ z lt-nat/z %.
%term _ %pi (lt-nat-succ (s N) (lt-nat/s D)) %<- (lt-nat-succ N D) %.
%worlds () (lt-nat-succ _ _) %.
%total T (lt-nat-succ T _) %.

Reflexivity and symmetry

%sort id-nat/symm {_ id-nat N1 N2} {_ id-nat N2 N1} %.
%mode id-nat/symm %in %out %.
%term _ id-nat/symm id-nat/refl id-nat/refl %.
%worlds () (id-nat/symm _ _) %.
%total {} (id-nat/symm _ _) %.
%sort id-nat/trans {_ id-nat N1 N2} {_ id-nat N2 N3} {_ id-nat N1 N3} %.
%mode id-nat/trans %in %in %out %.
%term _ id-nat/trans id-nat/refl id-nat/refl id-nat/refl %.
%worlds () (id-nat/trans _ _ _) %.
%total {} (id-nat/trans _ _ _) %.
%sort neq-nat/symm {_ neq-nat N1 N2} {_ neq-nat N2 N1} %.
%mode neq-nat/symm %in %out %.
%term _ neq-nat/symm (neq-nat/lt D) (neq-nat/gt D) %.
%term _ neq-nat/symm (neq-nat/gt D) (neq-nat/lt D) %.
%worlds () (neq-nat/symm _ _) %.
%total {} (neq-nat/symm _ _) %.
%sort lt-nat/trans {_ lt-nat N1 N2} {_ lt-nat N2 N3} {_ lt-nat N1 N3} %.
%mode lt-nat/trans %in %in %out %.
%term _ lt-nat/trans lt-nat/z _ lt-nat/z %.
%term _
  %pi (lt-nat/trans (lt-nat/s D1) (lt-nat/s D2) (lt-nat/s D3))
  %<- (lt-nat/trans D1 D2 D3) %.
%worlds () (lt-nat/trans _ _ _) %.
%total T (lt-nat/trans T _ _) %.
%sort leq-nat/trans {_ leq-nat N1 N2} {_ leq-nat N2 N3} {_ leq-nat N1 N3} %.
%mode leq-nat/trans %in %in %out %.
%term _ leq-nat/trans (leq-nat/eq _) D D %.
%term _ leq-nat/trans D (leq-nat/eq _) D %.
%term _
  %pi (leq-nat/trans (leq-nat/lt D1) (leq-nat/lt D2) (leq-nat/lt D3))
  %<- (lt-nat/trans D1 D2 D3) %.
%worlds () (leq-nat/trans _ _ _) %.
%total {} (leq-nat/trans _ _ _) %.

Respects lemmas

This is an instance of the generalization technique described in the page on respects lemmas.

%sort id-nat/compat {F %pi nat %-> nat} {_ id-nat N1 N2} {_ id-nat (F N1) (F N2)} %.
%mode id-nat/compat %in %in %out %.
%term _ id-nat/compat _ id-nat/refl id-nat/refl %.
%worlds () (id-nat/compat _ _ _) %.
%total {} (id-nat/compat _ _ _) %.
%inline id-nat/inc (%pi (id-nat N1 N2) %-> (id-nat (s N1) (s N2)) %-> %type) id-nat/compat s %.
%sort id-nat/dec {_ id-nat (s N1) (s N2)} {_ id-nat N1 N2} %.
%mode id-nat/dec %in %out %.
%term _ id-nat/dec id-nat/refl id-nat/refl %.
%worlds () (id-nat/dec _ _) %.
%total {} (id-nat/dec _ _) %.
%sort leq-nat-resp {_ id-nat N1 N1'} {_ id-nat N2 N2'} {_ leq-nat N1 N2} {_ leq-nat N1' N2'} %.
%mode leq-nat-resp %in %in %in %out %.
%term _ leq-nat-resp id-nat/refl id-nat/refl D D %.
%worlds () (leq-nat-resp _ _ _ _) %.
%total {} (leq-nat-resp _ _ _ _) %.
%sort lt-nat-resp {_ id-nat N1 N1'} {_ id-nat N2 N2'} {_ lt-nat N1 N2} {_ lt-nat N1' N2'} %.
%mode lt-nat-resp %in %in %in %out %.
%term _ lt-nat-resp id-nat/refl id-nat/refl D D %.
%worlds () (lt-nat-resp _ _ _ _) %.
%total {} (lt-nat-resp _ _ _ _) %.
%sort neq-nat-resp {_ id-nat N1 N1'} {_ id-nat N2 N2'} {_ neq-nat N1 N2} {_ neq-nat N1' N2'} %.
%mode neq-nat-resp %in %in %in %out %.
%term _ neq-nat-resp id-nat/refl id-nat/refl D D %.
%worlds () (neq-nat-resp _ _ _ _) %.
%total {} (neq-nat-resp _ _ _ _) %.

Contradictions

%sort lt-nat-contr {_ lt-nat N N} {_ void} %.
%mode lt-nat-contr %in %out %.
%term _ %pi (lt-nat-contr (lt-nat/s D) F) %<- (lt-nat-contr D F) %.
%worlds () (lt-nat-contr _ _) %.
%total T (lt-nat-contr T _) %.
%sort neq-nat-contr {_ neq-nat N N} {_ void} %.
%mode neq-nat-contr %in %out %.
%term _ %pi (neq-nat-contr (neq-nat/lt D) F) %<- (lt-nat-contr D F) %.
%term _ %pi (neq-nat-contr (neq-nat/gt D) F) %<- (lt-nat-contr D F) %.
%worlds () (neq-nat-contr _ _) %.
%total T (neq-nat-contr T _) %.
%sort lt-gt-nat-contr {_ lt-nat N1 N2} {_ lt-nat N2 N1} {_ void} %.
%mode lt-gt-nat-contr %in %in %out %.
%term _ %pi (lt-gt-nat-contr (lt-nat/s D1) (lt-nat/s D2) F) %<- (lt-gt-nat-contr D1 D2 F) %.
%worlds () (lt-gt-nat-contr _ _ _) %.
%total T (lt-gt-nat-contr T _ _) %.
%sort lt-leq-nat-contr {_ lt-nat N1 N2} {_ leq-nat N2 N1} {_ void} %.
%mode lt-leq-nat-contr %in %in %out %.
%term _ %pi (lt-leq-nat-contr D1 (leq-nat/lt D2) F) %<- (lt-gt-nat-contr D1 D2 F) %.
%term _ %pi (lt-leq-nat-contr D1 (leq-nat/eq D2) F) %<- (lt-nat-contr D1 F) %.
%worlds () (lt-leq-nat-contr _ _ _) %.
%total T (lt-leq-nat-contr T _ _) %.

Dichotomy

The property that any two numbers are comparable by lt, eq, or lt the other way around. Because leq and neq are defined in terms of lt and eq, this should allow relatively simple assessment of these cases as well.

%sort dichotomy-nat {_ nat} {_ nat} %.
%term dichotomy-nat/lt %pi (lt-nat N1 N2) %-> (dichotomy-nat N1 N2) %.
%term dichotomy-nat/gt %pi (lt-nat N1 N2) %-> (dichotomy-nat N2 N1) %.
%term dichotomy-nat/id %pi (id-nat N1 N2) %-> (dichotomy-nat N1 N2) %.
%sort can-dichotomy-nat/s {_ dichotomy-nat N1 N2} {_ dichotomy-nat (s N1) (s N2)} %.
%mode can-dichotomy-nat/s %in %out %.
%term _ can-dichotomy-nat/s (dichotomy-nat/gt D) (dichotomy-nat/gt (lt-nat/s D)) %.
%term _ can-dichotomy-nat/s (dichotomy-nat/lt D) (dichotomy-nat/lt (lt-nat/s D)) %.
%term _
  %pi (can-dichotomy-nat/s (dichotomy-nat/id D) (dichotomy-nat/id D'))
  %<- (id-nat/inc D D') %.
%worlds () (can-dichotomy-nat/s _ _) %.
%total {} (can-dichotomy-nat/s _ _) %.
%sort can-dichotomy-nat {N1} {N2} {_ dichotomy-nat N1 N2} %.
%mode can-dichotomy-nat %in %in %out %.
%term _ can-dichotomy-nat z z (dichotomy-nat/id id-nat/refl) %.
%term _ can-dichotomy-nat (s _) z (dichotomy-nat/gt lt-nat/z) %.
%term _ can-dichotomy-nat z (s _) (dichotomy-nat/lt lt-nat/z) %.
%term _
  %pi (can-dichotomy-nat (s N1) (s N2) D')
  %<- (can-dichotomy-nat N1 N2 D)
  %<- (can-dichotomy-nat/s D D') %.
%worlds () (can-dichotomy-nat _ _ _) %.
%total T (can-dichotomy-nat T _ _) %.