# 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`.

source
inductive ExistsAndEq.GoTo :
Type

Type for storing the chosen branch at `And` nodes.

- left : GoTo
- right : GoTo

Instances For

source
instance ExistsAndEq.instBEqGoTo :
BEq GoTo
Equations

- ExistsAndEq.instBEqGoTo = { beq := ExistsAndEq.instBEqGoTo.beq }

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

- ExistsAndEq.instBEqGoTo.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source
instance ExistsAndEq.instInhabitedGoTo :
Inhabited GoTo
Equations

- ExistsAndEq.instInhabitedGoTo = { default := ExistsAndEq.instInhabitedGoTo.default }

source
def ExistsAndEq.instInhabitedGoTo.default :
GoTo
Equations

- ExistsAndEq.instInhabitedGoTo.default = ExistsAndEq.GoTo.left

Instances For

source
@[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.

Equations

- ExistsAndEq.Path = List ExistsAndEq.GoTo

Instances For

source
@[reducible, inline]
abbrev ExistsAndEq.VarQ :
Type

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

Equations

- ExistsAndEq.VarQ = ((u : Lean.Level) × (α : Q(Sort u)) × Q(«$α»))

Instances For

source
instance ExistsAndEq.instInhabitedVarQ :
Inhabited VarQ
Equations

- ExistsAndEq.instInhabitedVarQ = { default := ⟨default, ⟨default, default⟩⟩ }

source
@[reducible, inline]
abbrev ExistsAndEq.HypQ :
Type

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

Equations

- ExistsAndEq.HypQ = ((P : Q(Prop)) × Q(«$P»))

Instances For

source
instance ExistsAndEq.instInhabitedHypQ :
Inhabited HypQ
Equations

- ExistsAndEq.instInhabitedHypQ = { default := ⟨default, default⟩ }

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

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

Equations

- One or more equations did not get rendered due to their size.
- ExistsAndEq.mkNestedExists [] body = pure body

Instances For

source
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.

source
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`.

Equations

- ExistsAndEq.findEq a P path = ExistsAndEq.findEq.go a P path

Instances For

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

Recursive part of `findEq`.

source
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)
      )
    ...

Instances For

source
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 concide 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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def ExistsAndEq.mkAfterToBefore.go {goal P : Q(Prop)} (h : Q(«$P»)) (exs : List VarQ) (path : Path) :
Lean.MetaM Q(«$goal»)

Traverses `P` and `goal` simultaneously, proving `goal`.

source
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`.

source
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.

Equations

- ExistsAndEq.withExistsElimAlongPath h exs path act = ExistsAndEq.withExistsElimAlongPathImp h exs path [] act

Instances For

source
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)
    ...

Instances For

source
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 concide 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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Traverses `P` and `goal` simultaneously, proving `goal`.

source
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 conjuctions searching for a `a = a'` or `a' = a` subexpression.

Equations

- One or more equations did not get rendered due to their size.

Instances For