feat: Church–Rosser theorem (Q1308502) for ULC (de Bruijn)#475
feat: Church–Rosser theorem (Q1308502) for ULC (de Bruijn)#475zayn7lie wants to merge 12 commits intoleanprover:mainfrom
Conversation
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Hi, thanks for your interest in contributing to CSLib! We do have Church-Rosser for locally nameless binding, but I think we are interested in having the more common de Bruijn indices representation as well.
I see there is a disclosure of AI usage, but this looks like its been mostly cleaned up pretty well, so thank you.
Below are some initial reviews about making this fit into CSLib conventions.
There was a problem hiding this comment.
This should go with the other lambda calculus modules under Cslib/Languages/LambdaCalculus and follow their structure of a directory for each type system. I would call this binding Unscoped to distinguish from well-scoped de Bruijn indices. So all togther, everything here would go under Cslib.Languages.LambdaCalculus.Unscoped.Untyped.*
There was a problem hiding this comment.
There was a problem hiding this comment.
I think all of this is subsumed by Cslib.Foundations.Data.Relation.
There was a problem hiding this comment.
There was a problem hiding this comment.
Maybe I was unclear here. I don't think this file should exist at all. All of this, with maybe the exception of rtc_eq_of_sandwich, is already in Cslib.Foundations.Data.Relation.
There was a problem hiding this comment.
Thanks for clarification:
commits/28e7a79deee335a4afc846052de594f970672010
commits/d38b50169dcbee2c72574911b79a68c1d6402b3a
| infixl:77 "·" => Term.app | ||
|
|
||
| /-- `incre i l t` increments `i` for all free vars `≥ l`. -/ | ||
| @[simp, expose] public def incre (i : Nat) (l : Nat) : Term → Term |
There was a problem hiding this comment.
It seems like you should just use @[expose] public section for these modules.
There was a problem hiding this comment.
| | app t u => app (subst j s t) (subst j s u) | ||
|
|
||
| /-- `decre c t` decrements free vars `> c` by 1. -/ | ||
| @[simp, expose] public def decre (l : Nat) : Term → Term |
There was a problem hiding this comment.
For the sake of consistency, I would also generalize this to an arbitrary decrement.
There was a problem hiding this comment.
| | app t₁ t₂ ih₁ ih₂ => simp_all | ||
|
|
||
| /-- Communitivity of incre. -/ | ||
| public theorem incre_comm {i j k l t} : |
There was a problem hiding this comment.
I think we can clean up some of the arithmetic in theorems like this, but I'll wait until we have more high-level changes done first to give specific suggestions.
| | app t u => app (decre l t) (decre l u) | ||
|
|
||
| /-- Substitute into the body of a lambda: `(λ.t) s` -/ | ||
| @[simp, expose] public def sub (t : Term) (n : Nat) (s : Term) := decre n (subst n (incre 1 n s) t) |
There was a problem hiding this comment.
See Cslib.Foundations.Syntax.HasSubstitution for the notation typeclass we use for substitution.
There was a problem hiding this comment.
| | appL {t t' u} : Beta t t' → Beta (t·u) (t'·u) | ||
| | appR {t u u'} : Beta u u' → Beta (t·u) (t·u') | ||
| | red (t' s : Term) : Beta ((λ.t')·s) (t'.sub 0 s) | ||
| public abbrev BetaStar := Relation.ReflTransGen Beta |
There was a problem hiding this comment.
We use the attribute reduction_sys for generating notations for reductions and the multi-step closure.
There was a problem hiding this comment.
|
|
||
| namespace BetaStar | ||
|
|
||
| public theorem refl (t : Term) : BetaStar t t := |
There was a problem hiding this comment.
As a general style rule, please out a single space between theorems.
There was a problem hiding this comment.
…lation`, and add `rtc_eq_of_sandwich`
…lation`, and add `rtc_eq_of_sandwich`
…multi-step closure
2 participants
Main contributions
Par) and its basic properties.Diamond,Confluent) for binary relations.The development follows the classical proof strategy:
parallel reduction -> diamond -> confluence -> Church–Rosser.Design choices
(
Diamond,Confluent) to keep the proof modular.Use of AI