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

This module implements the existsAndEq simproc that triggers on goals of the form ∃ a, body and checks whether body has the form ... ∧ a = a' ∧ ... or ... ∧ a' = a ∧ ... for some a' that is independent of a. If so, it replaces all occurrences of a with a' and removes the quantifier.

def existsAndEq.findImpEqProof (p : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

For an expression p of the form fun (x : α) ↦ (body : Prop), checks whether body implies x = a for some a, and constructs a proof of (∃ x, p x) = p a using exists_of_imp_eq.

Equations

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

partial def existsAndEq.findImpEqProof.go (x h : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Traverses the expression h, branching at each And, to find a proof of x = a for some a.

def existsAndEq : Lean.Meta.Simp.Simproc

Triggers on goals of the form ∃ a, body and checks whether body has the form ... ∧ a = a' ∧ ... or ... ∧ a' = a ∧ ... for some a' that is independent of a. If so, it replaces all occurrences of a with a' and removes the quantifier.

Equations

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