Benedict Smit (Aug 03 2024 at 07:26): Benedict Smit (Aug 03 2024 at 07:26):I am trying to analyze constructors and traverse the constr of its type for this by matching on its kind_of_term. Now I need to know if two locally bound variables are the same but given the following type
Inductive Test : (nat->Type) -> nat -> Type :=
| testI : forall (f:(nat->Type)) (n:nat), f n -> forall f (x:nat), Test f n.
I have the problem, that f has the same index in the two places and also the same name and type but are different. Is there a easy way in the library to compare this? I thought I could use Contexts, but if I understand it correct those also just store the name relevance and type so wouldn't be able to differentiate them.
Or is the way I traverse the constr wrong? Because if I match against a Prod variant and then recursively go deeper into the term I loose some information about where and how the local variables are bound.
Janno (Aug 03 2024 at 08:19):You probably want one of the ..with_binder functions in https://coq.inria.fr/doc/master/api/coq-core/EConstr/index.html#val-map_with_binders. If you look for uses in Coq itself you should be able to find good examples that track the binder levels correctly.
Janno (Aug 03 2024 at 08:20):But I guess it depends a lot on what exactly you are doing. Your description sounds like you are somehow collecting subterms and end up with similar looking terms taken from different binding levels. In that case you might want to lift the terms you collect by the current level (which you would track with one of the functions I linked)
Benedict Smit (Aug 03 2024 at 09:28):Thank you very much, I will look into those functions.
Yes exactly I need subterms and want to look where else those subterms appear. I'm not sure if I understand your suggestion correct. Do you mean subtracting the current depth from the index, so for the first f I would get Rel(0) instead of Rel(2) and for the second f I would get Rel(-2) instead of Rel(4) so they are different now, and the n would be Rel(-1) in both cases so they are equal like they should be?
I think I could use a local context to achieve a similar thing and keep track of the name and the type at the same time. Isn't it the case that (length context) - de Brujin index gives the same number for Rels introduced by the same binder?
Janno (Aug 05 2024 at 08:41):I am not sure I follow these computations. I am not advocating for negative de bruijn indices. I think they should generally only grow, not shrink, in what I suggest. I am sure a local context could also work. In the end the best choice probably depends on what your notion of (sub)term equality is. It seems you do not want to confuse the two f binders in your original example so it seems much simpler to lift the indices in a way that makes them easily distinguishable.
Last updated: Oct 13 2024 at 01:02 UTC