Skip to content
STELF
Documentation out of dateLearn more

Division over the natural numbers

This is a case study about division over the natural numbers. A number of arithmetic operations over the natural numbers will be defined, including division. The ultimate goal is to prove properties normally associated with division hold. STELF muscles flexed in this study include reasoning from false and using the %reduces directive to use strong induction in a proof.

First the “false” type and natural numbers are defined.

%sort uninhabited %.
%freeze uninhabited %.
%sort nat %.
%term nat/z nat %.
%term nat/s %pi nat %-> nat %.

Relations about arithmetic over the natural numbers are defined in the standard way.

%sort nat-plus {_ nat} {_ nat} {_ nat} %.
%term nat-plus/z nat-plus nat/z N N %.
%term nat-plus/s %pi (nat-plus (nat/s N1) N2 (nat/s N3)) %<- (nat-plus N1 N2 N3) %.
%sort nat-mult {_ nat} {_ nat} {_ nat} %.
%term nat-mult/z nat-mult nat/z N nat/z %.
%term nat-mult/s %pi (nat-mult (nat/s N1) N2 N3') %<- (nat-plus N2 N3 N3') %<- (nat-mult N1 N2 N3) %.
%sort nat-less {_ nat} {_ nat} %.
%term nat-less/z nat-less nat/z (nat/s _) %.
%term nat-less/s %pi (nat-less (nat/s N1) (nat/s N2)) %<- (nat-less N1 N2) %.
%sort nat-leq {_ nat} {_ nat} %.
%term nat-leq/z nat-leq nat/z _ %.
%term nat-leq/s %pi (nat-leq (nat/s N1) (nat/s N2)) %<- (nat-leq N1 N2) %.
%sort nat-compare {_ nat} {_ nat} %.
%term nat-compare/less %pi (nat-compare N1 N2) %<- (nat-less N1 N2) %.
%term nat-compare/leq %pi (nat-compare N1 N2) %<- (nat-leq N2 N1) %.
% nat-divmod DIVIDEND DIVISOR QUOTIENT REMAINDER
%sort nat-divmod {_ nat} {_ nat} {_ nat} {_ nat} %.
%term nat-divmod/base %pi (nat-divmod N1 N2 nat/z N1) %<- (nat-less N1 N2) %.
%term nat-divmod/rec
  %pi (nat-divmod N1 N2 (nat/s N3) N4)
  %<- (nat-divmod N1' N2 N3 N4)
  %<- (nat-plus N2 N1' N1) %.

Some basic properties about arithmetic.

%sort nat-leq-plus {_ nat-leq N1 N2} {_ nat-plus N1 _ N2} %.
%mode nat-leq-plus %in %out %.
%term _ nat-leq-plus nat-leq/z nat-plus/z %.
%term _ %pi (nat-leq-plus (nat-leq/s DLQ) (nat-plus/s DNP)) %<- (nat-leq-plus DLQ DNP) %.
%worlds () (nat-leq-plus _ _) %.
%total {D1} (nat-leq-plus D1 _) %.
%sort nat-compare-resp-s {_ nat-compare N1 N2} {_ nat-compare (nat/s N1) (nat/s N2)} %.
%mode nat-compare-resp-s %in %out %.
%term _ nat-compare-resp-s (nat-compare/less DL) (nat-compare/less (nat-less/s DL)) %.
%term _ nat-compare-resp-s (nat-compare/leq DLQ) (nat-compare/leq (nat-leq/s DLQ)) %.
%worlds () (nat-compare-resp-s _ _) %.
%total {} (nat-compare-resp-s _ _) %.
%sort can-nat-compare {N1} {N2} {_ nat-compare N1 N2} %.
%mode can-nat-compare %in %in %out %.
%term _ can-nat-compare _ _ (nat-compare/less nat-less/z) %.
%term _ can-nat-compare _ _ (nat-compare/leq nat-leq/z) %.
%term _
  %pi (can-nat-compare (nat/s N1) (nat/s N2) DC')
  %<- (can-nat-compare N1 N2 DC)
  %<- (nat-compare-resp-s DC DC') %.
%worlds () (can-nat-compare _ _ _) %.
%total {D1} (can-nat-compare D1 _ _) %.
%sort can-nat-plus {N1} {N2} {_ nat-plus N1 N2 N3} %.
%mode can-nat-plus %in %in %out %.
%term _ can-nat-plus _ _ nat-plus/z %.
%term _ %pi (can-nat-plus _ _ (nat-plus/s DP)) %<- (can-nat-plus _ _ DP) %.
%worlds () (can-nat-plus _ _ _) %.
%total (D1) (can-nat-plus D1 _ _) %.
%sort nat-plus-assoc {_ nat-plus N1 N2 N12} {_ nat-plus N2 N3 N23} {_ nat-plus N1 N23 N123} {_ nat-plus N12 N3 N123} %.
%mode nat-plus-assoc %in %in %in %out %.
%term _ nat-plus-assoc nat-plus/z DP nat-plus/z DP %.
%term _
  %pi (nat-plus-assoc (nat-plus/s DP1) DP2 (nat-plus/s DP3) (nat-plus/s DP4))
  %<- (nat-plus-assoc DP1 DP2 DP3 DP4) %.
%worlds () (nat-plus-assoc _ _ _ _) %.
%total (D1) (nat-plus-assoc D1 _ _ _) %.

The first proof about division: The remainder is less than the divisor!

%sort nat-divmod-mod-less {_ nat-divmod N1 N2 N3 N4} {_ nat-less N4 N2} %.
%sort nat-divmod-mod-less {_ nat-divmod N1 N2 N3 N4} {_ nat-less N4 N2} %.
%mode nat-divmod-mod-less %in %out %.
%term _ nat-divmod-mod-less (nat-divmod/base DL) DL %.
%term _
  %pi (nat-divmod-mod-less (nat-divmod/rec _ DDM) DL)
  %<- (nat-divmod-mod-less DDM DL) %.
%worlds () (nat-divmod-mod-less _ _) %.
%total {D1} (nat-divmod-mod-less D1 _) %.

Division by zero does not happen.

%sort nat-divmod-z-uninhabited {_ nat-divmod N1 nat/z N3 N4} {_ uninhabited} %.
%mode nat-divmod-z-uninhabited %in %out %.
%term _
  %pi (nat-divmod-z-uninhabited (nat-divmod/rec nat-plus/z DDM) DU)
  %<- (nat-divmod-z-uninhabited DDM DU) %.
%worlds () (nat-divmod-z-uninhabited _ _) %.
%total {D1} (nat-divmod-z-uninhabited D1 _) %.

The following theorem uses the %reduces directive to verify that if a non-zero number is added to N2, then the result is strictly larger than N2 in the sub-term sense. This is powerful information, because STELF verifies well-founded inductions over sub-term orderings.

%sort nat-plus-reduces-s {N2} {N3} {_ nat-plus (nat/s N1) N2 N3} %.
%mode nat-plus-reduces-s %in %in %in %.
%term _ nat-plus-reduces-s _ _ (nat-plus/s nat-plus/z) %.
%term _ %pi (nat-plus-reduces-s _ _ (nat-plus/s DL)) %<- (nat-plus-reduces-s _ _ DL) %.
%worlds () (nat-plus-reduces-s _ _ _) %.
%reduces < N2 N3 (nat-plus-reduces-s N2 N3 _) %.
%total {D1} (nat-plus-reduces-s _ _ D1) %.

The highlight of this example. Division is possible for any dividend as long as the divisor is non-zero. This proof is by induction over the dividend, which does get smaller as inductive calls are made. However, because STELF can not figure this out on its own, calls to nat-plus-reduces-s are required so that this proof passes the totality checker.

%sort can-nat-divmod* {N1} {_ nat-compare N1 (nat/s N2)} {_ nat-divmod N1 (nat/s N2) N3 N4} %.
%mode can-nat-divmod* %in %in %out %.
%term _ can-nat-divmod* _ (nat-compare/less DL) (nat-divmod/base DL) %.
%term _
  %pi (can-nat-divmod* N1 (nat-compare/leq DLQ) (nat-divmod/rec DP DDM))
  %<- (nat-leq-plus DLQ DP)
  %<- (nat-plus-reduces-s N1' N1 DP)
  %<- (can-nat-compare N1' (nat/s N2) DC)
  %<- (can-nat-divmod* N1' DC DDM) %.
%worlds () (can-nat-divmod* _ _ _) %.
%total {D1} (can-nat-divmod* D1 _ _) %.
%sort can-nat-divmod {N1} {N2} {_ nat-divmod N1 (nat/s N2) N3 N4} %.
%mode can-nat-divmod %in %in %out %.
%term _
  %pi (can-nat-divmod N1 N2 DDM)
  %<- (can-nat-compare N1 (nat/s N2) DC)
  %<- (can-nat-divmod* N1 DC DDM) %.
%worlds () (can-nat-divmod _ _ _) %.
%total {} (can-nat-divmod _ _ _) %.

It is also useful to know the definition of division is correct with respect to multiplication.

%sort nat-divmod-correct {_ nat-divmod N1 N2 N3 N4} {_ nat-mult N3 N2 N3'} {_ nat-plus N3' N4 N1} %.
%mode nat-divmod-correct %in %out %out %.
%term _ nat-divmod-correct (nat-divmod/base _) nat-mult/z nat-plus/z %.
%term _
  %pi (nat-divmod-correct (nat-divmod/rec DP DD) (nat-mult/s DM DP'') DP''')
  %<- (nat-divmod-correct DD DM DP')
  %<- (can-nat-plus N2 N3' DP'')
  %<- (nat-plus-assoc DP'' DP' DP DP''') %.
%worlds () (nat-divmod-correct _ _ _) %.
%total (D1) (nat-divmod-correct D1 _ _) %.

In the above code, the division algorithm for natural numbers was defined. A few interesting properties about this judgment were proven. The first is that the remainder computed is strictly less than the divisor. The second is that the judgment is not inhabited when the divisor is zero. The third is an effectiveness lemma which shows that this judgment is inhabited for any dividend and any divisor greater than zero. Finally, the division relation was shown to be correct with respect to multiplication.