Conversation

Behold the power of the Ultimate Decision Procedure for substitution lemmas #Autosubst (ps.uni-saarland.de/autosubst/)! And it's just a dozen rewrite rules! Yes, the syntax is a bit scary. Proving these lemmas by hand is just more so!

Beta-reduction and substitution commute, with the help of Autosubst. Stated with either alphabetic or symbolic operators (syntax blizzard mode, I admit).

read image description

ALT

The convergent rewriting system of the σ -calculus

read image description

ALT

Brendan Zabarauskas

@brendanzab

Replying to

@Blaisorblade

Oooh, will have to try it out! This looks like one of the nice metatheory lib thingos I've seen for Coq! Also seems like there's a Lean port in the works! ps.uni-saarland.de/~mameche/bache

6:37 AM · Aug 21, 2018Twitter Web Client

Replying to

and

Any idea why a pure debruijn approach was used, as opposed to something like locally nameless? (Just curious)

Paolo G. Giarrusso

@Blaisorblade

Aug 21, 2018

They don’t quite say, but I’m not sure LN is warranted at this point (other than complexity with multi-sorted syntaxes). I also don’t kmow if sigma-calculus still works for LN (you need to adapt it, but is the result a confluent, terminating and complete rewrite system?)

Show replies