2DM3 Tricks!

Contrapositivity is the antitonicity of logical not

Axiom “Demo”: Q ⇒ P

Theorem “Contrapositivity is the antitonicity of logical not”: ¬ P ⇒ ¬ Q
Proof:
    ¬ P
  ⇒⟨ “Contrapositive” with “Demo” ⟩
    ¬ Q

Getting past double implication

Using “Shunting” to get past the right-associativity of implication.
`P ⇒ Q ⇒ R` is `P ⇒ (Q ⇒ R)` with superfluous parenthesis.

Axiom “Demo”: Q ⇒ P ⇒ R

Theorem “Getting past double implication”: Q ∧ P ⇒ R
Proof:
    R
  ⇐⟨ “Consequence” with “Shunting”, “Demo” ⟩
    Q ∧ P
  

Using `Distributivity of ⇒ over ≡` in equivalence hints

We may have the following situation where without this trick it would be annoying to prove.
Using `Distributivity of ⇒ over ≡` allows us to take a theorem that would normally require an implication step into an equivalency.
For instance, we can turn `P ⇒ (Q ≡ R)` into `P ⇒ Q ≡ P ⇒ R` and use this in an equivalence step.

Axiom “Demo”: P ⇒ (Q ≡ R)

Theorem “Using `Distributivity of ⇒ over ≡` in equivalence hints”: P ⇒ Q ≡ P ⇒ R
Proof:
    P ⇒ Q
  ≡⟨ “Demo” with “Distributivity of ⇒ over ≡” ⟩
    P ⇒ R

Using an equality assumption directly

If we know that `R = S` is true, we can simply use it as a hint without any fancy Leibniz/Substitution/etc theorems.

Subproof for `R = S ⇒ R ⊆ S  ∧  S ⊆ R`:
  Assuming `R = S`:
      R ⊆ S ∧ S ⊆ R
    ≡⟨ Assumption `R = S` ⟩
      R ⊆ R ∧ R ⊆ R
    ≡⟨ “Reflexivity of ⊆”, “Identity of ∧” ⟩
      true

Utilizing the `with` keyword to produce equivalency steps

We might have a situation where we want the consequent of “Transitivity of =” but need to prove an equivalence.
“Transitivity of =” is defined as `e = f ∧ f = g ⇒ e = g`.
This can be combined with (3.60) `p ⇒ q ≡ (p ∧ q ≡ p)` to produce `e = f ∧ f = g ≡ e = f ∧ f = g ∧ e = g`.

Axiom “Demo”: P = Q ∧ P = R ∧ Q = R

Theorem “Utilizing the `with` keyword to produce equivalency steps”:
    P = Q ∧ P = R
Proof:
    P = Q ∧ P = R
  ≡⟨ “Transitivity of =” with (3.60) “Definition of Implication” ⟩
    P = Q ∧ P = R ∧ Q = R
  ≡⟨ “Demo” — Now we have the extra subexpression to work with! ⟩
    true