Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
156 lines (105 sloc) 3.89 KB
%{
PROPERTIES OF THE PRELUDE
}%
%{ Uniqueness of nat-plus ... }%
%worlds () (nat-plus _ _ _).
%unique nat-plus +N1 +N2 -1N3.
%worlds () (nat-mone _ _ _).
%unique nat-mone +N1 +N2 -1N3.
%worlds () (nat-lt _ _ _).
%unique nat-lt +N1 +N2 -1N3.
%{ Lift it to a lemma we can use }%
plus-unique : nat-plus N1 N2 M -> nat-plus N1 N2 M' -> nat-eq M M' -> type.
%mode plus-unique +NP1 +NP2 -NEQ.
- : plus-unique N N' nat-eq/refl.
%worlds () (plus-unique _ _ _).
%total NP (plus-unique NP _ _).
%{ Effectiveness of nat-plus, if N1 and N2 are given,
we always produce a result. }%
can-nat-plus : {N1} {N2} nat-plus N1 N2 N3 -> type.
%mode can-nat-plus +N1 +N2 -NPP.
- : can-nat-plus z z nat-plus/z.
- : can-nat-plus z (s _) nat-plus/z.
- : can-nat-plus (s K) L (nat-plus/s NPP')
<- can-nat-plus K L NPP'.
%worlds () (can-nat-plus _ _ _).
%total N (can-nat-plus N _ _).
%{ Effectiveness of nat-mone }%
can-nat-mone : {N1} {N2} nat-mone N1 N2 N3 -> type.
%mode can-nat-mone +N1 +N2 -NMP.
- : can-nat-mone z _ nat-mone/z.
- : can-nat-mone _ z nat-mone/s-1.
- : can-nat-mone (s K) (s L) (nat-mone/s-2 CNMP)
<- can-nat-mone K L CNMP.
%worlds () (can-nat-mone _ _ _).
%total N (can-nat-mone N _ _).
can-nat-lt : {N1} {N2} nat-lt N1 N2 B -> type.
%mode can-nat-lt +N1 +N2 -B.
- : can-nat-lt z z nat-lt/z-z.
- : can-nat-lt z (s _) nat-lt/z-s.
- : can-nat-lt (s _) z nat-lt/s-z.
- : can-nat-lt (s K1) (s K2) (nat-lt/s-s CLT)
<- can-nat-lt K1 K2 CLT.
%worlds () (can-nat-lt _ _ _).
%total N (can-nat-lt N _ _).
%{ Prove that x + 0 = x }%
nat-plus-zero-id : {N1} nat-plus N1 z N1 -> type.
%mode nat-plus-zero-id +N -NP.
- : nat-plus-zero-id z nat-plus/z.
- : nat-plus-zero-id (s K) (nat-plus/s NP)
<- nat-plus-zero-id K NP.
%worlds () (nat-plus-zero-id _ _).
%total E (nat-plus-zero-id E _).
%{ Auxillary lemma. Prove that the second argument increase by one }%
nat-plus-flip : nat-plus N1 N2 N3 -> nat-plus N1 (s N2) (s N3) -> type.
%mode nat-plus-flip +NP -NP2.
- : nat-plus-flip _ nat-plus/z.
- : nat-plus-flip
(nat-plus/s Dplus : nat-plus (s N1) N2 (s N3))
(nat-plus/s DIH : nat-plus (s N1) (s N2) (s (s N3)))
<- nat-plus-flip Dplus DIH.
%worlds () (nat-plus-flip _ _).
%total E (nat-plus-flip E _).
%{ Commutativity of nat-plus }%
nat-plus-commutes : nat-plus N1 N2 N3 -> nat-plus N2 N1 N3 -> type.
%mode nat-plus-commutes +NP -NP'.
- : nat-plus-commutes _ D
<- nat-plus-zero-id N1 D.
- : nat-plus-commutes
(nat-plus/s Dplus)
D
<- nat-plus-commutes Dplus DIH
<- nat-plus-flip DIH D.
%worlds () (nat-plus-commutes _ _).
%total NP (nat-plus-commutes NP _).
%{ Reduction metrics on natural numbers }%
nat-plus-reduces-2 : {N1} {N2} {N3} nat-plus N1 N2 N3 -> type.
%mode nat-plus-reduces-2 +N1 +N2 +N3 +NP.
- : nat-plus-reduces-2 _ _ _ nat-plus/z.
- : nat-plus-reduces-2 (s N1) N2 (s N3) (nat-plus/s D)
<- nat-plus-reduces-2 N1 N2 N3 D.
%worlds () (nat-plus-reduces-2 _ _ _ _).
%total D (nat-plus-reduces-2 _ _ _ D).
%reduces N2 <= N3 (nat-plus-reduces-2 N1 N2 N3 _).
nat-plus-reduces-1 : {N1} {N2} {N3} nat-plus N1 N2 N3 -> type.
%mode nat-plus-reduces-1 +N1 +N2 +N3 +NP.
- : nat-plus-reduces-1 N1 N2 N3 D
<- nat-plus-commutes D D'
<- nat-plus-reduces-2 N2 N1 N3 D'.
%worlds () (nat-plus-reduces-1 _ _ _ _).
%total D (nat-plus-reduces-1 _ _ _ D).
%reduces N1 <= N3 (nat-plus-reduces-1 N1 N2 N3 _).
nat-eq-neq-void : nat-eq N1 N2 -> nat-neq N1 N2 -> void -> type.
%mode nat-eq-neq-void +EQ +NEQ -V.
- : nat-eq-neq-void nat-eq/refl (nat-neq/ss NEQP) V
<- nat-eq-neq-void nat-eq/refl NEQP V.
%worlds () (nat-eq-neq-void _ _ _).
%total NEQ (nat-eq-neq-void _ NEQ _).
nat-neq-sym : nat-neq N1 N2 -> nat-neq N2 N1 -> type.
%mode nat-neq-sym +NEQ1 -NEQ2.
- : nat-neq-sym nat-neq/zs nat-neq/sz.
- : nat-neq-sym nat-neq/sz nat-neq/zs.
- : nat-neq-sym (nat-neq/ss K1) (nat-neq/ss K2)
<- nat-neq-sym K1 K2.
%worlds () (nat-neq-sym _ _).
%total NEQ (nat-neq-sym NEQ _).
Jump to Line
Something went wrong with that request. Please try again.