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.

• andLeft : GoTo
• andRight : GoTo
• existsType : GoTo
• existsBody : GoTo

@[instance_reducible]

instance ExistsAndEq.instBEqGoTo : BEq GoTo

Equations

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

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

Equations

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

@[instance_reducible]

instance ExistsAndEq.instInhabitedGoTo : Inhabited GoTo

Equations

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

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

@[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(«$α»))

@[instance_reducible]

instance ExistsAndEq.instInhabitedVarQ : Inhabited VarQ

Equations

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

@[reducible, inline]

abbrev ExistsAndEq.HypQ : Type

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

Equations

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

@[instance_reducible]

instance ExistsAndEq.instInhabitedHypQ : Inhabited HypQ

Equations

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

def ExistsAndEq.eqDetermines (a x y : Lean.Expr) : Bool

Checks whether the equation with sides x and y determines the free variable a as y: x is a itself, and y doesn't mention a (in a = f a, for example, it does). The callers try both orientations.

Equations

• ExistsAndEq.eqDetermines a x y = (a == x && !y.containsFVar a.fvarId!)

partial def ExistsAndEq.findEqPath {u : Lean.Level} {α : Q(Sort u)} (a : Q(«$α»)) (P : Q(Prop)) : OptionT Lean.MetaM 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.

Equations

• ExistsAndEq.findEq a P path = ExistsAndEq.findEq.go✝ a P path

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

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

Equations

• ExistsAndEq.mkNestedExists [] body = pure body
• ExistsAndEq.mkNestedExists (⟨fst, ⟨β, b⟩⟩ :: tl) body = do let res ← ExistsAndEq.mkNestedExists tl body let p ← Lean.Meta.mkLambdaFVars #[b] res pure q(Exists «$p»)

def ExistsAndEq.Path.forResult (path : Path) : Path

The path to the equation in the result formula: the quantifiers entered along path are moved to the front, so their existsBody steps come first, followed by the And steps in their original order.

Equations

• path.forResult = match List.partition (fun (x : ExistsAndEq.GoTo) => x == ExistsAndEq.GoTo.existsBody) path with | (quantifiers, conjunctions) => quantifiers ++ conjunctions

partial def ExistsAndEq.destruct {P goal : Q(Prop)} (h : Q(«$P»)) (exs : List VarQ) (path : Path) (acc : List HypQ) (k : List HypQ → HypQ → Lean.MetaM Q(«$goal»)) : Lean.MetaM Q(«$goal»)

Destructs h : P following path, as the chain of refine h.elim fun … ↦ ?_ in the docstring of mkBeforeToAfter does: at an existsBody step the quantifier is unpacked with Exists.elim, using the next variable of exs as the bound variable; at an andLeft/andRight step the conjunction is split with And.elim, and the part outside the path becomes a leaf. The continuation k receives the leaves (in path order, after those in acc) and the hypothesis at the end of the path, i.e. the equation. All of them are local hypotheses.

partial def ExistsAndEq.construct {goal : Q(Prop)} (exs : List VarQ) (path : Path) (leaves : List HypQ) : Lean.MetaM Q(«$goal»)

Constructs a proof of goal following path, as the chain of refine Exists.intro … ?_ and refine And.intro … ?_ in the docstring of mkBeforeToAfter does: at an existsBody step the next variable of exs is the witness; at an andLeft/andRight step the part outside the path is proved by the next leaf; the equation at the end of the path is closed by rfl.

def ExistsAndEq.mkBeforeToAfter {u : Lean.Level} {α : Q(Sort u)} {p : Q(«$α» → Prop)} {P' : 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 (f : β → α) {P Q : β → Prop} :
    (∃ x b, P b ∧ (∃ c, f c = x ∧ Q c) ∧ Q b) → ∃ b c, P b ∧ (f c = f c ∧ Q c) ∧ Q b := by
  -- path : existsBody, andRight, andLeft, existsBody, andLeft
  intro ⟨x, h₁⟩
  -- destruct the input following the path:
  -- obtain ⟨e1, a1, ⟨e2, h_eq, a3⟩, a2⟩ := h₁
  refine
    h₁.elim fun e1 h₂ ↦           -- existsBody
    h₂.elim fun a1 h₃ ↦           -- andRight
    h₃.elim fun h₄ a2 ↦           -- andLeft
    h₄.elim fun e2 h₅ ↦           -- existsBody
    h₅.elim fun h_eq a3 ↦ ?_      -- andLeft
  -- subst the equation (`substCore`)
  subst h_eq
  -- construct the output following the path of the result (with all existsBody moved left):
  -- existsBody, existsBody, andRight, andLeft, andLeft
  -- exact ⟨e1, e2, a1, ⟨rfl, a3⟩, a2⟩
  refine Exists.intro e1 ?_       -- existsBody
  refine Exists.intro e2 ?_       -- existsBody
  refine And.intro a1 ?_          -- andRight
  refine And.intro ?_ a2          -- andLeft
  refine And.intro ?_ a3          -- andLeft
  exact rfl

Equations

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

def ExistsAndEq.mkAfterToBefore {u : Lean.Level} {α : Q(Sort u)} {p : Q(«$α» → Prop)} {P' : Q(Prop)} (a' : Q(«$α»)) (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 (f : β → α) {P Q : β → Prop} :
    (∃ b c, P b ∧ (f c = f c ∧ Q c) ∧ Q b) → ∃ x b, P b ∧ (∃ c, f c = x ∧ Q c) ∧ Q b := by
  intro h₁
  -- destruct the input following the path of the result (with all existsBody moved left):
  -- existsBody, existsBody, andRight, andLeft, andLeft
  -- obtain ⟨e1, e2, a1, ⟨_, a3⟩, a2⟩ := h₁
  refine
    h₁.elim fun e1 h₂ ↦           -- existsBody
    h₂.elim fun e2 h₃ ↦           -- existsBody
    h₃.elim fun a1 h₄ ↦           -- andRight
    h₄.elim fun h₅ a2 ↦           -- andLeft
    h₅.elim fun _ a3 ↦ ?_         -- andLeft
  -- construct the output following the path: existsBody, andRight, andLeft, existsBody, andLeft
  -- exact ⟨f e2, e1, a1, ⟨e2, rfl, a3⟩, a2⟩
  refine Exists.intro (f e2) ?_   -- `a'`
  refine Exists.intro e1 ?_       -- existsBody
  refine And.intro a1 ?_          -- andRight
  refine And.intro ?_ a2          -- andLeft
  refine Exists.intro e2 ?_       -- existsBody
  refine And.intro ?_ a3          -- andLeft
  exact rfl

Equations

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

def ExistsAndEq.withAbstractMVars (e : Lean.Expr) (k : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Step) : Lean.MetaM Lean.Meta.Simp.Step

Runs k on e with the metavariables occurring in e replaced by local variables, and substitutes the metavariables back into the resulting Simp.Step. In some cases (e.g. under aesop) the goal contains metavariables, and this is needed to handle them properly: the proof built by substCore can only be instantiated when the goal contains none.

The abstraction is done by abstractMVars, so that metavariables occurring in the types of other metavariables (as in ?f : α → ?β) are handled consistently.

TODO: this is a general simproc infrastructure, should we moved somewhere else?

Equations

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

def ExistsAndEq.existsAndEqCore (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Step

The implementation of existsAndEq, for an expression without metavariables.

Equations

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

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.

Equations

• existsAndEq e = liftM (ExistsAndEq.withAbstractMVars e ExistsAndEq.existsAndEqCore)