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.

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.