LeanLogicPuzzle.lean

theorem dne_iff_lem :
  (∀p : Prop, ¬¬p -> p) ↔ (∀p: Prop, p ∨ ¬p) := by
    unfold Not
    constructor
    · intros dne q
      apply dne
      intros h0
      apply h0
      right
      intros hq
      apply h0
      left
      exact hq
    · intros lem q h0
      have lemq := lem q
      cases lemq with
      | inl h1 => exact h1
      | inr h1 => exact absurd h1 h0

theorem peirce_iff_lem :
  (∀(p q : Prop), ((p -> q) -> p) -> p) ↔ (∀p: Prop, p ∨ ¬p) := by
    unfold Not
    constructor
    · intros peirce q
      have h0 := peirce (q ∨ (q -> False)) False
      apply h0
      intros h1
      right
      intros hq
      apply h1
      left
      exact hq
    · intros lem p q
      have lemp := lem p
      intros h0
      cases lemp with
      | inl h1 => exact h1
      | inr h1 =>
        apply h0
        intros hp
        exact absurd hp h1

theorem demorgan_not_or :
  ∀(p q : Prop), ¬(p ∨ q) -> ¬p ∧ ¬q := by
    unfold Not
    intros p q h
    constructor
    · intros hp
      apply h
      left
      exact hp
    · intros hq
      apply h
      right
      exact hq

theorem demorgan_and_not :
  ∀(p q : Prop), ¬p /\ ¬q -> ¬(p ∨ q) := by
    unfold Not
    intros p q h0 h1
    obtain ⟨hnp, hnq⟩ := h0
    cases h1 with
    | inl hp => exact absurd hp hnp
    | inr hq => exact absurd hq hnq

theorem demorgan_not_and :
  (∀p : Prop, p ∨ ¬p) -> ∀(p q : Prop), ¬(p ∧ q) -> ¬p ∨ ¬q := by
    unfold Not
    intros lem p q h
    have lemp := lem p
    have lemq := lem q
    cases lemp with
    | inl hp => cases lemq with
      | inl hq => exact absurd ⟨hp, hq⟩ h
      | inr hnq => right; exact hnq
    | inr hnp => left; exact hnp

theorem impl_to_or :
  (∀p : Prop, p ∨ ¬p) -> (∀(p q : Prop), (p -> q) -> ¬p ∨ q) := by
    unfold Not
    intros lem p q h
    have lemp := lem p
    cases lemp with
    | inl hp => right; exact (h hp)
    | inr hnp => left; exact hnp

theorem dni : ∀p : Prop, p -> ¬¬p := by
  unfold Not
  intros p hp hnp
  apply hnp
  exact hp

theorem tne : ∀p : Prop, ¬¬¬p -> ¬p := by
  unfold Not
  intros p h hp
  apply h
  intros hnp
  exact absurd hp hnp