3. Summary of tactics & De Morgan

14/10/22

		How to prove	How to use?
Conjunction	$P\wedge Q$	constructor,	cases h with p q,
Disjunction	$P\vee Q$	Right/Left	cases h with p q,
Implication	$P\rightarrow Q$	assume h,	apply h,
Falsum	$false$	x	cases h,
Vemum	$true$	constructor,	x

De Morgan 1

¬(P ∨ Q) ↔ ¬ P ∧ ¬ Q

¬(P ∧ Q) ↔ ¬ P ∨ ¬ Q

Code

variables P Q R : Prop

theorem distr : P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R :=
begin
  constructor,
  assume pqr,
  cases pqr with p qr,
  cases qr with q r,
  left,
  constructor,
  exact p,
  exact q,

  right,
  constructor,
  exact p,
  exact r,

  assume pqpr,
  cases pqpr with pq pr,
  cases pq with p q,
  constructor,
  exact p,
  left,
  exact q,

  cases pr with p r,
  constructor,
  exact p,
  right,
  exact r,
  
end


theorem deMorgan1 :
¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q :=
begin
  constructor,
  assume npq,
  constructor,
  assume p,
  apply npq,
  left,
  exact p,
  
  assume q,
  apply npq,
  right,
  exact q,

  assume npq,
  cases npq with np nq,
  assume pq,
  cases pq with p q,
  apply np,
  exact p,

  apply nq,
  exact q,
end