1  variables (P Q S : Prop)
 2  -- P = "Dragons exist"
 3  -- Q = "Unicorns exist"
 4  -- S = "Goblins exist"
 5  -- <dead dragon> : P
 6  
 7  theorem p_and_q (hP : P) (hQ : Q) : P ∧ Q := and.intro hP hQ
 8  theorem p_and_q_implies_p (h : P ∧ Q) : P := and.left h
 9  theorem p_and_q_implies_q (h : P ∧ Q) : Q := and.right h
10  theorem p_and_q_implies_q_and_p (h : P ∧ Q) : Q ∧ P := and.intro (and.right h) (and.left h)
11  
12  theorem p_implies_p_or_q (hP : P) : P ∨ Q := or.inl hP
13  theorem q_implies_p_or_q (hQ : Q) : P ∨ Q := or.inr hQ
14  theorem p_or_q_implies_q_or_p (h : P ∨ Q) : Q ∨ P :=
15  or.elim h (λ hP : P, or.inr hP) (λ hQ : Q, or.inl hQ)
16  
17  theorem modus_ponens (h : P → Q) (hP : P) : Q := h hP
18  
19  -- P → Q → S
20  -- P → (Q → S)
21  -- P ∧ Q → S
22  example (h : P → Q → S) (hP : P) (hQ : Q) : S :=
23  have hQS : Q → S, from h hP,
24  hQS hQ
25  
26  
27  def alwaysTrue : true := trivial
28  -- _ : False
29  -- def alwaysFalse : false := _
30  
31  -- → = "not" \n
32  -- →P
33  -- P → false
34  -- "if dragons existing implies unicorns must exist,
35  -- and unicorns don't exist, then dragons can't exist"
36  
37  theorem contrapositive (hPQ : P → Q) (hnQ : Q → false) : P → false :=
38  λ hP : P,
39  have hQ : Q, from hPQ hP,
40  hnQ hQ
41  
42  theorem explode (hP : P) (hnP : P → false) : Q :=
43  false.elim (hnP hP)
44  
45  theorem lem : P ∨ false := or.inl (sorry : P)
46  
47  -- ↔
48  theorem and_swap : (P ∧ Q) ↔ (Q ∧ P) :=
49  have forwards : (P ∧ Q) → (Q ∧ P), from
50  λ (h : P ∧ Q), and.intro (and.right h) (and.left h),
51  have backwards : (Q ∧ P) → (P ∧ Q), from
52  λ (h : Q ∧ P), and.intro (and.right h) (and.left h),
53  iff.intro forwards backwards
54  
55  theorem and_swap_tactic : (P ∧ Q) ↔ (Q ∧ P) :=
56  iff.intro
57  (λ h, and.intro (and.right h) (and.left h))
58  (λ h, and.intro (and.right h) (and.left h))
59  
60  theorem discrete : ((P → Q) → (Q → S)) ↔ (Q → S) :=
61  iff.intro
62  (λ h, λ hQ, h (λ hp : P, hQ) hQ)
63  (λ hQS, λ hPQ, hQS)
64  
65  -- x → y
66  -- Eq.refl 0 : 0 = 0
67  -- Rq.refl x : x = x
68  -- : 1  = 0
69  -- Eq.refl 0 : 0 = 0
70  -- Eq.refl 1 : 1 = 1
71  
72  -- 2 + 2 = 4
73  -- 4 = 4
74  -- Eq.refl 4
75  theorem twoPlusTwo : (2 + 2 : nat) = 4 := eq.refl 4
76  
77  -- uocsclub.net/lean