Module prop::imply

Tactics for Logical IMPLY.

Functions

absurd

false => a.

chain

((a ∧ b) => c) => (a => (b => c)).

double_neg

(a => b) => (¬¬a => ¬¬b).

flip_neg_left

(¬a => b) => (¬b => a).

flip_neg_right

(a => ¬b) => (b => ¬a).

from_or

(¬a ∨ b) => (a => b).

id

a => a.

in_left_arg

(a => b) ∧ (a = c) => (c => b).

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

reorder_args

(a => (b => c)) => (b => (a => c))

rev_double_neg

(¬¬a => ¬¬b) => (a => b).

rev_modus_ponens

(b => a) ∧ ¬a => ¬b.

rev_modus_tollens

(¬b => ¬a) => (a => b).

to_or

(a => b) => (¬a ∨ b).

transitivity

(a => b) ∧ (b => c) => (a => c).