Abella logo (small)

well-founded.thm

%% Use well-founded induction to prove the totality of Euclid's GCD algorithm. %% Well-foundedness is characterized by using the idea of accessibility %% (e.g. see https://coq.inria.fr/library/Coq.Init.Wf.html). %% %% Author: Todd Wilson %% %%%% Natural numbers Kind nat type. Type z nat. Type s nat -> nat. % Ground nats Define nat : nat -> prop by nat z; nat (s N) := nat N. % Less than Define lt : nat -> nat -> prop by lt N (s N); lt N1 (s N2) := lt N1 N2. % The accessible part of the less-than relation Define lt_acc : nat -> prop by lt_acc N := forall M, lt M N -> lt_acc M. %%%% Every natural number is accessible. Theorem nat_acc : forall N, nat N -> lt_acc N. induction on 1. intros. case H1. unfold. intros. case H2. apply IH to H2. unfold. intros. case H4. search. case H3. apply H6 to H5. search. %%%% Some properties of lt Theorem lt_z : forall N, nat N -> lt z (s N). induction on 1. intros. case H1. search. apply IH to H2. search. Theorem lt_s : forall N1 N2, lt N1 N2 -> lt (s N1) (s N2). induction on 1. intros. case H1. search. apply IH to H2. search. %%%% Algorithms % Subtraction Define sub : nat -> nat -> nat -> prop by sub N z N := nat N; sub (s N1) (s N2) N3 := sub N1 N2 N3. % Remainder: mod N M = R Define mod : nat -> nat -> nat -> prop by mod N M N := lt N M; mod N M R := exists N', sub N M N' /\ mod N' M R. % Euclid's Algorithm: gcd N M = D (including gcd z z = z) Define gcd : nat -> nat -> nat -> prop by gcd N z N; gcd N (s M) D := exists R, mod N (s M) R /\ gcd (s M) R D. %%%% Properties of algorithms % Totality of subtraction Theorem sub_total : forall N1 N2, nat N1 -> nat N2 -> lt N1 N2 \/ exists N3, nat N3 /\ sub N1 N2 N3. induction on 1. intros. case H1. case H2. search. apply lt_z to H3. search. case H2. search. apply IH to H3 H4. case H5. apply lt_s to H6. search. search. % Non-zero subtraction gets smaller Theorem sub_lt : forall N1 N2 N3, nat N2 -> sub N1 (s N2) N3 -> lt N3 N1. induction on 1. intros. case H1. case H2. case H3. search. case H2. apply IH to H3 H4. search. % Totality of mod N (s M) R, by strong induction on N Theorem mod_total_strong : forall N M, nat N -> lt_acc N -> nat M -> exists R, nat R /\ mod N (s M) R. induction on 2. intros. case H2. apply sub_total to H1 _ with N2 = s M. case H5. search. apply sub_lt to H3 H7. apply H4 to H8. apply IH to H6 H9 H3. search. Theorem mod_total : forall N M, nat N -> nat M -> exists R, nat R /\ mod N (s M) R. intros. apply nat_acc to H1. apply mod_total_strong to H1 H3 H2. search. % Remainder smaller than divisor Theorem mod_lt : forall N M R, mod N M R -> lt R M. induction on 1. intros. case H1. search. apply IH to H3. search. % Totality of gcd N M D, by strong induction on m Theorem gcd_total_strong : forall N M, nat N -> nat M -> lt_acc M -> exists D, nat D /\ gcd N M D. induction on 3. intros. case H3. case H2. search. apply mod_total to H1 H5. apply mod_lt to H7. apply H4 to H8. %\ apply IH to _ H6 H9 with N = s N1. search. Theorem gcd_total : forall N M, nat N -> nat M -> exists D, nat D /\ gcd N M D. intros. apply nat_acc to H2. apply gcd_total_strong to H1 H2 H3. search.