natural-number-game

Solututions to the Natural Number Game

advanced-proposition.lean (2104B)

  1 example (P Q : Prop) (p : P) (q : Q) : P ∧ Q :=
  2 begin
  3   split,
  4   exact p,
  5   exact q,
  6 end
  7 
  8 lemma and_symm (P Q : Prop) : P ∧ Q → Q ∧ P :=
  9 begin
 10   intro h,
 11   cases h with p q,
 12   split,
 13   exact q,
 14   exact p,
 15 end
 16 
 17 lemma and_trans (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R :=
 18 begin
 19   intro h1,
 20   cases h1 with p _,
 21   intro h2,
 22   cases h2 with _ r,
 23   split,
 24   exact p,
 25   exact r,
 26 end
 27 
 28 lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
 29 begin
 30   intro p_iff_q,
 31   cases p_iff_q with hpq hqp,
 32   intro q_iff_r,
 33   cases q_iff_r with hqr hrq,
 34   split,
 35   intro p,
 36   apply hqr,
 37   apply hpq,
 38   exact p,
 39   intro r,
 40   apply hqp,
 41   apply hrq,
 42   exact r,
 43 end
 44 
 45 lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
 46 begin
 47   intro p_iff_q,
 48   cases p_iff_q with hpq hqp,
 49   intro q_iff_r,
 50   cases q_iff_r with hqr hrq,
 51   split,
 52   intro p,
 53   apply hqr,
 54   apply hpq,
 55   exact p,
 56   intro r,
 57   apply hqp,
 58   apply hrq,
 59   exact r,
 60 end
 61 
 62 example (P Q : Prop) : Q → (P ∨ Q) :=
 63   begin
 64   intro q,
 65   right,
 66   exact q,
 67 end
 68 
 69 lemma or_symm (P Q : Prop) : P ∨ Q → Q ∨ P :=
 70 begin
 71   intro h,
 72   cases h with p q,
 73   right,
 74   exact p,
 75   left,
 76   exact q,
 77 end
 78 
 79 lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
 80 begin
 81   split,
 82   intro h,
 83   have p := h.1,
 84   cases h.2 with q r,
 85   left,
 86   split,
 87   exact p,
 88   exact q,
 89   right,
 90   split,
 91   exact p,
 92   exact r,
 93   intro h,
 94   cases h with p_and_q p_and_r,
 95   cases p_and_q with p q,
 96   split,
 97   exact p,
 98   left,
 99   exact q,
100   cases p_and_r with p r,
101   split,
102   exact p,
103   right,
104   exact r,
105 end
106 
107 lemma contra (P Q : Prop) : (P ∧ ¬ P) → Q :=
108 begin
109   intro h,
110   rw not_iff_imp_false at h,
111   exfalso,
112   apply h.2,
113   exact h.1,
114 end
115 
116 lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
117 begin
118   by_cases p : P; by_cases q : Q,
119   intros _ _,
120   exact q,
121   intro h,
122   have not_p := h q,
123   exfalso,
124   rw not_iff_imp_false at not_p,
125   apply not_p,
126   exact p,
127   intros _ _,
128   exact q,
129   intros h p,
130   have not_p := h q,
131   rw not_iff_imp_false at not_p,
132   exfalso,
133   apply not_p,
134   exact p,
135 end
136