Simproc for ∃ a', ... ∧ a' = a ∧ ...

This module implements the existsAndEq simproc, which triggers on goals of the form ∃ a, P. It checks whether P allows only one possible value for a, and if so, substitutes it, eliminating the leading quantifier.

The procedure traverses the body, branching at each ∧ and entering existential quantifiers, searching for a subexpression of the form a = a' or a' = a for a' that is independent of a. If such an expression is found, all occurrences of a are replaced with a'. If a' depends on variables bound by existential quantifiers, those quantifiers are moved outside.

For example, ∃ a, p a ∧ ∃ b, a = f b ∧ q b will be rewritten as ∃ b, p (f b) ∧ q b.

inductive ExistsAndEq.GoTo : Type

Type for storing the chosen branch at And nodes.

• left : GoTo
• right : GoTo

@[implicit_reducible]

instance ExistsAndEq.instBEqGoTo : BEq GoTo

def ExistsAndEq.instBEqGoTo.beq : GoTo → GoTo → Bool

@[implicit_reducible]

instance ExistsAndEq.instInhabitedGoTo : Inhabited GoTo

def ExistsAndEq.instInhabitedGoTo.default : GoTo

@[reducible, inline]

abbrev ExistsAndEq.Path : Type

Type for storing the path in the body expression leading to a = a'. We store only the chosen directions at each And node because there is no branching at Exists nodes, and Exists nodes will be removed from the body.

@[reducible, inline]

abbrev ExistsAndEq.VarQ : Type

Qq-fied version of Expr. Here, we use it to store free variables introduced when unpacking existential quantifiers.

@[implicit_reducible]

instance ExistsAndEq.instInhabitedVarQ : Inhabited VarQ

@[reducible, inline]

abbrev ExistsAndEq.HypQ : Type

Qq-fied version of Expr proving some P : Prop.

@[implicit_reducible]

instance ExistsAndEq.instInhabitedHypQ : Inhabited HypQ

def ExistsAndEq.mkNestedExists (fvars : List VarQ) (body : Q(Prop)) : Lean.MetaM Q(Prop)

Constructs ∃ f₁ f₂ ... fₙ, body, where [f₁, ..., fₙ] = fvars.

partial def ExistsAndEq.findEqPath {u : Lean.Level} {α : Q(Sort u)} (a : Q(«$α»)) (P : Q(Prop)) : Lean.MetaM (Option Path)

Finds a Path for findEq. It leads to a subexpression a = a' or a' = a, where a' doesn't contain the free variable a. This is a fast version that quickly returns none when the simproc is not applicable.

def ExistsAndEq.findEq {u : Lean.Level} {α : Q(Sort u)} (a : Q(«$α»)) (P : Q(Prop)) (path : Path) : Lean.MetaM (List VarQ × Lean.LocalContext × Q(Prop) × Q(«$α»))

Given P : Prop and a : α, traverses the expression P to find a subexpression of the form a = a' or a' = a for some a'. It branches at each And and walks into existential quantifiers.

Returns a tuple (fvars, lctx, P', a'), where:

• fvars is a list of all variables bound by existential quantifiers along the path.
• lctx is the local context containing all these free variables.
• P' is P with all existential quantifiers along the path removed, and corresponding bound variables replaced with fvars.
• a' is the expression found that must be equal to a. It may contain free variables from fvars.

def ExistsAndEq.withNestedExistsElim {P body goal : Q(Prop)} (exs : List VarQ) (h : Q(«$P»)) (act : Q(«$body») → Lean.MetaM Q(«$goal»)) : Lean.MetaM Q(«$goal»)

When P = ∃ f₁ ... fₙ, body, where exs = [f₁, ..., fₙ], this function takes act : body → goal and proves P → goal using Exists.elim.

Example:

exs = []: act h
exs = [b]:
  P := ∃ b, body
  Exists.elim h (fun b hb ↦ act hb)
exs = [b, c]:
  P := ∃ b c, body
  Exists.elim h (fun b hb ↦
    Exists.elim hb (fun c hc ↦ act hc)
  )
...

