Module prop::eq

Tactics for Logical EQ.

Functions

absurd	false = false.
assoc	(a = b) = c => a = (b = c).
assoc_eq	((a = b) = c) = (a = (b = c)).
assoc_left	(a = b) = c => (b = c) => a.
assoc_right	(a = b) = c => a => (b = c)
commute	(a = b) => (b = a).
commute_eq	(a = b) = (b = a).
contra	¬(a = b) ∧ a => ¬b.
double_neg	a => (a = ¬¬a).
imply_to_or	(a => b) = (¬a ∨ b).
in_left_arg	(a = b) ∧ (a = c) => (c = b)
in_right_arg	See transitivity.
inv_triangle	¬(a = b) = ¬(c = b) => (a = c).
is_false	(false = a) => ¬a.
is_true	(true = a) => a.
modus_tollens	(a = b) = (¬a = ¬b)
refl	a = a.
rev_modus_tollens	(¬a = ¬b) = (b = a).
swap_left	(a = b) = c => (b = a) = c.
swap_right	a = (b = c) => a = (c = b).
transitivity	(a = b) ∧ (b = c) => (a = c).
transpose	(a = b) = (c = d) => (a = c) = (b = d).
triangle	(a = b) = (c = b) => (a = c).
true_eq	There is an a : A is the same as A being true.