1. Propositional logic in tautology

07/10/22

/-Lecture 2: Propositional logic in tautology-/

variables P Q R : Prop

#check P → Q --\->
-- if P then Q, implication

#check P ∧ Q -- \and
-- P and Q, conjunction

#check P ∨ Q -- \or
-- P or Q, disjunction

#check ¬P -- \not
-- not P, negation
-- ¬P = P → false

#check P ↔ Q -- \iff
-- P if and only if Q, equivalnce
-- P ↔ Q = (P→Q) ∧ (Q→P)

#check true
#check false

theorem I : P → P :=

begin
    assume h,
    exact h,
end

#print I

theorem C:(P → Q) → (Q → R) → (P → R) :=
begin
    assume pq,
    assume qr,
    assume p,
    apply qr,
    apply pq,
    exact p,
end

#print C

theorem swap :
    (P → Q → R) → (Q → P → R) :=
begin
    assume pqr,
    assume q,
    assume p,
    apply pqr,
    exact p,
    exact q,
end

#print swap

Exact only works if the assumption exactly matches the goal