Natural numbers with inequality

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

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

nat: type.
z: nat.
s: nat -> nat.

The uninhabited type

void: type. %freeze void.

Constants

0 = z.
1 = s 0.

... and continuing on to 25

Equality and inequality

Definitions

%% equality
id-nat	    : nat -> nat -> type.
id-nat/refl : id-nat N N.

%% less than
lt-nat   : nat -> nat -> type.
lt-nat/z : lt-nat z (s N).
lt-nat/s : lt-nat (s N1) (s N2)
	    <- lt-nat N1 N2.

%% less than or equal to
leq-nat    : nat -> nat -> type.
leq-nat/eq : leq-nat N1 N2
	      <- id-nat N1 N2.
leq-nat/lt : leq-nat N1 N2
	      <- lt-nat N1 N2.

%% not equal
neq-nat : nat -> nat -> type.
neq-nat/gt : neq-nat N1 N2
	      <- lt-nat N2 N1.
neq-nat/lt : neq-nat N1 N2
	      <- lt-nat N1 N2.

Theorems

False implies anything

false-imp-id-nat : void -> {N1}{N2} id-nat N1 N2 -> type.
%mode false-imp-id-nat +X +N1 +N2 -D. 
%worlds () (false-imp-id-nat _ _ _ _).
%total {} (false-imp-id-nat _ _ _ _).



false-imp-neq-nat : void -> {N1}{N2} neq-nat N1 N2 -> type.
%mode false-imp-neq-nat +X +N1 +N2 -D. 
%worlds () (false-imp-neq-nat _ _ _ _).
%total {} (false-imp-neq-nat _ _ _ _).



false-imp-lt-nat : void -> {N1}{N2} lt-nat N1 N2 -> type.
%mode false-imp-lt-nat +X +N1 +N2 -D. 
%worlds () (false-imp-lt-nat _ _ _ _).
%total {} (false-imp-lt-nat _ _ _ _).



false-imp-leq-nat : void -> {N1}{N2} leq-nat N1 N2 -> type.
%mode false-imp-leq-nat +X +N1 +N2 -D. 
%worlds () (false-imp-leq-nat _ _ _ _).
%total {} (false-imp-leq-nat _ _ _ _).

Basic properties

lt-nat-succ : {N} lt-nat N (s N) -> type.
%mode lt-nat-succ +N -D.

- : lt-nat-succ z lt-nat/z.
- : 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

id-nat/symm : id-nat N1 N2 -> id-nat N2 N1 -> type.
%mode id-nat/symm +D1 -D2.

- : id-nat/symm id-nat/refl id-nat/refl.

%worlds () (id-nat/symm _ _).
%total {} (id-nat/symm _ _).



id-nat/trans : id-nat N1 N2 -> id-nat N2 N3 -> id-nat N1 N3 -> type.
%mode id-nat/trans +D1 +D2 -D3.

- : id-nat/trans id-nat/refl id-nat/refl id-nat/refl.

%worlds () (id-nat/trans _ _ _).
%total {} (id-nat/trans _ _ _).



neq-nat/symm : neq-nat N1 N2 -> neq-nat N2 N1 -> type.
%mode neq-nat/symm +D1 -D2.

- : neq-nat/symm (neq-nat/lt D) (neq-nat/gt D).
- : neq-nat/symm (neq-nat/gt D) (neq-nat/lt D).

%worlds () (neq-nat/symm _ _).
%total {} (neq-nat/symm _ _).



lt-nat/trans : lt-nat N1 N2 -> lt-nat N2 N3 -> lt-nat N1 N3 -> type.
%mode lt-nat/trans +D1 +D2 -D3.

- : lt-nat/trans lt-nat/z _ lt-nat/z.
- : 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 _ _).



leq-nat/trans : leq-nat N1 N2 -> leq-nat N2 N3 -> leq-nat N1 N3 -> type.
%mode leq-nat/trans +D1 +D2 -D3.

- : leq-nat/trans (leq-nat/eq _) D D.
- : leq-nat/trans D (leq-nat/eq _) D.
- : 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.

id-nat/compat : {F: nat -> nat} id-nat N1 N2 -> id-nat (F N1) (F N2) -> type.
%mode id-nat/compat +F +D1 -D2.

- : id-nat/compat _ id-nat/refl id-nat/refl.

