Project

Namespaces

Public Vars

latte-integers.times

The multiplication defined on ℤ.

*

(* [m int] [n int])
((times m) n)

Definition: The function that multiplies m with n.

mult-prop

(mult-prop [m int])
(lambda
 [g (==> int int)]
 (and
  (= (g zero) zero)
  (forall [x int] (= (g (succ x)) ((plus-fun m) (g x))))))

Definition: The property of the multiplication function on integers.

mult-split-zero

(mult-split-zero [m int] [n int])
(==> (= (* m n) zero) (or (= m zero) (= n zero)))

Theorem:

mult-unique

(mult-unique [m int])
(q/unique (mult-prop m))

Theorem: The unicity of the multiplication function, through mult-prop.

plus-fun

(plus-fun [m int])
(lambda [n int] (+ n m))

Definition: The addition function used in multiplication.

times

(times [m int])
(q/the (mult-unique m))

Definition: The function that multiplies m to an integer

times-assoc

(times-assoc [n int] [m int] [p int])
(= (* (* n m) p) (* n (* m p)))

Theorem: Associativity of multiplication.

times-assoc-sym

(times-assoc-sym [n int] [m int] [p int])
(= (* n (* m p)) (* (* n m) p))

Theorem: The symmetric of times-assoc.

times-commute

(times-commute [n int] [m int])
(= (* n m) (* m n))

Theorem: Commutativity of multiplication.

times-dist-minus

(times-dist-minus [n int] [m int] [p int])
(= (* n (- m p)) (- (* n m) (* n p)))

Theorem: Distributivity of multiplication over subtraction.

times-dist-minus-sym

(times-dist-minus-sym [n int] [m int] [p int])
(= (- (* n m) (* n p)) (* n (- m p)))

Theorem: The symmetric of times-dist-minus.

times-dist-plus

(times-dist-plus [n int] [m int] [p int])
(= (* n (+ m p)) (+ (* n m) (* n p)))

Theorem: Distributivity of multiplication over addition.

times-dist-plus-sym

(times-dist-plus-sym [n int] [m int] [p int])
(= (+ (* n m) (* n p)) (* n (+ m p)))

Theorem: The symmetric of times-dist-plus.

times-eq-one

(times-eq-one [m int] [n int])
(==>
 (= (* m n) one)
 (or (and (= m one) (= n one)) (and (= m (-- one)) (= n (-- one)))))

Theorem:

times-eq-one-nat

(times-eq-one-nat [m int] [n int])
(==> (elem m nat) (= (* m n) one) (= m one))

Theorem:

times-eq-one-nat-swap

(times-eq-one-nat-swap [m int] [n int])
(==> (elem m nat) (= (* m n) one) (= n one))

Theorem:

times-gt-pos

(times-gt-pos [m int] [n int])
(==> (positive n) (> m one) (> (* n m) n))

Theorem:

times-gt-pos-one

(times-gt-pos-one [m int] [n int])
(==> (positive n) (> m one) (> (* n m) one))

Theorem:

times-le-nat

(times-le-nat [m int] [n int] [p int])
(==> (<= m n) (elem p nat) (<= (* m p) (* n p)))

Theorem:

times-left-cancel

(times-left-cancel [m int] [n int] [p int])
(==> (= (* p m) (* p n)) (not (= p zero)) (= m n))

Theorem:

times-nat-closed

(times-nat-closed)
(forall-in [n nat] (forall-in [m nat] (elem (* n m) nat)))

Theorem: The multiplication is closed for natural integers.

times-neg-neg

(times-neg-neg [m int] [n int])
(==> (negative m) (negative n) (positive (* m n)))

Theorem:

times-neg-pos

(times-neg-pos [m int] [n int])
(==> (negative m) (positive n) (negative (* m n)))

Theorem:

times-one

(times-one [n int])
(= (* n one) n)

Theorem:

times-one-swap

(times-one-swap [n int])
(= (* one n) n)

Theorem:

times-opp

(times-opp [m int] [n int])
(= (* m (-- n)) (-- (* m n)))

Theorem:

times-opp-opp

(times-opp-opp [m int] [n int])
(= (* (-- m) (-- n)) (* m n))

Theorem:

times-pos-neg

(times-pos-neg [m int] [n int])
(==> (positive m) (negative n) (negative (* m n)))

Theorem:

times-pos-pos

(times-pos-pos [m int] [n int])
(==> (positive m) (positive n) (positive (* m n)))

Theorem:

times-pred

(times-pred [m int] [n int])
(= (* m (pred n)) (- (* m n) m))

Theorem:

times-pred-swap

(times-pred-swap [n int] [m int])
(= (* (pred n) m) (- (* n m) m))

Theorem:

times-pred-swap-sym

(times-pred-swap-sym [n int] [m int])
(= (- (* n m) m) (* (pred n) m))

Theorem:

times-pred-sym

(times-pred-sym [m int] [n int])
(= (- (* m n) m) (* m (pred n)))

Theorem:

times-prop

(times-prop [m int])
(and
 (= ((times m) zero) zero)
 (forall [n int] (= (* m (succ n)) (+ (* m n) m))))

Theorem:

times-right-cancel

(times-right-cancel [m int] [n int] [p int])
(==> (= (* m p) (* n p)) (not (= p zero)) (= m n))

Theorem:

times-succ

(times-succ [m int] [n int])
(= (* m (succ n)) (+ (* m n) m))

Theorem:

times-succ-swap

(times-succ-swap [n int] [m int])
(= (* (succ n) m) (+ (* n m) m))

Theorem:

times-succ-swap-sym

(times-succ-swap-sym [n int] [m int])
(= (+ (* n m) m) (* (succ n) m))

Theorem:

times-succ-sym

(times-succ-sym [m int] [n int])
(= (+ (* m n) m) (* m (succ n)))

Theorem:

times-zero

(times-zero [n int])
(= (* n zero) zero)

Theorem:

times-zero-swap

(times-zero-swap [n int])
(= (* zero n) zero)

Theorem: