Natural numbers with inequality
From The Twelf Project
| 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.
Contents |
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.
