search

coq-community / autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
https://www.ps.uni-saarland.de/autosubst
MIT License
52 stars 14 forks source link

A few extra lemmas. #5

Closed fpottier closed 2 years ago

fpottier commented 7 years ago

Hello,

I am experimenting with Autosubst, for use in teaching the metatheory of programming languages. Congratulations! My initial experiments are encouraging: life with de Bruijn indices is becoming tolerable.

I find that there are some situations where the tactics "asimpl" and "autosubst" are not sufficient and one has to explicitly establish auxiliary lemmas and use them as rewriting rules. Would you be interested in adding these lemmas to the library, provided they are of sufficient general interest? (Maybe I should ask also, is the library still maintained?)

For now, I am submitting a couple patches related to associativity, but I have more, if you are interested. (I could also show you the small project where I am using Autosubst.)

Best regards, François Pottier.

RalfJung commented 2 years ago

oops looks like when we took over maintenance of this, we entirely missed this PR. Sorry for that!

(Maybe I should ask also, is the library still maintained?)

I guess you got your answer, given it took 5 years for a reply to appear here... ;) Basically not, though I am we are keeping it on "life support" since some Iris case studies use it.

I would not be opposed to adding some lemmas, but I have not properly used this library myself, so I can't really tell how generally useful they are. Also I would be opposed to changing any of the existing lemmas; let's avoid breaking changes if at all possible. So, compA should remain unchanged.

co-dan commented 2 years ago

Indeed, that's a big 'oops'.. that being said, I recall proving something like upn_upn, so I wouldn't mind those lemmas. Except, as Ralf said, backwards compatibility is key

fpottier commented 2 years ago

Hi! I won't have time to work on this in the foreseeable future, so I think we can close this PR (and I am closing it).

RalfJung commented 2 years ago

That's fair. Sorry again for the huge latency!