Stream: Coq users

Topic: Preserving binder names while manipulating functions


view this post on Zulip Mathis Bouverot-Dupuis (May 07 2024 at 17:40):

Hi all,

I have a lambda abstraction f (fun my_name => _). I would like to compose this with a function, say g, but have the resulting lambda abstraction use the same binder as f i.e. have something like fun my_name => g _. This is not the case if I define comp f g := fun x => g (f x). Is there a way to preserve the binder of f ?

I am looking for a solution that doesn't involve directly manipulating the syntax of the terms in Ocaml or Ltac, as I still want to be able to prove properties about the composition.

view this post on Zulip Gaëtan Gilbert (May 07 2024 at 18:17):

Is there a way to preserve the binder of f ?

no

view this post on Zulip Ali Caglayan (May 08 2024 at 18:12):

Why do you need the binder to stay the same however?

view this post on Zulip Mathis Bouverot-Dupuis (May 08 2024 at 22:11):

Ali Caglayan said:

Why do you need the binder to stay the same however?

I'm trying to implement a Lean tactic called push_neg : https://leanprover-community.github.io/mathlib4_docs//Mathlib/Tactic/PushNeg.html

This involves manipulating propositions while preserving the names of bound variables.

view this post on Zulip Thomas Lamiaux (May 08 2024 at 23:14):

Can't this be implemented using Ltac and rewrites ? Rewrites shouldn't change the name of the binders ?

view this post on Zulip Mathis Bouverot-Dupuis (May 09 2024 at 14:43):

Thomas Lamiaux said:

Can't this be implemented using Ltac and rewrites ? Rewrites shouldn't change the name of the binders ?

Sadly this won't work. For instance let's say I have a constant P : Prop -> Prop, and I have a hypothesis H : P (~ forall x, x = 0). Calling push_neg in H should not do anything, which seems tricky to do with only Ltac and rewrites. The issue is that rewrites are not sensitive to the context of where we rewrite.

view this post on Zulip Ali Caglayan (May 09 2024 at 15:51):

Here is the issue for it: https://github.com/coq/coq/issues/10114

view this post on Zulip Ali Caglayan (May 09 2024 at 15:53):

That issue however is specifically about not having this "feature" in ltac2 but perhaps ltac has a way of doing this.


Last updated: Jun 13 2024 at 19:02 UTC