Parametricity

Stream: lean4

[Joachim Breitner]

Parametricity has been discussed here on-and-off (here or here) , and I read hat parametricity is false in the presence of classical.choice.

But if I have a concrete definition and check that it does not depend on that axiom (or other axioms), can I then reason by parametricity? Is every axiom-free lean definition f : (α : Type) → α → α equal to the identity?

[Geoffrey Irving]

Can’t you check if the type is Bool and do not if so? Ah, I guess that requires choice?

[Joachim Breitner]

Isn’t that precisely the thing that needs classical choice?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Joachim Breitner said:

Parametricity has been discussed here on-and-off (here or here) , and I read hat parametricity is false in the presence of classical.choice.

But if I have a concrete definition and check that it does not depend on that axiom (or other axioms), can I then reason by parametricity? Is every axiom-free lean definition f : (α : Type) → α → α equal to the identity?

One issue with this approach is that such a restricted parametricity lemma cannot be stated internally (since 'depends on this or that axiom' is not expressible in the type theory). But maybe you could have a metaprogram that generates proofs of equal-to-identity for _specific_ terms of type (α : Type) → α → α by inspecting the term (this should always succeed assuming that parametricity does hold for the axiom-free fragment of Lean, a statement that I don't know to be true or false).

[Joachim Breitner]

My thoughts keep coming back to this. Having parametricity theorems for (axiom-free) definition could be a very convenient proof tool! So I understand that parametricity does not hold internally, and could not hold externally for definitions using choice.

But for everything else, how plausible would it be to have a tactic or command that derives the “free theorem” when possible? Did anyone work on this before?

And is there prior part in other systems to check out? Superficial searching found https://github.com/coq-community/paramcoq.

[Arthur Adjedj]

I'm not certain of the usefulness of generating "free theorems" for axiom-free terms, knowing how much Quot.sound, propext and Classical.choice are propagated in Lean in practice. However, Lean could very certainly benefit from implementing Trocq's parametricity translation, and from using it to do proof-transfer IMO.

[Johan Commelin]

I'm supervising an MSc project on porting Trocq to Lean.

[Joachim Breitner]

Nice!

[Joachim Breitner]

But from skimming that reference, transfer seems to be a less powerful gadget than parametricity results.

Consider, as an application, that I have a monad were some property P holds for bind a f if it holds for a and for all f x. Now it is „obvious” that similar statements can be shown for all kinds of monad combinators, like mapM etc, and it seems that parametricity is a tool to get these statements. Is that too optimistic?

[Joachim Breitner]

@Cyril Cohen I see you are one of the authors of https://github.com/coq-community/paramcoq. What is your take here?

Also, from reading the paper Parametricity in an Impredicative Sort it seems that you had to introduce a variant of the CIC logic (in the theory, not the plugin) because of the cumulative universes. Does that mean that parametricity is actually easier in Lean than in Coq?

[Cyril Cohen]

Joachim Breitner said:

Cyril Cohen I see you are one of the authors of https://github.com/coq-community/paramcoq. What is your take here?

Also, from reading the paper Parametricity in an Impredicative Sort it seems that you had to introduce a variant of the CIC logic (in the theory, not the plugin) because of the cumulative universes. Does that mean that parametricity is actually easier in Lean than in Coq?

I merely ported some pieces of code once, but I'm a co-author of Trocq.
Trocq is a generalisation of paramcoq, you get way more powerful results out of it.

[Cyril Cohen]

Also, I tried to write a parametricity plugin for Lean3, and go stuck because of missing bits of API, I guess this wouldn't happen today in Lean4

[Cyril Cohen]

Arthur Adjedj said:

I'm not certain of the usefulness of generating "free theorems" for axiom-free terms, knowing how much Quot.sound, propext and Classical.choice are propagated in Lean in practice. However, Lean could very certainly benefit from implementing Trocq's parametricity translation, and from using it to do proof-transfer IMO.

Quot.sound and propext should behave well, not choice indeed, but problems arise only when statements rely on them.

[Cyril Cohen]

Also, for application of parametricity techniques to get free theorems, you can take a look at https://inria.hal.science/hal-01113453/document, there https://inria.hal.science/hal-00734505/document with some Coq code here https://github.com/coq-community/coqeal/.

There is another kind of application in https://pastel.hal.science/pastel-00649586v1/document Section 3.4.

[Joachim Breitner]

Thanks for the context, and in particular pointing out that Trcoq is more general. In that case I'll just wait for Johann's student to port it to lean and come back here then :-)