# # From Arkoudas/Musser: Fundamental Proof Methods in Computer Science # MIT Press 2017. Chapter 3. # #========================================================================== # SECTION: Numeric equations # datatype N := zero | (S N) declare Plus: [N N] -> N [+] set-precedence S 350 define [x y z n m k] := [?x:N ?y:N ?z:N ?n:N ?m:N ?k:N] (x Plus S y) # Term: (Plus ?x:N # (S ?y:N)) (forall n m . n Plus m = m Plus n) # Sentence: (forall ?n:N # (forall ?m:N # (= (Plus ?n:N ?m:N) # (Plus ?m:N ?n:N)))) assert right-zero := (forall n . n + zero = n) assert right-nonzero := (forall n m . n + S m = S (n + m)) (!instance right-zero [(S zero)]) (!instance right-nonzero [zero (S zero)]) # Theorem: (= (Plus zero # (S (S zero))) # (S (Plus zero # (S zero)))) (!instance right-nonzero [zero]) # Theorem: (forall ?v303:N # (= (Plus zero # (S ?v303:N)) # (S (Plus zero ?v303:N)))) #========================================================================== # SECTION: Equality chaining # (!chain [(S S zero + S S zero) = (S (S S zero + S zero)) [right-nonzero] = (S S (S S zero + zero)) [right-nonzero] = (S S S S zero) [right-zero] ]) #========================================================================== # SECTION: Terms and sentences as trees # (positions-and-subterms (Plus (S zero) (Plus x y))) # List: [[[] (Plus (S zero) (Plus ?x ?y))] # [[1] (S zero)] # [[1 1] zero] # [[2] (Plus ?x ?y)] # [[2 1] ?x] # [[2 2] ?y]] define (subterm t I) := match I { [] => t | (list-of i rest) => (subterm (ith (children t) i) rest) } define (subterm-node t I) := (root (subterm t I)) (subterm-node (x + S S zero) [2 1]) # Symbol: S #========================================================================== # SECTION: More examples of equality chaining # define left-zero := (forall n . zero + n = n) define left-nonzero := (forall m n . (S n) + m = S (n + m)) (!force left-zero) (!force left-nonzero) declare Times: [N N] -> N [*] assert Times-zero := (forall x . x * zero = zero) assert Times-nonzero := (forall x y . x * S y = x * y + x) declare one: N assert one-definition := (one = S zero) define Times-right-one := (forall x . x * one = x) conclude Times-right-one pick-any x:N (!chain [(x * one) = (x * S zero) [one-definition] = (x * zero + x) [Times-nonzero] = (zero + x) [Times-zero] = x [left-zero]]) assert Times-associative := (forall x y z . (x * y) * z = x * (y * z)) declare **: [N N] -> N [310] assert Power-right-zero := (forall x . x ** zero = one) assert Power-right-nonzero := (forall x n . x ** S n = x * x ** n) #========================================================================== # SECTION: A more substantial proof example # define power-square-theorem := (forall n x . (x * x) ** n = x ** (n + n)) define (power-square-property n) := (forall x . (x * x) ** n = x ** (n + n)) (power-square-theorem equals? (forall n . power-square-property n)) # Term: true conclude power-zero-case := (power-square-property zero) pick-any x:N (!chain [((x * x) ** zero) = one [Power-right-zero] = (x ** zero) [Power-right-zero] = (x ** (zero + zero)) [right-zero]]) conclude power-one-case := (power-square-property (S zero)) pick-any x:N (!combine-equations (!chain [((x * x) ** S zero) = ((x * x) * (x * x) ** zero) [Power-right-nonzero] = ((x * x) * one) [Power-right-zero] = (x * x) [Times-right-one]]) (!chain [(x ** (S zero + S zero)) = (x ** (S (S zero + zero))) [right-nonzero] = (x ** (S S zero)) [right-zero] = (x * (x ** S zero)) [Power-right-nonzero] = (x * (x * (x ** zero))) [Power-right-nonzero] = (x * x * one) [Power-right-zero] = (x * x) [Times-right-one]])) conclude (forall x . (x * x) ** zero = x ** (zero + zero)) pick-any x:N (!chain [((x * x) ** zero) --> one [Power-right-zero] <-- (x ** zero) [Power-right-zero] <-- (x ** (zero + zero)) [right-zero]]) #========================================================================== # SECTION: A better proof # conclude (forall x . (x * x) ** S zero = x ** (S zero + S zero)) pick-any x:N (!combine-equations (!chain [((x * x) ** S zero) --> ((x * x) * ((x * x) ** zero)) [Power-right-nonzero] --> ((x * x) * (x ** (zero + zero))) [power-zero-case] --> (x * x * x ** (zero + zero)) [Times-associative]]) (!chain [(x ** (S zero + S zero)) --> (x ** (S (S zero + zero))) [right-nonzero] --> (x ** (S (S (zero + zero)))) [left-nonzero] --> (x * (x ** (S (zero + zero)))) [Power-right-nonzero] --> (x * x * x ** (zero + zero)) [Power-right-nonzero]])) define power-square-step := method (n) let {previous-result := (power-square-property n)} conclude (power-square-property (S n)) pick-any x:N (!combine-equations (!chain [((x * x) ** S n) --> ((x * x) * ((x * x) ** n)) [Power-right-nonzero] --> ((x * x) * (x ** (n + n))) [previous-result] --> (x * x * (x ** (n + n))) [Times-associative]]) (!chain [(x ** (S n + S n)) --> (x ** (S (S n + n))) [right-nonzero] --> (x ** (S S (n + n))) [left-nonzero] --> (x * (x ** (S (n + n)))) [Power-right-nonzero] --> (x * x * (x ** (n + n))) [Power-right-nonzero]])) define power-square-base := method () conclude (power-square-property zero) pick-any x:N (!chain [((x * x) ** zero) = one [Power-right-zero] = (x ** zero) [Power-right-zero] = (x ** (zero + zero)) [right-zero]]) #========================================================================== # SECTION: The principle of mathematical induction # by-induction power-square-theorem { zero => (!power-square-base) | (S n) => (!power-square-step n) } (forall n . power-square-property n ==> power-square-property (S n)) pick-any n:N assume induction-hypothesis := (power-square-property n) conclude (power-square-property (S n)) (!power-square-step n) define (power-square-property n) := (forall x . (x * x) ** n = x ** (n + n)) (power-square-property zero) # Sentence: (forall ?x:N # (= (** (Times ?x:N ?x:N) # zero) # (** ?x:N # (Plus zero zero)))) # (power-square-property (S zero)) # Sentence: (forall ?x:N # (= (** (Times ?x:N ?x:N) # (S zero)) # (** ?x:N # (Plus (S zero) # (S zero))))) # (power-square-property ?k) # Sentence: (forall ?x:N # (= (** (Times ?x:N ?x:N) # ?k:N) # (** ?x:N # (Plus ?k:N ?k:N)))) define left-zero := (forall n . zero + n = n) by-induction left-zero { zero => conclude (zero + zero = zero) (!chain [(zero + zero) --> zero [right-zero]]) | (n as (S m)) => conclude (zero + n = n) let {induction-hypothesis := (zero + m = m)} (!chain [(zero + S m) --> (S (zero + m)) [right-nonzero] --> (S m) [induction-hypothesis]]) }