mathlib documentation

non-mathlib.early_version

source
inductive mynat  :
Type
source
theorem succ_eq (a b : mynat) :
a = b → a.mysucc = b.mysucc
source
def nat_one  :
mynat
Equations
source
def myadd  :
mynat → mynat → mynat
Equations
source
theorem add_zero (n : mynat) :
myadd n mynat.zero = n
source
theorem add_succ (n m : mynat) :
myadd n m.mysucc = (myadd n m).mysucc
source
theorem zero_add (n : mynat) :
myadd mynat.zero n = n
source
theorem succ_add (n m : mynat) :
myadd n.mysucc m = (myadd n m).mysucc
source
theorem add_assoc (a b c : mynat) :
myadd (myadd a b) c = myadd a (myadd b c)
source
theorem add_comm (a b : mynat) :
myadd a b = myadd b a
source
theorem add_cancel_a (a b c : mynat) :
myadd b a = myadd c a → b = c
source
theorem add_cancel_a_rev (a b c : mynat) :
myadd a b = myadd a c → b = c
source
theorem add_cancel_b (a b c : mynat) :
b = c → myadd b a = myadd c a
source
theorem add_comm_in_tree (a b c d : mynat) :
myadd (myadd a b) (myadd c d) = myadd (myadd a c) (myadd b d)
source
theorem add_combine_eq (a b c d : mynat) :
a = b → c = d → myadd a c = myadd b d
source
def mymul  :
mynat → mynat → mynat
Equations
source
theorem zero_mul (n : mynat) :
mymul mynat.zero n = mynat.zero
source
theorem mul_zero (n : mynat) :
mymul n mynat.zero = mynat.zero
source
theorem one_mul_eq (n : mynat) :
mymul mynat.zero.mysucc n = n
source
theorem mul_one_eq (n : mynat) :
mymul n mynat.zero.mysucc = n
source
theorem mul_succ (n m : mynat) :
mymul n.mysucc m = myadd (mymul n m) m
source
theorem succ_mul (n m : mynat) :
mymul n m.mysucc = myadd (mymul n m) n
source
theorem mul_comm (n m : mynat) :
mymul n m = mymul m n
source
theorem mul_add (t a b : mynat) :
mymul t (myadd a b) = myadd (mymul t a) (mymul t b)
source
theorem mul_assoc (a b c : mynat) :
mymul (mymul a b) c = mymul a (mymul b c)
source
theorem mul_add_distrib (a b c : mynat) :
mymul (myadd a b) c = myadd (mymul a c) (mymul b c)
source
theorem mul_add_distrib_alt (a b c : mynat) :
mymul a (myadd b c) = myadd (mymul a b) (mymul a c)
source
theorem mul_add_distrib_rev (a b c : mynat) :
myadd (mymul a b) (mymul a c) = mymul (myadd b c) a
source
theorem mul_two (a : mynat) :
mymul mynat.zero.mysucc.mysucc a = myadd a a
source
theorem mul_result_zero (a b c : mynat) :
a = c.mysucc → mymul a b = mynat.zero → b = mynat.zero
source
theorem mul_cancel (a b c : mynat) :
mymul a c.mysucc = mymul b c.mysucc → a = b
source
theorem mul_zero_collapse (a b c : mynat) :
¬a = b → mymul a c = mymul b c → c = mynat.zero
source
theorem add_self_eq_mul_two (a : mynat) :
myadd a a = mymul mynat.zero.mysucc.mysucc a
source
theorem add_self (a b : mynat) :
myadd a a = myadd b b → a = b
source
theorem add_self_inv (a b : mynat) :
¬a = b → ¬myadd a a = myadd b b
source
theorem mul_weird_sub_a (a b c d : mynat) :
(∃ (e : mynat), d = myadd c e.mysucc) → myadd (mymul a c) (mymul b d) = myadd (mymul b c) (mymul a d) → a = b
source
theorem difference_exists (a b : mynat) :
(∃ (c : mynat), myadd a c = b) ∨ ∃ (c : mynat), a = myadd b c
source
theorem ne_implies_nonzero_diff (a b : mynat) :
a ≠ b → ((∃ (c : mynat), b = myadd a c.mysucc) ∨ ∃ (c : mynat), a = myadd b c.mysucc)
source
theorem mul_weird_sub (a b c d : mynat) :
c ≠ d → myadd (mymul a c) (mymul b d) = myadd (mymul b c) (mymul a d) → a = b
source
inductive myint  :
Type
source
def int_zero  :
myint
Equations
source
def int_one  :
myint
Equations
source
def iszero  :
myint → Prop
Equations
source
def int_equal  :
myint → myint → Prop
Equations
source
theorem int_zeros_eq (a b : myint) :
iszero a → iszero b → int_equal a b
source
theorem int_zeros_only_eq (a b : myint) :
iszero a → int_equal a b → iszero b
source
theorem int_zeros_only_eq_rev (a b : myint) :
iszero a → int_equal b a → iszero b
source
theorem int_equal_refl (a : myint) :
int_equal a a
source
theorem int_eq_comm (a b : myint) :
int_equal a b → int_equal b a
source
theorem int_eq_comm_double (a b : myint) :
int_equal a b ↔ int_equal b a
source
theorem int_eq_trans (a b c : myint) :
int_equal a b → int_equal b c → int_equal a c
source
def int_add  :
myint → myint → myint
Equations
source
theorem add_zero_int (a b : myint) :
iszero a → int_equal b (int_add a b)
source
theorem add_zero_int_alt (a b : myint) :
iszero a → int_equal (int_add a b) b
source
theorem add_comm_int (a b : myint) :
int_equal (int_add a b) (int_add b a)
source
theorem add_comm_int_rw (a b : myint) :
int_add a b = int_add b a
source
theorem add_eq (a b c : myint) :
int_equal b c ↔ int_equal (int_add a b) (int_add a c)
source
theorem add_assoc_int (a b c : myint) :
int_equal (int_add (int_add a b) c) (int_add a (int_add b c))
source
theorem add_assoc_int_rw (a b c : myint) :
int_add (int_add a b) c = int_add a (int_add b c)
source
theorem add_sub_int (a b c d : myint) :
int_equal a b → int_equal (int_add a c) d → int_equal (int_add b c) d
source
theorem int_add_self_nonzero (a : myint) :
¬iszero a → ¬iszero (int_add a a)
source
def int_mul  :
myint → myint → myint
Equations
source
theorem mul_comm_int (a b : myint) :
int_equal (int_mul a b) (int_mul b a)
source
theorem mul_comm_int_rw (a b : myint) :
int_mul a b = int_mul b a
source
theorem add_helper_1 (a b c : mynat) :
myadd (myadd a b) c = myadd (myadd a c) b
source
theorem add_helper_2 (a b c d : mynat) :
myadd a (myadd (myadd b c) d) = myadd b (myadd (myadd a c) d)
source
theorem mul_eq (a b c : myint) :
int_equal b c → int_equal (int_mul a b) (int_mul a c)
source
theorem mul_eq_alt (a b c : myint) :
int_equal b c → int_equal (int_mul b a) (int_mul c a)
source
@[simp]
theorem mul_assoc_int (a b c : myint) :
int_equal (int_mul (int_mul a b) c) (int_mul a (int_mul b c))
source
theorem mul_assoc_int_rw (a b c : myint) :
int_mul (int_mul a b) c = int_mul a (int_mul b c)
source
theorem mul_tree_swap_int_rw (a b c d : myint) :
int_mul (int_mul a b) (int_mul c d) = int_mul (int_mul a c) (int_mul b d)
source
theorem mul_distrib_int (a b c : myint) :
int_equal (int_mul (int_add a b) c) (int_add (int_mul a c) (int_mul b c))
source
theorem mul_distrib_int_rw (a b c : myint) :
int_mul (int_add a b) c = int_add (int_mul a c) (int_mul b c)
source
theorem mul_distrib_int_rw_alt (a b c : myint) :
int_mul a (int_add b c) = int_add (int_mul a b) (int_mul a c)
source
theorem mul_zero_int (a b : myint) :
iszero a → iszero (int_mul a b)
source
theorem mul_zero_int_alt (a b : myint) :
iszero a → iszero (int_mul b a)
source
theorem mul_zero_int_zero (a : myint) :
int_equal (int_mul a int_zero) int_zero
source
theorem mul_result_zero_int (a b : myint) :
¬iszero a → iszero (int_mul a b) → iszero b
source
theorem mul_result_zero_int_rev (a b : myint) :
¬iszero b → iszero (int_mul a b) → iszero a
source
theorem mul_one_int (a : myint) :
int_equal a (int_mul a int_one)
source
theorem mul_one_int_rw (a : myint) :
int_mul a int_one = a
source
theorem mul_one_int_rw_alt (a : myint) :
int_mul (myint.int mynat.zero.mysucc mynat.zero) a = a
source
theorem mul_comm_zero_int (a b : myint) :
iszero (int_mul a b) = iszero (int_mul b a)
source
theorem mul_sub_int (a b c d : myint) :
int_equal a b → int_equal (int_mul a c) d → int_equal (int_mul b c) d
source
theorem multiply_two_equalities_int (a b c d : myint) :
int_equal a b → int_equal c d → int_equal (int_mul a c) (int_mul b d)
source
theorem stupid (a b : mynat) :
a = b = (b = a)
source
theorem mul_cancel_int (a b c : myint) :
¬iszero b → int_equal (int_mul a b) (int_mul c b) → int_equal a c
source
theorem mul_cancel_int_alt (a b c : myint) :
¬iszero a → int_equal (int_mul a b) (int_mul a c) → int_equal b c
source
theorem mul_nonzero_int (a b : myint) :
¬iszero a → ¬iszero b → ¬iszero (int_mul a b)
source
theorem mul_sub_in_add_int (a b c d e : myint) :
int_equal a b → int_equal (int_add (int_mul a c) d) e → int_equal (int_add (int_mul b c) d) e
source
theorem mul_two_int (a : myint) :
int_mul (myint.int mynat.zero.mysucc.mysucc mynat.zero) a = int_add a a
source
def negative  :
myint → myint
Equations
source
def negative_eq (a b : myint) :
int_equal a b → int_equal (negative a) (negative b)
source
def add_to_negative (a : myint) :
int_equal int_zero (int_add a (negative a))
source
def add_to_negative_alt (a : myint) :
iszero (int_add a (negative a))
source
def mul_negative (a b : myint) :
int_mul a (negative b) = negative (int_mul a b)
source
def mul_negative_alt (a b : myint) :
int_mul a (negative b) = int_mul (negative a) b
source
inductive myrat  :
Type
source
def rat_zero  :
myrat
Equations
source
def rat_one  :
myrat
Equations
source
def rat_two  :
myrat
Equations
source
def defined  :
myrat → Prop
Equations
source
def iszero_rat  :
myrat → Prop
Equations
source
theorem undef_iszero (a : myrat) :
¬defined a → iszero_rat a
source
def rat_eq  :
myrat → myrat → Prop
Equations
source
theorem undef_eq (a b : myrat) :
¬defined a → rat_eq a b
source
theorem rat_eq_refl (a : myrat) :
rat_eq a a
source
theorem rat_eq_comm (a b : myrat) :
rat_eq a b → rat_eq b a
source
theorem eq_undef (a b : myrat) :
¬defined b → rat_eq a b
source
theorem zeroes_only_eq_rat (a b : myrat) :
defined a → rat_eq a b → iszero_rat a → iszero_rat b
source
theorem rat_eq_trans (a b c : myrat) :
defined b → rat_eq a b → rat_eq b c → rat_eq a c
source
def rat_mul  :
myrat → myrat → myrat
Equations
source
theorem rat_mul_comm (a b : myrat) :
rat_mul a b = rat_mul b a
source
theorem rat_mul_def (a b : myrat) :
defined a → defined b → defined (rat_mul a b)
source
theorem rat_mul_undef (a b : myrat) :
¬defined a → ¬defined (rat_mul a b)
source
theorem rat_undef_mul (a b : myrat) :
¬defined b → ¬defined (rat_mul a b)
source
theorem rat_mul_zero (a b : myrat) :
iszero_rat a → iszero_rat (rat_mul a b)
source
theorem rat_mul_assoc (a b c : myrat) :
rat_mul (rat_mul a b) c = rat_mul a (rat_mul b c)
source
theorem rat_mul_eq (a b c : myrat) :
rat_eq b c → rat_eq (rat_mul a b) (rat_mul a c)
source
theorem mul_sub_rat (a b c d : myrat) :
defined a → rat_eq a b → rat_eq (rat_mul a c) d → rat_eq (rat_mul b c) d
source
theorem mul_eq_rat (a b c : myrat) :
rat_eq a b → rat_eq (rat_mul a c) (rat_mul b c)
source
theorem mul_eq_rat_alt (a b c : myrat) :
rat_eq a b → rat_eq (rat_mul c a) (rat_mul c b)
source
def rat_add  :
myrat → myrat → myrat
Equations
source
theorem rat_add_undef (a b : myrat) :
¬defined a → ¬defined (rat_add a b)
source
theorem rat_add_def (a b : myrat) :
defined a → defined b → defined (rat_add a b)
source
theorem rat_add_zero (a b : myrat) :
iszero_rat a → rat_eq (rat_add a b) b
source
theorem rat_add_zero_alt (a : myrat) :
rat_add a rat_zero = a
source
theorem add_eq_rat (a b c : myrat) :
rat_eq a b → rat_eq (rat_add a c) (rat_add b c)
source
theorem rat_add_comm (a b : myrat) :
rat_add a b = rat_add b a
source
theorem rat_add_assoc (a b c : myrat) :
rat_add a (rat_add b c) = rat_add (rat_add a b) c
source
theorem add_sub_rat (a b c d : myrat) :
defined a → rat_eq a b → rat_eq (rat_add a c) d → rat_eq (rat_add b c) d
source
theorem add_sub_rat_alt (a b c d : myrat) :
defined a → rat_eq a b → rat_eq (rat_add c a) d → rat_eq (rat_add c b) d
source
theorem add_self_nonzero_rat (a : myrat) :
¬iszero_rat a → ¬iszero_rat (rat_add a a)
source
theorem rat_mul_zero_alt (a : myrat) :
rat_eq rat_zero (rat_mul a rat_zero)
source
theorem rat_mul_one (a b : myrat) :
rat_eq a rat_one → rat_eq b (rat_mul a b)
source
theorem rat_mul_one_rw (a : myrat) :
rat_mul a rat_one = a
source
theorem rat_mul_distrib (a b c : myrat) :
rat_eq (rat_mul (rat_add a b) c) (rat_add (rat_mul a c) (rat_mul b c))
source
theorem rat_mul_distrib_inv (a b c : myrat) :
rat_eq (rat_add (rat_mul a c) (rat_mul b c)) (rat_mul (rat_add a b) c)
source
theorem rat_mul_distrib_alt (a b c : myrat) :
rat_eq (rat_mul a (rat_add b c)) (rat_add (rat_mul a b) (rat_mul a c))
source
theorem rat_one_mul (a b : myrat) :
rat_eq a rat_one → rat_eq (rat_mul a b) b
source
def rat_reciprocal  :
myrat → myrat
Equations
source
theorem reciprocal_mul_inv (a : myrat) :
rat_eq rat_one (rat_mul a (rat_reciprocal a))
source
theorem reciprocal_inv_mul (a : myrat) :
rat_eq (rat_mul a (rat_reciprocal a)) rat_one
source
theorem reciprocal_mul_cancel (a b : myrat) :
rat_eq a (rat_mul a (rat_mul b (rat_reciprocal b)))
source
theorem reciprocal_def (a : myrat) :
defined a → ¬iszero_rat a → defined (rat_reciprocal a)
source
theorem reciprocal_undef_undef (a : myrat) :
¬defined a → ¬defined (rat_reciprocal a)
source
theorem reciprocal_zero_undef (a : myrat) :
iszero_rat a → ¬defined (rat_reciprocal a)
source
theorem reciprocal_mul_inv_alt (a b : myrat) :
rat_eq a (rat_mul (rat_mul a b) (rat_reciprocal b))
source
theorem reciprocal_eq (a b : myrat) :
rat_eq a b → rat_eq (rat_reciprocal a) (rat_reciprocal b)
source
theorem half_reciprocal_mul (a : myrat) :
rat_eq (rat_reciprocal rat_two) (rat_mul a (rat_reciprocal (rat_add a a)))
source
def negate_rat  :
myrat → myrat
Equations
source
theorem negate_def (a : myrat) :
defined a → defined (negate_rat a)
source
theorem negate_undef (a : myrat) :
¬defined a → ¬defined (negate_rat a)
source
theorem negate_eq_rat (a b : myrat) :
rat_eq a b → rat_eq (negate_rat a) (negate_rat b)
source
theorem double_negate (a : myrat) :
negate_rat (negate_rat a) = a
source
theorem mul_negate (a b : myrat) :
rat_eq (rat_mul a (negate_rat b)) (negate_rat (rat_mul a b))
source
theorem mul_negate_rw (a b : myrat) :
rat_mul a (negate_rat b) = negate_rat (rat_mul a b)
source
theorem mul_negate_alt_rw (a b : myrat) :
rat_mul (negate_rat a) b = rat_mul a (negate_rat b)
source
theorem add_negate_rat (a : myrat) :
rat_eq (rat_add a (negate_rat a)) rat_zero
source
theorem add_negate_rat_alt (a : myrat) :
iszero_rat (rat_add a (negate_rat a))
source
theorem iszero_mul_rat (a b : myrat) :
¬iszero_rat b → defined b → iszero_rat (rat_mul a b) → iszero_rat a
source
def linear_formula  :
myrat → myrat → myrat
Equations
source
theorem linear_formula_works (a b : myrat) :
rat_eq (rat_add (rat_mul a (linear_formula a b)) b) rat_zero
source
inductive rat_plus_sqrt (a : myrat) :
Type
source
def zero_rps (k : myrat) :
rat_plus_sqrt k
Equations
source
def defined_rps (k : myrat) :
rat_plus_sqrt k → Prop
Equations
source
def rps_equal (k : myrat) :
rat_plus_sqrt k → rat_plus_sqrt k → Prop
Equations
source
def iszero_rps (k : myrat) :
rat_plus_sqrt k → Prop
Equations
source
def add_rps (k : myrat) :
rat_plus_sqrt k → rat_plus_sqrt k → rat_plus_sqrt k
Equations
source
def negate_rps (k : myrat) :
rat_plus_sqrt k → rat_plus_sqrt k
Equations
source
def mul_rps (k : myrat) :
rat_plus_sqrt k → rat_plus_sqrt k → rat_plus_sqrt k
Equations
source
def add_rps_to_rat (k : myrat) :
rat_plus_sqrt k → myrat → rat_plus_sqrt k
Equations
source
def mul_rps_by_rat (k : myrat) :
rat_plus_sqrt k → myrat → rat_plus_sqrt k
Equations
source
def sqrt (k : myrat) :
rat_plus_sqrt k
Equations
source
theorem add_zero_rps_alt (k : myrat) (a : rat_plus_sqrt k) :
add_rps k a (zero_rps k) = a
source
theorem add_comm_rps (k : myrat) (a b : rat_plus_sqrt k) :
add_rps k a b = add_rps k b a
source
theorem add_assoc_rps (k : myrat) (a b c : rat_plus_sqrt k) :
add_rps k (add_rps k a b) c = add_rps k a (add_rps k b c)
source
theorem add_zero_rps (k : myrat) (a b : rat_plus_sqrt k) :
iszero_rps k a → rps_equal k (add_rps k a b) b
source
theorem add_def_rps (k : myrat) (a b : rat_plus_sqrt k) :
defined_rps k a → defined_rps k b → defined_rps k (add_rps k a b)
source
theorem negate_and (a b c : Prop) :
¬(a ∧ b ∧ c) → ¬a ∨ ¬b ∨ ¬c
source
theorem add_undef_rps (k : myrat) (a b : rat_plus_sqrt k) :
¬defined_rps k a → ¬defined_rps k (add_rps k a b)
source
theorem negate_add_inv_rps (k : myrat) (a : rat_plus_sqrt k) :
iszero_rps k (add_rps k a (negate_rps k a))
source
theorem mul_comm_rps (k : myrat) (a b : rat_plus_sqrt k) :
mul_rps k a b = mul_rps k b a
source
theorem mul_assoc_rps (k : myrat) (a b c : rat_plus_sqrt k) :
rps_equal k (mul_rps k (mul_rps k a b) c) (mul_rps k a (mul_rps k b c))
source
theorem mul_distrib_rps (k : myrat) (a b c : rat_plus_sqrt k) :
rps_equal k (mul_rps k (add_rps k a b) c) (add_rps k (mul_rps k a c) (mul_rps k b c))
source
def rat_four  :
myrat
Equations
source
def discriminant  :
myrat → myrat → myrat → myrat
Equations
source
def quadratic_formula (a b c : myrat) :
rat_plus_sqrt (discriminant a b c)
Equations
source
def quadratic_subst (k : myrat) :
myrat → myrat → myrat → rat_plus_sqrt k → rat_plus_sqrt k
Equations
source
theorem half_defined  :
defined (rat_reciprocal rat_two)
source
theorem rat_two_defined  :
defined rat_two
source
theorem four_divided_by_two  :
rat_eq (rat_mul rat_four (rat_reciprocal rat_two)) rat_two
source
theorem add_two_halves (a : myrat) :
rat_eq a (rat_add (rat_mul a (rat_reciprocal rat_two)) (rat_mul a (rat_reciprocal rat_two)))
source
theorem mul_two_rat (a : myrat) :
rat_eq (rat_mul a rat_two) (rat_add a a)
source
theorem rat_zero_defined  :
defined rat_zero
source
theorem quadratic_formula_works (a b c : myrat) :
iszero_rps (discriminant a b c) (quadratic_subst (discriminant a b c) a b c (quadratic_formula a b c))