%{ This is part of a proof of the soundness of Featherweight Java (Atsushi Igarashi, Benjamin Pierce and Philip Wadler) in the Twelf logical Framework. It was developed by Stephanie Weirich and Geoffrey Washburn . }% %{ Library for natural numbers. Decided to write this myself so that I was sure to understand everything }% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % The definition of natural numbers nat : type. %name nat N n. % Zero z : nat. % Successor s : nat -> nat. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Predecessor function % Necessary for some inductive reasoning, because equality on nats is not % inductively defined. pred : nat -> nat -> type. %name nat PRED pred. %mode pred +N1 -N2. % Could perhaps choose to make this a partial function? Would it matter much? pred_z: pred z z. pred_s: pred (s N) N. %worlds () (pred N1 N2). %covers pred +N1 -N2. %unique pred +N1 -1N2. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Plus relation % FIX - should this be moded? plus : nat -> nat -> nat -> type. %name plus PL pl. %mode plus +N1 +N2 -N3. plus_z : plus z N N. plus_s : plus N1 N2 N3 -> % -------------- plus (s N1) N2 (s N3). %terminates N1 (plus N1 N2 N3). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Equality relation % FIX? Should this be moded? nat_eq : nat -> nat -> type. %name nat_eq NEQ neq. %mode nat_eq +N1 +N2. nat_refl : nat_eq N N. % Decided to try going with equality defined by unification % rather than inductively over the structure of its inputs. % % nat_eq_z : nat_eq z z. % % nat_eq_s : nat_eq N1 N2 -> % % ---------------------- % nat_eq (s N1) (s N2). %worlds () (nat_eq N1 N2). %terminates {N1 N2} (nat_eq N1 N2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Disequals relation % % Should we be defining this directly? Or using false? nat_neq : nat -> nat -> type. %name nat_neq NNEQ nneq. %mode nat_neq +N1 +N2. % FIX? Should this be moded? nat_neq_zs : nat_neq z (s N). nat_neq_sz : nat_neq (s N) z. nat_neq_ss : nat_neq N1 N2 -> % ---------------------- nat_neq (s N1) (s N2). %worlds () (nat_neq N1 N2). %terminates {N1 N2} (nat_neq N1 N2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Less than relation nat_lt : nat -> nat -> type. %name nat_lt NLT nlt. %mode nat_lt +N1 +N2. % FIX? Should this be moded? nat_lt_z : nat_lt z (s N). nat_lt_s : nat_lt N1 N2 -> % -------------------- nat_lt (s N1) (s N2). %worlds () (nat_lt N1 N2). %terminates {N1 N2} (nat_lt N1 N2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Less than or equal to relation nat_lte : nat -> nat -> type. %name nat_lte NLTE nlte. %mode nat_lte +N1 +N2. % FIX? Should this be moded? nat_lte_z : nat_lte z N. nat_lte_s : nat_lte N1 N2 -> % --------------------- nat_lte (s N1) (s N2). %terminates {N1 N2} (nat_lte N1 N2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Less than or equal to algorithm comp_nat_lte : {N1:nat} {N2:nat} nat_lte N1 N2 -> type. %mode comp_nat_lte +N1 +N2 -LTE. comp_nat_lte_z : comp_nat_lte z N (nat_lte_z). comp_nat_lte_s : comp_nat_lte N1 N2 LTE -> % -------------------------- comp_nat_lte (s N1) (s N2) (nat_lte_s LTE). %worlds () (comp_nat_lte N1 N2 LTE). %terminates N1 (comp_nat_lte N1 N2 LTE). %unique comp_nat_lte +N1 +N2 -1LTE. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Greater than relation nat_gt : nat -> nat -> type. %name nat_gt NGT ngt. %mode nat_gt +N1 +N2. % FIX? Should this be moded? nat_gt_z : nat_gt (s N) z. nat_gt_s : nat_gt N1 N2 -> % -------------------- nat_gt (s N1) (s N2). %terminates {N1 N2} (nat_gt N1 N2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Greater than algorithm comp_nat_gt : {N1:nat} {N2:nat} nat_gt N1 N2 -> type. %mode comp_nat_gt +N1 +N2 -GT. comp_nat_gt_z : comp_nat_gt (s N) z (nat_gt_z). comp_nat_gt_s : comp_nat_gt N1 N2 GT -> % ----------------------- comp_nat_gt (s N1) (s N2) (nat_gt_s GT). %worlds () (comp_nat_gt N1 N2 GT). %terminates N2 (comp_nat_gt N1 N2 GT). %unique comp_nat_gt +N1 +N2 -1GT. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% excluded middle for natural numbers %% nat_em is a datatype for the excluded middle property %% of natural number equality. Either two numbers are equal %% or they are not. nat_em : nat -> nat -> type. nat_em_eq : nat_eq N M -> nat_em N M. nat_em_neq : nat_neq N M -> nat_em N M. %% nat_excluded takes two numbers and returns the datatype %% that contains either a proof of their equality or %% disequality. :-) %% It is defined in conjunction with nat_em_helper that %% takes care of the splitting issue. nat_excluded : {N}{M} nat_em N M -> type. %mode (nat_excluded +N +M -NE). -: nat_excluded z z (nat_em_eq nat_refl). -: nat_excluded (s N) z (nat_em_neq nat_neq_sz). -: nat_excluded z (s N) (nat_em_neq nat_neq_zs). nat_em_helper : nat_em N M -> nat_em (s N) (s M) -> type. %mode (nat_em_helper +N -M). -: nat_em_helper (nat_em_eq nat_refl) (nat_em_eq (nat_refl)). -: nat_em_helper (nat_em_neq R) (nat_em_neq (nat_neq_ss R)). %worlds () (nat_em_helper N M). %total N (nat_em_helper N M). %unique (nat_em_helper +N -1M). -: nat_em_helper R RR -> nat_excluded N M R -> nat_excluded (s N) (s M) RR. %worlds () (nat_excluded M N MN). %total {M N} (nat_excluded M N MN). %unique (nat_excluded +M +N -1MN). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% properties of natural number equality nat_trans : nat_eq M N -> nat_eq N P -> nat_eq M P -> type. %mode nat_trans +N +O -P. -: nat_trans nat_refl nat_refl nat_refl. %worlds () (nat_trans N O P). %total N (nat_trans N O P). nat_sym : nat_eq M N -> nat_eq N M -> type. %mode nat_sym +N -P. -: nat_sym nat_refl nat_refl. %worlds () (nat_sym N P). %total N (nat_sym N P). % Disequality is symmetric nat_neq_sym : nat_neq M N -> nat_neq N M -> type. %mode nat_neq_sym +N -P. -: nat_neq_sym (nat_neq_zs) (nat_neq_sz). -: nat_neq_sym (nat_neq_sz) (nat_neq_zs). -: nat_neq_sym NNEQ1 NNEQ2 -> % ------------------------------------------------ nat_neq_sym (nat_neq_ss NNEQ1) (nat_neq_ss NNEQ2). %worlds () (nat_neq_sym N P). %total N (nat_neq_sym N P). %% congruence rules/would be nice to have Leibniz equality. %% if M = N then P(M) => P (N). %% But we can't prove things in that generality. We must prove it for each %% particular case. %% this is congruence over inequality. nat_cong : nat_eq M N -> nat_neq M P -> nat_neq N P -> type. %mode nat_cong +N +O -P. -: nat_cong nat_refl nat_neq_zs nat_neq_zs. -: nat_cong nat_refl nat_neq_sz nat_neq_sz. -: nat_cong nat_refl NEQ1 NEQ2 -> nat_cong nat_refl (nat_neq_ss NEQ1) (nat_neq_ss NEQ2). %worlds () (nat_cong N O P). %total O (nat_cong N O P). %% natural numbers cannot both be equal and inequal. nat_eq_exclusive : nat_eq N M -> nat_neq N M -> false -> type. %mode nat_eq_exclusive +N +M -F. -: nat_eq_exclusive nat_refl NEQ FALSE -> nat_eq_exclusive nat_refl (nat_neq_ss NEQ) FALSE. %worlds () (nat_eq_exclusive N M F). %total (M) (nat_eq_exclusive N M F). %% false implies that we have any equality we choose. false_imp_nat_eq : {N1:nat} {N2:nat} false -> nat_eq N1 N2 -> type. %mode false_imp_nat_eq +N1 +N2 +FALSE -NEQ. %worlds () (false_imp_nat_eq N1 N2 F NEQ). %total F (false_imp_nat_eq N1 N2 F NEQ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % If two nats are equal and they have a predecessor, their predecessors are also % equal. Not true when one of the nats is zero, so we also require that the % inputs are not equal to zero. % % This is necessary because we do not have inductive reasoning over equality. pred_eq_lemma: nat_neq N1 z -> nat_neq N2 z -> nat_eq N1 N2 -> pred N1 N3 -> pred N2 N4 -> nat_eq N3 N4 -> type. %mode pred_eq_lemma +NNEQ1 +NNEQ2 +NEQ1 +PRED1 +PRED2 -NEQ2. -: pred_eq_lemma NNEQ1 NNEQ2 NEQ1 PRED1 PRED2 nat_refl. %worlds () (pred_eq_lemma NNEQ1 NNEQ2 NEQ1 PRED1 PRED2 NEQ2). %total {PRED1 PRED2} (pred_eq_lemma NNEQ1 NNEQ2 NEQ1 PRED1 PRED2 NEQ2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% pred_eq_lemma_alt: nat_eq (s N1) (s N2) -> nat_eq N1 N2 -> type. %mode pred_eq_lemma_alt +NEQ1 -NEQ2. -: pred_eq_lemma_alt NEQ nat_refl. %worlds () (pred_eq_lemma_alt NEQ1 NEQ2). %total {NEQ1} (pred_eq_lemma_alt NEQ1 NEQ2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % If two nats are equal, then their succecessors are also equal % % Also needed because equality is not inductively defined. succ_eq_lemma : nat_eq N1 N2 -> nat_eq (s N1) (s N2) -> type. %mode succ_eq_lemma +NEQ1 -NEQ2. - : succ_eq_lemma NEQ nat_refl. %worlds () (succ_eq_lemma NEQ1 NEQ2). %total NEQ1 (succ_eq_lemma NEQ1 NEQ2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % If we add equal nats we get an equal result. plus_eq_lemma : nat_eq N1 N2 -> nat_eq N3 N4 -> plus N1 N3 N5 -> plus N2 N4 N6 -> nat_eq N5 N6 -> type. %mode plus_eq_lemma +NEQ1 +NEQ2 +PL1 +PL2 -NEQ. - : plus_eq_lemma NEQ1 NEQ2 (plus_z) (plus_z) NEQ2. - : succ_eq_lemma NEQ4 NEQ5 -> plus_eq_lemma NEQ3 NEQ2 PL1 PL2 NEQ4 -> pred_eq_lemma_alt NEQ1 NEQ3 -> % ------------------------------------------------------------------------------ plus_eq_lemma NEQ1 NEQ2 (plus_s PL1) (plus_s PL2) NEQ5. %worlds () (plus_eq_lemma NEQ1 NEQ2 PL1 PL2 NEQ). %total {PL1 PL2} (plus_eq_lemma NEQ1 NEQ2 PL1 PL2 NEQ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % If N1 is less than N2 and N2 = N3 then N1 is less than N3. nat_lt_eq : nat_lt N1 N2 -> nat_eq N2 N3 -> nat_lt N1 N3 -> type. %mode nat_lt_eq +NLT1 +NEQ -NLT2. -: nat_lt_eq (nat_lt_z) (nat_refl) (nat_lt_z). -: nat_lt_eq NLT1 NEQ2 NLT2 -> pred_eq_lemma_alt NEQ1 NEQ2 -> % ----------------------------------------- nat_lt_eq (nat_lt_s NLT1) NEQ1 (nat_lt_s NLT2). %worlds () (nat_lt_eq NLT1 NEQ NLT2). %total NLT1 (nat_lt_eq NLT1 NEQ NLT2).