Module prop::eq

Tactics for Logical EQ.

Re-exports

pub use commute as symmetry;

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).

to_eq_false

¬a => (a == false).

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.