%{ 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 |hidden = true}% 2 = s 1. 3 = s 2. 4 = s 3. 5 = s 4. 6 = s 5. 7 = s 6. 8 = s 7. 9 = s 8. 10 = s 9. 11 = s 10. 12 = s 11. 13 = s 12. 14 = s 13. 15 = s 14. 16 = s 15. 17 = s 16. 18 = s 17. 19 = s 18. 20 = s 19. 21 = s 20. 22 = s 21. 23 = s 22. 24 = s 23. 25 = s 24. %{ == 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 lemma]]s. }% 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 _ _). %{ {{case study}} }%