sig gcd. kind nat, bool type. type z nat. type s nat -> nat. type tt, ff bool. type nat nat -> o. type bool bool -> o. type sub, gcd nat -> nat -> nat -> o. type less nat -> nat -> bool -> o. type lt nat -> nat -> o.
%% Euclid's GCD algorithm %% %% Adapted from the %reduces example in the Twelf User's Guide: %% http://www.cs.cmu.edu/~twelf/guide-1-4/twelf_8.html#SEC47 module gcd. nat z. nat (s N) :- nat N. bool tt. bool ff. sub X z X. sub (s X) (s Y) Z :- sub X Y Z. less z (s X) tt. less X z ff. less (s X) (s Y) B :- less X Y B. lt z (s Y). lt (s X) (s Y) :- lt X Y. gcd z Y Y. gcd X z X. gcd (s X) (s Y) Z :- less X Y tt, sub Y X Y', gcd (s X) Y' Z. % (1) gcd (s X) (s Y) Z :- less X Y ff, sub X Y X', gcd X' (s Y) Z. % (2)
Click on a command or tactic to see a detailed view of its use.
%% This requires strong induction which we can encode using regular %% inducution together with an ordering on natural numbers. %% %% Adapted from the %reduces example in the Twelf User's Guide: %% http://www.cs.cmu.edu/~twelf/guide-1-4/twelf_8.html#SEC47 Specification "gcd". Theorem sub_total_tt : forall X Y, {less X Y tt} -> exists Z, {sub Y X Z}. Theorem sub_total_ff : forall X Y, {less X Y ff} -> exists Z, {sub X Y Z}. Theorem less_total : forall X Y, {nat X} -> {nat Y} -> exists B, {bool B} /\ {less X Y B}.induction on 1. intros. case H1. case H2. search. search. case H2. search. apply IH to H3 H4. search.Theorem lt_trans : forall X Y Z, {lt X (s Y)} -> {lt Y Z} -> {lt X Z}.induction on 1. intros. case H1. case H2. search. search. case H2. case H3. apply IH to H3 H4. search.Theorem lt_nat : forall X Y, {lt X Y} -> {nat X}. Theorem lt_x_sx : forall X, {nat X} -> {lt X (s X)}. Theorem lt_s : forall X Y, {lt X Y} -> {lt X (s Y)}. Theorem sub_lt : forall X Y Z, {nat X} -> {sub X Y Z} -> {lt Z (s X)}.induction on 2. intros. case H2. apply lt_x_sx to H1. search. case H1. apply IH to H4 H3. apply lt_s to H5. search.Theorem gcd_total_strong : forall A B, {nat A} -> {nat B} -> (forall X Y, {lt X A} -> {lt Y B} -> exists Z, {nat Z} /\ {gcd X Y Z}).induction on 1. induction on 2. intros. apply lt_nat to H3. apply lt_nat to H4. % Trivial base cases case H1 (keep). case H3. case H2 (keep). case H4. % A = s N, B = s N1 apply IH to H7 H2. apply IH1 to H1 H8. clear IH IH1 H1 H2 H7 H8. % X = z case H3. search. % Y = z case H4. search. % X = s X1, Y = s X2 case H5. case H6. apply less_total to H13 H14. case H15. % X1 < X2 apply sub_total_tt to H16. apply sub_lt to H14 H17. apply lt_trans to H18 H12. apply H10 to _ H19 with X = s X1. search. % X1 >= X2 apply sub_total_ff to H16. apply sub_lt to H13 H17. apply lt_trans to H18 H11. apply H9 to H19 _ with Y = s X2. search.Theorem gcd_total : forall X Y, {nat X} -> {nat Y} -> exists Z, {nat Z} /\ {gcd X Y Z}.