macro "conj_elim" hp:ident hq:ident "from" h:ident : tactic =>
  `(tactic|(have ⟨$hp,$hq⟩ := $h))

macro "conj_intro" h:ident "from" hp:ident hq:ident : tactic =>
  `(tactic|(have $h : _∧_ := And.intro $hp $hq))

macro "disj_elim" hp:ident hq:ident "from" h:term:arg : tactic =>
  `(tactic|(refine Or.elim $h (fun $hp => ?_) (fun $hq => ?_)))

macro "disj_intro_left" h:ident "from" hp:ident q:term:arg : tactic =>
  `(tactic|(have $h : _∨($q) := Or.inl $hp))

macro "disj_intro_right" h:ident "from" p:term:arg hq:ident : tactic =>
  `(tactic|(have $h : ($p)∨_ := Or.inr $hq))

macro "impl_elim" hq:ident "from" hp:ident hpq:ident : tactic =>
  `(tactic|(have $hq := $hpq $hp))

namespace And
theorem elim' {P Q : Prop} {R : Sort} (h : P ∧ Q) (f : P → Q → R) : R :=
  And.elim f h
end And

variable ( S T : Type )
variable ( P Q R : S → Prop )

/- The first group of examples show how quantifiers work in Lean -/




example ( h : ∀ x : S, P x ) ( t : S ) : P t := by
  have h' := h t
  exact h'


example ( h : ∀ x : S, P x ) ( t : S ) : P t := by
  apply h

example : ∀ x : S, P x := by
  intro t

example ( t : S ) ( h : P t ) : ∃ x : S, P x := by
  apply Exists.intro t
  exact h

example {Q:Prop} 
        ( h1 : ∃ x : S, P x )
        ( h2 : ∀ x : S, P x → Q )
        : Q := by
          apply Exists.elim h1
          intro t
          intro hpt
          have h3 := h2 t
          apply h3
          exact hpt




/- The second group involves problems we have already done in English in class. -/


  

example ( h : ( ∀ x : S, P x → Q x ) 
              ∧ ( ∀ y : S, P y → R y ) ) 
        : (∀ x : S, P x → Q x ∧ R x) := by
  intro t -- We are using universal introduction.  Now our goal is P t → Q t ∧ R t.
  intro hpt -- Our goal is an implication, so we use implication introduction.  We assume P t and the goal becomes Q t ∧ R t.
  conj_elim h₁ h₂ from h -- We break our hypothesis into two using conjunction elimination.
  apply And.intro -- We need to prove a conjunction, so we split it into two goals : Q t and R t.
  · have h₃  := h₁ t -- We prove Q t first.  By universal elimination, we get P t → Q t from h₁ applied to t.
    apply h₃ -- Our goal is Q t and we have P t → Q t, so we can simplify the goal to P t.
    exact hpt -- And we already know P t!
  · have h₄ := h₂ t -- Our second goal is R t.  Use use universal elimination again to get P t → R t from h₂ applied to t.
    apply h₄ -- We simplify the goal from R t to P t using P t → R t.
    exact hpt -- And again, P t is something we know.



/- This example shows existential introduction, existential elimination, and universal elimination. -/
example ( h : ( ∃ x : S, P x ) ∧ ( ∀ x : S, Q x ) ) : ∃ x : S, P x ∧ Q x := by
  conj_elim h₁ h₂ from h -- First break apart the conjunction h into h₁ : ∃ x, P x and h₂ : ∀ (x:S), Q x.
  apply Exists.elim h₁ -- Apply existential elimination to h₁ : ∃ x, P x...
  intro t -- ... that gives us a t : S ... 
  intro hpt -- ... such that P t is true.
  apply Exists.intro t -- Our goal is to show ∃ x, P x ∧ Q x.  We'll use x = t.  Our goal becomes P t ∧ Q t.
  apply And.intro -- Our goal is a conjunction so we use conjunction introduction.  That gives two goals.
  exact hpt -- The first goal is P t, which we got when we introduced t.
  exact h₂ t -- The second goal is Q t, which we have by universal elimination on h₂ : ∀ t:S, Q t and t:S.



example ( h : ∀ x : S, P x ∧ Q x ) 
        : ( ∀ x : S, P x ) ∧ ( ∀ x : S, Q x )
        := by
          apply And.intro
          intro t
          have h1 := h t
          have ⟨ hpt, hqt ⟩ := h1
          exact hpt
          intro t
          have h2 := h t
          have ⟨ hpt, hqt ⟩ := h2
          exact hqt


