-- ========================================================== --> Sample answers to exercises of lecture01 --> Proof scores for verifications of properties (including --> associativity and commutativity of _+_ and _*_) about --> Peano Style natural numbers -- ========================================================== --> Peano style natural numbers mod! PNAT { [ Nat ] op 0 : -> Nat {constr} . op s_ : Nat -> Nat {constr} . -- equality over the natural numbers eq (0 = s(Y:Nat)) = false . eq (s(X:Nat) = s(Y:Nat)) = (X = Y) . } --> PNAT with plus _+_ operation mod! PNAT+ { pr(PNAT) op _+_ : Nat Nat -> Nat {r-assoc} . eq 0 + Y:Nat = Y . eq (s X:Nat) + Y:Nat = s(X + Y) . } --> fundamental predicates of PNAT+ mod! PRED-PNAT+ {pr(PNAT+) -- 0 is right zero of _+_ op +rz : Nat -> Bool . eq +rz(X:Nat) = (X + 0 = X) . -- associativity of _+_ op +assoc : Nat Nat Nat -> Bool eq +assoc(X:Nat,Y:Nat,Z:Nat) = ((X + Y) + Z = X + (Y + Z)) . -- right successor of _+_ op +rs : Nat Nat -> Bool eq +rs(X:Nat,Y:Nat) = (X + s(Y) = s(X + Y)) . -- commutativity of _+_ op +comm : Nat Nat -> Bool eq +comm(X:Nat,Y:Nat) = (X + Y = Y + X) . } -- ========================================================== --> verification of the properties about _+_ -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+ --> (for-all X:Nat).(X + 0 = X) --> (i.e. +rz(X:Nat) = true) -- Proof: By induction on X. --> I Base case open PRED-PNAT+ . -- check red +rz(0) . close --> II Induction case open PRED-PNAT+ . -- arbitrary value op x : -> Nat . -- induction hypothesis eq x + 0 = x . -- check red +rz(s(x)) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+ --> (for-all X,Y,Z:Nat).((X + Y) + Z = X + (Y + Z)) --> (i.e. +assoc(X:Nat,Y:Nat,Z:Nat) = true) -- Proof: By induction on X. --> I Base case open PRED-PNAT+ . -- check red +assoc(0,`y:Nat,`z:Nat) . close --> II Induction case open PRED-PNAT+ . -- arbitrary values op x : -> Nat . -- induction hypothesis eq (x + Y:Nat) + Z:Nat = x + (Y + Z) . -- check red +assoc(s(x),`y:Nat,`z:Nat) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+ --> (for-all X,Y:Nat).(X + s(Y) = s(X + Y)) --> (i.e. +rs(X:Nat,Y:Nat) = true) -- Proof: By induction on X --> I Base case open PRED-PNAT+ . -- check red +rs(0,`y:Nat) . close --> II Induction case open PRED-PNAT+ . -- arbitrary values op x : -> Nat . -- induction hypothesis eq x + s(Y:Nat) = s(x + Y) . -- check red +rs(s(x),`y:Nat) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+ --> (for-all X,Y:Nat).(X + Y = Y + X) --> (i.e. +comm(X:Nat,Y:Nat) = true) -- Proof: By induction on X --> I Base case -- This case uses +rz(Y:Nat) as a lemma. open PRED-PNAT+ . -- already proved lemma: +rz(Y:Nat) eq (X:Nat + 0) = X . -- check red +comm(0,`y:Nat) . close --> II Induction case open PRED-PNAT+ . -- already proved lemma: +rs(X:Nat,Y:Nat) eq X:Nat + (s Y:Nat) = s(X + Y) . -- arbitrary values op x : -> Nat . -- induction hypothesis eq x + Y:Nat = Y + x . -- check red +comm(s(x),`y:Nat) . close --> QED -- ========================================================== -- ========================================================== --> PNAT with _+_ and _*_ operations -- ========================================================== mod! PNAT+* { pr(PNAT) -- notice that assoc and comm of _+_ are already proved op _+_ : Nat Nat -> Nat {assoc comm prec: 30} eq 0 + Y:Nat = Y . eq s(X:Nat) + Y:Nat = s(X + Y) . -- _*_ connects stronger than _+_ -- because it has smaller precedence (prec:) op _*_ : Nat Nat -> Nat {prec: 29 r-assoc} eq 0 * Y:Nat = 0 . eq s(X:Nat) * Y:Nat = Y + (X * Y) . } -- "{assoc comm prec: 30}" declares that the operator "_+_" -- is associative and commutative and parsing precedence 30. --> fundamental predicates of PNAT+* mod! PRED-PNAT+* { pr(PRED-PNAT+) pr(PNAT+*) -- _*_ distributes over _+_ from right op *distr : Nat Nat Nat -> Bool eq *distr(X:Nat,Y:Nat,Z:Nat) = ((X + Y) * Z = X * Z + Y * Z) . -- associativity of _*_ op *assoc : Nat Nat Nat -> Bool eq *assoc(X:Nat,Y:Nat,Z:Nat) = ((X * Y) * Z = X * (Y * Z)) . -- 0 is right zero of _*_ op *rz : Nat -> Bool eq *rz(X:Nat) = (X * 0 = 0) . -- right successor of _*_ op *rs : Nat Nat -> Bool eq *rs(X:Nat,Y:Nat) = (X * s(Y) = X + (X * Y)) . -- commutativity of _*_ op *comm : Nat Nat -> Bool eq *comm(X:Nat,Y:Nat) = (X * Y = Y * X) . } ** ========================================================== --> verification of properties about _*_ ** ========================================================== -- ========================================================== --> Property of PRED-PNAT+* --> \forall X,Y,Z:Nat.((X + Y) * Z = X * Z + Y * Z) -- (i.e. *distr(X:Nat,Y:nat,Z:Nat) = true) -- Proof: By induction on X. --> I Base case open PRED-PNAT+* . -- check red *distr(0,`y:Nat,`z:Nat) . close --> II Induction case open PRED-PNAT+* . -- arbitrary value op x : -> Nat . -- induction hypothesis eq (x + Y:Nat) * Z:Nat = (x * Z) + (Y * Z) . -- check red *distr(s(x),`y:Nat,`z:Nat) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+* --> (for-all X,Y,Z:Nat).((X * Y) * Z = X * (Y * Z)) --> (i.e. *assoc(X:Nat,Y:Nat,Z:Nat) = true) -- Proof: By induction on X --> I Base case open PRED-PNAT+* . -- check red *assoc(0,`y:Nat,`z:Nat) . close --> II Induction case open PRED-PNAT+* . -- already proved lemma: *distr(X:Nat,Y:Nat,Z:Nat) eq (X:Nat + Y:Nat) * Z:Nat = (X * Z) + (Y * Z) . -- arbitrary values op x : -> Nat . -- induction hypothesis eq (x * Y:Nat) * Z:Nat = x * (Y * Z) . -- check red *assoc(s(x),`y:Nat,`z:Nat) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+* --> (for-all X:Nat).(X * 0 = 0) --> (i.e. *rz(X:Nat) = true) -- Proof: By induction on X --> I Base case open PRED-PNAT+* . -- check red *rz(0) . close --> II Induction case open PRED-PNAT+* . -- arbitrary value op x : -> Nat . -- induction hypothesis eq x * 0 = 0 . -- check red *rz(s(x)) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+* --> (for-all X,Y:Nat).(X * s(Y) = X + (X * Y)) --> (i.e. *rs(X:Nat,Y:Nat) = true) -- Proof: By induction on X --> I Base case open PRED-PNAT+* . -- check red *rs(0,`y:Nat) . close --> II Induction case open PRED-PNAT+* . -- arbitrary value op x : -> Nat . -- induction hypothesis eq x * s(Y:Nat) = x + (x * Y) . -- check red *rs(s(x),`y:Nat) . close --> QED -- ========================================================== -- ========================================================== --> Property of PRED-PNAT+* --> (for-all X,Y:Nat).(X * Y = Y * X) --> (i.e. *comm(X:Nat,Y:Nat) = true) -- Proof: By induction on X --> I Base case open PRED-PNAT+* . -- already proved lemma: *rz(Y:Nat) eq (X:Nat * 0) = 0 . -- check red *comm(0,`y:Nat) . close --> II Induction case open PRED-PNAT+* . -- already proved lemma: *rs(X:Nat,Y:Nat) eq X:Nat * (s Y:Nat) = X + (X * Y) . -- arbitrary values op x : -> Nat . -- induction hypothesis eq x * Y:Nat = Y:Nat * x . -- check red *comm(s(x),`y:Nat) . close --> QED -- ========================================================== -- ========================================================== --> end -- ==========================================================