def ExistsAndEq.mkAfterToBefore {u : Lean.Level} {α : Q(Sort u)} {p : Q(«$α» → Prop)} {P' : Q(Prop)} (a' : Q(«$α»)) (newBody : Q(Prop)) (fvars : List VarQ) (path : Path) : Lean.MetaM Q(«$P'» → ∃ (a : «$α»), «$p» a)

Generates a proof of P' → ∃ a, p a. We assume that fvars = [f₁, ..., fₙ] are free variables and P' = ∃ f₁ ... fₙ, newBody, and path leads to a = a' in ∃ a, p a.

The proof follows the following structure:

example {α β : Type} (f : β → α) {p : α → Prop} :
    (∃ b, p (f b) ∧ f b = f b) → (∃ a, p a ∧ ∃ b, a = f b) := by
  -- withLocalDeclQ
  intro h
  -- withNestedExistsElim : we unpack all quantifiers in `P` to get `h : newBody`.
  refine h.elim (fun b h ↦ ?_)
  -- use `a'` in the leading existential quantifier
  refine Exists.intro (f b) ?_
  -- then we traverse `newBody` and goal simultaneously
  refine And.intro ?_ ?_
  -- at branches outside the path `h` must coincide with goal
  · replace h := h.left
    exact h
  -- inside path we substitute variables from `fvars` into existential quantifiers.
  · replace h := h.right
    refine Exists.intro b ?_
    -- at the end the goal must be `x' = x'`.
    rfl

partial def ExistsAndEq.withExistsElimAlongPathImp {u : Lean.Level} {α : Q(Sort u)} {P goal : Q(Prop)} (h : Q(«$P»)) {a a' : Q(«$α»)} (exs : List VarQ) (path : Path) (hs : List HypQ) (act : Q(«$a» = «$a'») → List HypQ → Lean.MetaM Q(«$goal»)) : Lean.MetaM Q(«$goal»)

Recursive implementation for withExistsElimAlongPath.

def ExistsAndEq.withExistsElimAlongPath {u : Lean.Level} {α : Q(Sort u)} {P goal : Q(Prop)} (h : Q(«$P»)) {a a' : Q(«$α»)} (exs : List VarQ) (path : Path) (act : Q(«$a» = «$a'») → List HypQ → Lean.MetaM Q(«$goal»)) : Lean.MetaM Q(«$goal»)

Given act : (a = a') → hb₁ → hb₂ → ... → hbₙ → goal where hb₁, ..., hbₙ are hypotheses obtained when unpacking existential quantifiers with variables from exs, it proves goal using Exists.elim. We use this to prove implication in the forward direction.

def ExistsAndEq.withNestedExistsIntro {P body : Q(Prop)} (exs : List VarQ) (act : Lean.MetaM Q(«$body»)) : Lean.MetaM Q(«$P»)

When P = ∃ f₁ ... fₙ, body, where exs = [f₁, ..., fₙ], this function takes act : body and proves P using Exists.intro.

Example:

exs = []: act
exs = [b]:
  P := ∃ b, body
  Exists.intro b act
exs = [b, c]:
  P := ∃ b c, body
  Exists.intro b (Exists.intro c act)
...

def ExistsAndEq.mkBeforeToAfter {u : Lean.Level} {α : Q(Sort u)} {p : Q(«$α» → Prop)} {P' : Q(Prop)} (a' : Q(«$α»)) (newBody : Q(Prop)) (fvars : List VarQ) (path : Path) : Lean.MetaM Q((∃ (a : «$α»), «$p» a) → «$P'»)

Generates a proof of ∃ a, p a → P'. We assume that fvars = [f₁, ..., fₙ] are free variables and P' = ∃ f₁ ... fₙ, newBody, and path leads to a = a' in ∃ a, p a.

The proof follows the following structure:

example {α β : Type} (f : β → α) {p : α → Prop} :
    (∃ a, p a ∧ ∃ b, a = f b) → (∃ b, p (f b) ∧ f b = f b) := by
  -- withLocalDeclQ
  intro h
  refine h.elim (fun a ha ↦ ?_)
  -- withExistsElimAlongPath: following the path we unpack all existential quantifiers.
  -- at the end `hs = [hb]`.
  have h' := ha
  replace h' := h'.right
  refine Exists.elim h' (fun b hb ↦ ?_)
  replace h' := hb
  have h_eq := h'
  clear h'
  -- go: we traverse `P` and `goal` simultaneously
  have h' := ha
  refine Exists.intro b ?_
  refine And.intro ?_ ?_
  -- outside the path goal must coincide with `h_eq ▸ h'`
  · replace h' := h'.left
    exact Eq.mp (congrArg (fun t ↦ p t) h_eq) h'
  -- inside the path:
  · replace h' := h'.right
    -- when `h'` starts with existential quantifier we replace it with next hypothesis from `hs`.
    replace h' := hb
    -- at the end the goal must be `x' = x'`.
    rfl

def ExistsAndEq.existsAndEq : Lean.Meta.Simp.Simproc

Triggers at goals of the form ∃ a, body and checks if body allows a single value a' for a. If so, replaces a with a' and removes quantifier.

It looks through nested quantifiers and conjunctions searching for a a = a' or a' = a subexpression.