example ( h : ∃ x : S, P x ∨ Q x ) 
        : ( ∃ x : S, P x ) ∨ ( ∃ x : S, Q x ) 
        := by
          apply Exists.elim h
          intro t
          intro hptqt
          apply Or.elim hptqt
          intro hpt
          apply Or.intro_left
          apply Exists.intro t
          exact hpt
          intro hqt
          apply Or.intro_right
          apply Exists.intro t
          exact hqt





 

 /- The third group will require combining even more ideas.  We haven't done these in class yet. -/


open Classical 
/- This is a hint that we'll need the excluded middle or proof by contradiction somewhere. -/

theorem not_forall_from_exists_not { P:T → Prop }
  (h : ∃ x:T, ¬ P x) : ¬ ∀ x:T, P x := by
  /- Our goal is to show ¬ ∀ x:T, P x. -/
  intro h₁ /- We prove a negation by assuming the thing we want to negate and deriving a contradiction. -/
  obtain ⟨t, hnpt⟩ := h /- h says that there is some x in T where ¬ P x, so we can introduce a t:T and hnpt:¬P t to our knowledge. -/
  have := h₁ t /- h₁ says that P x is true for every x in T, so we can apply it to t, since t is in T. This gives us P t. -/
  contradiction /- But now we have both P t and ¬ P t, which is a contradiction. -/


theorem not_exists_from_forall_not { P:T → Prop }
  (h : ∀ x:T, ¬ P x) : ¬ ∃ x:T, P x := by
    intro h₁ /- We have to prove ¬ ∃ x:T, P x, so we assume ∃ x:T, P x and derive a contradiction. -/
    obtain ⟨t,hpt⟩ := h₁ /- h₁ says there is an x in T where P x is true, so we can introduce a t in T and P t. -/
    have h₂ := h t /- h applies to every x in T so it applied to t.  This gives ¬ P t. -/
    contradiction /- And ¬ P t contradicts P t. -/



theorem forall_not_from_not_exists { P:T → Prop }
  (h : ¬ ∃ x:T, P x) : ∀ x:T, ¬ P x := by
    /- Our goal is ∀ x:T, ¬ P x. -/
    intro t /- The goal is universally quantified, so we introduce t in T and we need to show ¬ P t. -/
    intro hpt /- We prove ¬ P t by assuming P t and deriving a contradiction. -/
    /- Now we need a plan.  Where will the contradiction come from?  The goal will be to contradict ¬ ∃ x, P x. -/
    have h₁ : ∃ x, P x := by
        apply Exists.intro t
        exact hpt
    contradiction



theorem exists_not_from_not_forall { P:T → Prop }
  (h : ¬ ∀ x:T, P x) : ∃ x:T, ¬ P x := by
  /- Our goal is ∃ x:T, ¬ P x. -/
  apply byContradiction /- We will argue by contradiction.  This changes our goal to (original goal) → False. -/
  intro a /- Our goal is ¬ ∃x, ¬ P x so we assume ∃ x, ¬ P x and derive a contradiction. -/
  apply h /- h says that ∀ x:T, P x is false, so we can obtain a contradiction by proving ∀ x:T, P x.  Now our goal becomes ∀ x:T, P x. -/
  intro t /- We prove the universally quantified statement ∀ x:T, P t by introducing t an arbitrary t in T and showing that P t is true -/
  apply byContradiction /- We'll do this one by contradiction again.  This changes our goal to showing that the opposite of our goal is false. -/
  intro hnpt /- We show ¬ P t → False by assuming ¬ P t and deriving a contradiction. -/
  apply a /- Since ¬ ∃ x, ¬ P x, we can get a contradiction by proving ∃ x, ¬ P x. -/
  apply Exists.intro t /- To prove an existentially quantified statement, we just need to find some x in T such that ¬ P x.  We'll use t. Our goal changes to showing ¬ P t. -/
  exact hnpt /- And we already know ¬ P t. -/





example ( h1 : ∀ x : S, P x ∨ Q x )
        ( h2 : ∃ x : S, ¬ Q x )
        : ∃ x : S, P x := by
          apply Exists.elim h2
          intro t
          intro hnqt
          apply Exists.intro t
          have h3 := h1 t
          apply Or.elim h3
          intro hpt
          exact hpt
          intro hqt
          contradiction