Module prop::eq

Tactics for Logical EQ.

Functions

• absurd
  false == false.
• anti
  (a == ¬a) => 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)
• contra
  ¬(a == b) ∧ a => ¬b.
• contra_excm
  ¬(a == b) ∧ a => ¬b.
• double_neg
  a => (a == ¬¬a).
• eq_left
  (a == b) => (a == c) == (b == c).
• eq_not_to_neq
  (a == ¬b) => ¬(a == b).
• eq_right
  (a == b) => (c == a) == (c == b).
• eq_to_eq_excm
  (a == b) => ((a ⋁ ¬a) == (b ⋁ ¬b)).
• imply_to_or_da
  (a => b) = (¬a ∨ b).
• imply_to_or_db
  (a => b) = (¬a ∨ b).
• in_left
  Makes it easier to traverse.
• in_left_arg
  (a == b) ∧ (a == c) => (c == b)
• in_right
  Makes it easier to traverse.
• 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) => (¬b == ¬a)
• neq_left
  (a == b) ⋀ ¬(a == c) => ¬(b == c).
• neq_right
  (a == b) ⋀ ¬(b == c) => ¬(a == c).
• neq_symmetry
  ¬(a == b) => ¬(b == a).
• neq_to_eq_not
  ¬(a == b) => (a == ¬b).
• neq_to_nand
  ¬(a == b) => ¬(a ⋀ b).
• refl
  a == a.
• rev_modus_tollens
  (¬a == ¬b) => (b == a).
• rev_modus_tollens_eq_excm
  (¬a == ¬b) ∧ ((a ∨ ¬a) == (b ∨ ¬b)) => (b == a).
• rev_modus_tollens_excm
  (¬a == ¬b) ∧ (a ∨ ¬a) ∧ (b ∨ ¬b) => (b == a).
• rev_modus_tollens_imply_excm
  (¬a == ¬b) ∧ (a => (b ∨ ¬b)) ∧ (b => (b ∨ ¬b)) => (b == a).
• swap_left
  (a == b) == c => (b == a) == c.
• swap_right
  a == (b == c) => a == (c == b).
• symmetry
  (a == b) => (b == a).
• symmetry_eq
  (a == b) == (b == a).
• to_eq_false
  ¬a => (a == false).
• trans3
  (a == b) ∧ (b == c) ∧ (c == d) => (a == d).
• trans4
  (a == b) ∧ (b == c) ∧ (c == d) ∧ (d == e) => (a == e).
• trans5
  (a == b) ∧ (b == c) ∧ (c == d) ∧ (d == e) ∧ (e == f) => (a == f).
• 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.