Questions tagged [substitution]

Questions regarding syntactic substitutions should be tagged with this.

Filter by
Sorted by
Tagged with
2 votes
1 answer

In Lean 4 how to substitute equals in an expression with other variables?

I can use 'subst' to prove that if a=b and a is positive then b is positive: example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2 How do I ...
Lewis Baxter's user avatar
4 votes
1 answer

How to encode and manipulate (parallel) substitutions?

While attempting to formalize some basic properties of STLC I fell into a very deep rabbit hole revolving around substitutions. Apparently there are a few different ways to go about it, including ...
aradarbel10's user avatar
5 votes
0 answers

An algorithm for the substitution of formulas for predicates in first order logic

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
user695931's user avatar
4 votes
0 answers

Are there any proof assistants that can not be derived from substitution?

Are there any type of proof systems that can not be implemented with substitution at the core? In essence if I want to implement a base library for building up various proof assistants do I only need ...
Guy Coder's user avatar
  • 2,836
17 votes
2 answers

How to deal with Binders?

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
Wno-all's user avatar
  • 1,098