Term rewriting for deduction system

Stream: new members

[Ashley Blacquiere]

Hi all - I've been lurking here for a little while, but haven't yet introduced myself: I'm a comp sci MSc student at the University of Victoria and I've spent some of the summer working on learning Lean via TPIL and other resources with the aim of using it as tool for a project in formal verification and cryptography. At present, my supervisor and I are thinking of perhaps trying to implement a term rewriting tactic for deduction systems (i.e. within a specific equational theory) with the eventual aim of supporting term rewriting for abelian groups with homomorphism. This has some application in intruder detection in cryptography - though that's all something new to me, so I'm not too familiar with all the ins and outs at the moment.

Lately I've been working through some of the VU Logical Verification course material, and I've found some of the other papers from the Lean Forward group's publication to be quite helpful. I'm still figuring out how to navigate mathlib though, and I'm trying to get a sense of whether or not some aspects of term rewriting in the abelian group sense might already be complete...? I'm not sure that our eventual goal would be to contribute to mathlib, though we're definitely open to that, if we end up producing something of value.

Does anyone have any suggestions or direction I might be interested in?

[Johan Commelin]

@Ashley Blacquiere Welcome! Can you explain a bit more what "term rewriting for abelian groups" means? (I'm a mathematician, so I know what abelian group means, but I don't know what term rewriting means in that context.

Would this be a version of rw that does rewrites modulo associativity and commutativity? And that automatically collapses a * a¯¹ to 1?

[Ashley Blacquiere]

Thanks, @Johan Commelin ! In answer to your question: Yes, this would be something like a version of rw, or perhaps ring_exp, that reduces terms to a normal form, but in addition to associativity and commutativity also rewrites based on an equational theory stemming from a cryptographic protocol (i.e. the equational theory would include rules for things like message encoding / decoding, among others). This is motivated by the intruder deduction problem, and specifically equational theories that include associativity and commutativity (see for example Intruder deduction problem for locally stable theories with normal forms and inverses.

Our current thought is to attempt to implement the necessary term rewriting rules in Lean as a tactic. I'm assuming there is already some existing term rewriting work that we can extend (i.e. similar to @Anne Baanen's ring_exp paper extending ring), but I'm not sure if that would be an extension of what rw does, or something similar to simp - though much more constrained - or something else entirely. Or maybe I'd have to start from scratch. I've spent some time this summer learning about proof technique in Lean, but I'm just getting into meta-programming now, so I'm not yet really sure what I need, or precisely what I'm looking for. It's all pretty overwhelming, but I'm slowly narrowing down my focus and improving my understanding. That said, if anyone has any thoughts that might help direct my efforts, I'm all ears. :)

[Patrick Massot]

Do you know about https://leanprover-community.github.io/mathlib_docs/tactics.html#abel?

[Ashley Blacquiere]

Thanks for reminding me! I only recently saw abel - I hadn't come across it in any of the texts / tutorials, I don't think, so I haven't really experimented with it and wasn't top of mind. Yes, it might be more on the lines of what I'm looking for. Certainly it seems to be a good starting point.