Dependent and connective

DAnd.lean

import Lean

/--
`(h : a) ∧ b`, the "dependent and" connective. This is a conjunction
just like `And`, but to even state the right hand side proposition,
we need the left hand side to hold.
Due to proof irrelevance, this is not actually quite as dependent as
it might look.
-/
structure DAnd {a : Prop} (b : a → Prop) : Prop where
  intro ::
  {left : a}
  right : b left

open Lean TSyntax.Compat in
@[inherit_doc DAnd]
macro:35 a:bracketedExplicitBinders " ∧ " b:term:35  : term => expandBrackedBinders ``DAnd a b

open Lean PrettyPrinter Delaborator SubExpr TSyntax.Compat in
/--
Pretty-print expressions of the form `DAnd (a := a) fun ha => b ha` as
syntax of the form `(ha : a) ∧ b ha`, where
- `a` is a term (denoting a prop),
- `ha` is an (implied) identifier
- `b ha` is any term that can reference the `ha` bound variable.
-/
@[app_delab DAnd]
def delabDAnd : Delab := do
  -- get the expression we're delaborating
  let e : Expr ← getExpr
  -- it must be of the specific shape, otherwise give up
  let .app (.app _ lhs) (.lam binderName binderType body binderInfo) := e | failure
  -- pick a name for the binder (`ha` in the doc above); if the binder had a name
  -- in the original code, try to use that, otherwise make one up, but try to
  -- prevent shadowing other names in the local context.
  let binderName' : Name ← getUnusedName binderName body
  -- recursively delaborate LHS (`a` in the doc above)
  let delab_lhs : Term ← descend lhs 0 delab
  -- declare the binder variable...
  Meta.withLocalDecl binderName' binderInfo binderType fun fvar => do
    -- make an identifier that uses the name chosen above, and references the
    -- just declared variable
    let binderIdent : Ident ← mkAnnotatedIdent binderName' fvar
    -- recursively delaborate RHS (`b ha` in the doc above), substituting the
    -- "loose bound variable" for our binder variable
    let rhs : Term ← descend (body.instantiate1 fvar) 1 delab
    -- let ourselves use te `∧` character
    let dandSymbol := mkNode ``Parser.Term.quotedName #[Syntax.mkNameLit "∧"]
    -- finally, delaborate to this form:
    `(($binderIdent : $delab_lhs) $dandSymbol $rhs)

def DAnd.of_and {a b : Prop} (h : a ∧ b) : (_ : a) ∧ b :=
  DAnd.intro (left := h.left) h.right

def DAnd.to_and {a b : Prop} (da : (_ : a) ∧ b) : a ∧ b :=
  And.intro da.left da.right

example : (_ : 2 + 2 = 4) ∧ 2 + 3 = 5 → 2 + 2 = 4 ∧ 2 + 3 = 5
  | da => da.to_and

def DAnd.of_exists {a : Prop} {b : a → Prop} (h : ∃ a, b a) : (ha : a) ∧ b ha :=
  have ⟨_, hb⟩ := h
  DAnd.intro hb

def DAnd.to_exists {a : Prop} {b : a → Prop} (da : (ha : a) ∧ b ha) : ∃ a, b a :=
  Exists.intro da.left da.right

def DAnd.elim.{u} {a : Prop} {b : a → Prop} {γ : Sort u}
  (f : (ha : a) → b ha → γ) (h : (ha : a) ∧ b ha) : γ := f h.left h.right

theorem DAnd.assoc {a : Prop} {b : a → Prop} {c : (ha : a) → b ha -> Prop}
  : (ha : a) ∧ (hb : b ha) ∧ c ha hb ↔ (h : (ha : a) ∧ b ha) ∧ c h.left h.right := by
  apply Iff.intro <;>
  intro da <;>
  apply DAnd.intro
  -- mp
  exact da.right.right
  apply DAnd.intro
  exact da.right.left
  -- mpr
  apply DAnd.intro
  exact da.right

theorem DAnd.assoc_and {a c : Prop} {b : a → Prop}
  : (ha : a) ∧ (b ha ∧ c) ↔ ((ha : a) ∧ b ha) ∧ c := by
  apply Iff.intro
  case mp =>
    intro da
    exact And.intro (DAnd.intro da.right.left) da.right.right
  case mpr =>
    intro h
    exact DAnd.intro (And.intro h.left.right h.right)

theorem DAnd.distr_and_right {a : Prop} {b c : a → Prop}
  : (ha : a) ∧ (b ha ∧ c ha) ↔ ((ha : a) ∧ b ha) ∧ ((ha : a) ∧ c ha) := by
  apply Iff.intro
  case mp =>
    intro da
    apply And.intro
    exact DAnd.intro da.right.left
    exact DAnd.intro da.right.right
  case mpr =>
    intro h
    apply DAnd.intro
    exact And.intro h.left.right h.right.right

theorem DAnd.distr_and_left {a b : Prop} {c : a ∨ b → Prop} :
  ((ha : a) ∧ c (Or.inl ha)) ∧ ((hb : b) ∧ c (Or.inr hb)) ↔ (h : a ∧ b) ∧ c (Or.inl h.left) := by
  apply Iff.intro
  case mp =>
    intro h
    apply DAnd.intro
    exact h.left.right
    exact And.intro h.left.left h.right.left
  case mpr =>
    intro da
    apply And.intro
    exact DAnd.intro (left := da.left.left) da.right
    exact DAnd.intro (left := da.left.right) da.right

theorem DAnd.distr_or_right {a : Prop} {b c : a → Prop}
  : (ha : a) ∧ (b ha ∨ c ha) ↔ ((ha : a) ∧ b ha) ∨ ((ha : a) ∧ c ha) := by
  apply Iff.intro
  case mp =>
    intro da
    cases da.right with
    | inl hb => exact Or.inl (DAnd.intro hb)
    | inr hc => exact Or.inr (DAnd.intro hc)
  case mpr =>
    intro o
    cases o with
    | inl hb => exact DAnd.intro (Or.inl hb.right)
    | inr hc => exact DAnd.intro (Or.inr hc.right)

theorem DAnd.distr_or_left {a b : Prop} {c : a ∨ b → Prop} :
  ((ha : a) ∧ c (Or.inl ha)) ∨ ((hb : b) ∧ c (Or.inr hb)) ↔ (h : a ∨ b) ∧ c h := by
  apply Iff.intro
  case mp =>
    intro o
    cases o with
    | inl ha => exact DAnd.intro ha.right
    | inr hb => exact DAnd.intro hb.right
  case mpr =>
    intro da
    cases da.left with
    | inl ha => exact Or.inl (DAnd.intro (left := ha) da.right)
    | inr hb => exact Or.inr (DAnd.intro (left := hb) da.right)

@[simp]
theorem DAnd.true_and {b : True → Prop} : ((h : True) ∧ b h) ↔ b True.intro :=
  Iff.intro DAnd.right DAnd.intro

@[simp]
theorem DAnd.false_and {b : False → Prop} : ((h : False) ∧ b h) ↔ False :=
  Iff.intro DAnd.left False.elim

@[simp]
theorem DAnd.and_true {a : Prop} : (_ : a) ∧ True ↔ a := by
  apply Iff.intro
  case mp =>
    exact DAnd.left
  case mpr =>
    intro h
    exact DAnd.intro (left := h) True.intro

@[simp]
theorem DAnd.and_false {a : Prop} : (_ : a) ∧ False ↔ False := by
  apply Iff.intro
  case mp =>
    exact DAnd.right
  case mpr =>
    intro f
    contradiction

@[simp]
theorem DAnd.and_self {a : Prop} : (_ : a) ∧ a ↔ a := by
  apply Iff.intro
  case mp =>
    exact DAnd.left
  case mpr =>
    intro h
    exact DAnd.intro (left := h) h

theorem DAnd.not_and {a : Prop} {b : a → Prop} : ¬((h : a) ∧ b h) ↔ (∀ h, ¬ b h) := by
  apply Iff.intro
  case mp =>
    intro not_da ha hb
    exact not_da.elim (DAnd.intro hb)
  case mpr =>
    intro h da
    exact (h da.left).elim da.right

theorem DAnd.not_and' {a : Prop} {b : a → Prop} : ¬a ∨ (h : a) ∧ ¬b h → ¬((h : a) ∧ b h) := by
  intro h
  cases h
  case inl hna =>
    intro hda
    exact hna hda.left
  case inr hnb =>
    intro hda
    exact hnb.right hda.right

theorem DAnd.not_and_dec {a : Prop} [da : Decidable a] {b : a → Prop} : ¬((h : a) ∧ b h) ↔ ¬a ∨ (h : a) ∧ ¬b h := by
  apply Iff.intro
  intro hnda
  cases da
  case mp.isFalse hna => exact Or.inl hna
  case mp.isTrue ha =>
    apply Or.inr
    apply DAnd.intro (left := ha)
    intro hb
    exact hnda (DAnd.intro hb)
  case mpr => exact DAnd.not_and'

theorem DAnd.not_or {a : Prop} {b : ¬a → Prop} : ¬(a ∨ ∀ hna, b hna) ↔ (hna : ¬a) ∧ (¬ b hna) := by
  apply Iff.intro
  case mp =>
    intro h
    have hna (ha : a) := h (Or.inl ha)
    have hnb (hb : b hna) := h (Or.inr fun _ => hb)
    exact DAnd.intro hnb
  case mpr =>
    intro da h
    cases h
    case inl ha => exact da.left ha
    case inr hb => exact da.right (hb da.left)

instance {a : Prop} {b : a → Prop} [da : Decidable a] [db : (h : a) → Decidable (b h)]
  : Decidable ((h : a) ∧ b h) :=
  match da with
  | isFalse na => isFalse fun h => na.elim h.left
  | isTrue ha => match db ha with
    | isFalse nb => isFalse fun h => nb.elim h.right
    | isTrue hb => isTrue (DAnd.intro hb)