%worlds () (id-nat/compat _ _ _).
%total {} (id-nat/compat _ _ _).



%abbrev
id-nat/inc : id-nat N1 N2 -> id-nat (s N1) (s N2) -> type = id-nat/compat s.



id-nat/dec : id-nat (s N1) (s N2) -> id-nat N1 N2 -> type.
%mode id-nat/dec +D1 -D2.

- : id-nat/dec id-nat/refl id-nat/refl.

%worlds () (id-nat/dec _ _).
%total {} (id-nat/dec _ _).



leq-nat-resp : id-nat N1 N1' 
		-> id-nat N2 N2' -> leq-nat N1 N2 -> leq-nat N1' N2' -> type.
%mode leq-nat-resp +X1 +X2 +X3 -X4.

- : leq-nat-resp id-nat/refl id-nat/refl D D.

%worlds () (leq-nat-resp _ _ _ _).
%total {} (leq-nat-resp _ _ _ _).



lt-nat-resp : id-nat N1 N1' 
	       -> id-nat N2 N2' -> lt-nat N1 N2 -> lt-nat N1' N2' -> type.
%mode lt-nat-resp +D1 +D2 +D3 -D.

- : lt-nat-resp id-nat/refl id-nat/refl D D.

%worlds () (lt-nat-resp _ _ _ _).
%total {} (lt-nat-resp _ _ _ _).



neq-nat-resp : id-nat N1 N1' 
		-> id-nat N2 N2' -> neq-nat N1 N2 -> neq-nat N1' N2' -> type.
%mode neq-nat-resp +X1 +X2 +X3 -X4.

- : neq-nat-resp id-nat/refl id-nat/refl D D.

%worlds () (neq-nat-resp _ _ _ _).
%total {} (neq-nat-resp _ _ _ _).

Contradictions

lt-nat-contr : lt-nat N N -> void -> type.
%mode lt-nat-contr +D -F.

- : lt-nat-contr (lt-nat/s D) F
     <- lt-nat-contr D F.

%worlds () (lt-nat-contr _ _).
%total T (lt-nat-contr T _).



neq-nat-contr : neq-nat N N -> void -> type.
%mode neq-nat-contr +D -F.

- : neq-nat-contr (neq-nat/lt D) F
     <- lt-nat-contr D F.
- : neq-nat-contr (neq-nat/gt D) F
     <- lt-nat-contr D F.

%worlds () (neq-nat-contr _ _).
%total T (neq-nat-contr T _).



lt-gt-nat-contr : lt-nat N1 N2 -> lt-nat N2 N1 -> void -> type.
%mode lt-gt-nat-contr +D1 +D2 -F.

- : 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 _ _).



lt-leq-nat-contr : lt-nat N1 N2 -> leq-nat N2 N1 -> void -> type.
%mode lt-leq-nat-contr +D1 +D2 -F.

- : lt-leq-nat-contr D1 (leq-nat/lt D2) F
     <- lt-gt-nat-contr D1 D2 F.
- : 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.

dichotomy-nat : nat -> nat -> type.
dichotomy-nat/lt : lt-nat N1 N2 -> dichotomy-nat N1 N2.
dichotomy-nat/gt : lt-nat N1 N2 -> dichotomy-nat N2 N1.
dichotomy-nat/id : id-nat N1 N2 -> dichotomy-nat N1 N2.

can-dichotomy-nat/s : dichotomy-nat N1 N2 
		       -> dichotomy-nat (s N1) (s N2) -> type.
%mode can-dichotomy-nat/s +D1 -D2.

- : can-dichotomy-nat/s (dichotomy-nat/gt D) (dichotomy-nat/gt (lt-nat/s D)).
- : can-dichotomy-nat/s (dichotomy-nat/lt D) (dichotomy-nat/lt (lt-nat/s D)).
- : 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 _ _).

can-dichotomy-nat : {N1}{N2} dichotomy-nat N1 N2 -> type.
%mode can-dichotomy-nat +N1 +N2 -D.

- : can-dichotomy-nat z z     (dichotomy-nat/id id-nat/refl).
- : can-dichotomy-nat (s _) z (dichotomy-nat/gt lt-nat/z).
- : can-dichotomy-nat z (s _) (dichotomy-nat/lt lt-nat/z).
- : 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 _ _).

Read more Twelf case studies and other Twelf documentation.