Module prop::imply

Tactics for Logical IMPLY.

Functions

• absurd
  false => a.
• and_map
  a => (b => (a ∧ b)).
• chain
  ((a ∧ b) => c) => (a => (b => c)).
• double_neg
  (a => b) => (¬¬a => ¬¬b).
• eq_left
  (a == b) => (a => c) == (b => c).
• eq_right
  (a == b) => (c => a) == (b => c).
• flip_neg_left
  (¬a => b) => (¬b => a).
• flip_neg_left_excm
  (¬a => b) ⋀ (a ⋁ ¬a) => (¬b => a).
• flip_neg_right
  (a => ¬b) => (b => ¬a).
• from_or
  (¬a ∨ b) => (a => b).
• id
  a => a.
• 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
  (a => b) ∧ (b == c) => (a => c).
• join
  (a => c) ∧ (b => c) => ((a ∧ b) => c).
• modus_ponens
  (a => b) ∧ a => b
• modus_tollens
  (a => b) => (¬b => ¬a).
• or_split_da
  (a => (b ∨ c)) => (a => b) ∨ (a => c).
• or_split_db
  (a => (b ∨ c)) => (a => b) ∨ (a => c).
• or_split_dc
  (a => (b ∨ c)) => (a => b) ∨ (a => c).
• or_split_excm_a
  (a => (b ∨ c)) ⋀ (a ⋁ ¬a) => (a => b) ∨ (a => c).
• reduce
  (a => (a => b)) => (a => b).
• reorder_args
  (a => (b => c)) => (b => (a => c))
• rev_chain
  a => (b => c) => ((a ∧ b) => c).
• rev_double_neg
  (¬¬a => ¬¬b) => (a => b).
• rev_double_neg_eq_excm
  (¬¬a => ¬¬b) ∧ ((a ∨ ¬a) == (b ∨ ¬b)) => (a => b).
• rev_double_neg_excm
  (¬¬a => ¬¬b) => (a => b).
• rev_double_neg_imply_excm
  (¬¬a => ¬¬b) ∧ (a => (b ∨ ¬b)) => (a => b).
• rev_modus_ponens
  (b => a) ∧ ¬a => ¬b.
• rev_modus_tollens
  (¬b => ¬a) => (a => b).
• rev_modus_tollens_eq_excm
  (¬b => ¬a) ∧ ((a ∨ ¬a) == (b ∨ ¬b)) => (a => b).
• rev_modus_tollens_excm
  (¬b => ¬a) ∧ (a ∨ ¬a) ∧ (b ∨ ¬b) => (a => b).
• rev_modus_tollens_imply_excm
  (¬b => ¬a) ∧ (a => (b ∨ ¬b)) => (a => b).
• to_or_da
  (a => b) => (¬a ∨ b).
• to_or_db
  (a => b) => (¬a ∨ b).
• to_or_excm_a
  (a => b) ⋀ (a ⋁ ¬a) => (¬a ∨ b).
• to_or_excm_b
  (a => b) => (¬a ∨ b).
• total
  (a => b) ∨ (b => a).
• total_excm
  (a ∨ ¬a) => (a => b) ∨ (b => a).
• transitivity
  (a => b) ∧ (b => c) => (a => c).