# Decidable variable equality in Coq

**URL:** <https://discourse.rocq-prover.org/t/decidable-variable-equality-in-coq/323>\
**Category:** Using Rocq\
**Created:** [June 8, 2019, 9:56am UTC](https://discourse.rocq-prover.org/t/decidable-variable-equality-in-coq/323 "2019-06-08T09:56:44Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![uma](https://avatars.discourse-cdn.com/v4/letter/u/ba9def/32.png) [@uma](https://discourse.rocq-prover.org/u/uma)\
**Post date:** [June 8, 2019, 9:56am UTC](https://discourse.rocq-prover.org/t/decidable-variable-equality-in-coq/323/1 "2019-06-08T09:56:44Z")

</div>

For some `fun a => ...` there’s an inductive structure with constructors that use `a` as their parameter. How can these constructors be found? Decidable equality on the type of `a` would work, but what if the type of `a` is parametric? Does it even matter what type `a` is? For all types `A` and all `a b : A`, if `a` and `b` are syntactically the same variable, then `a = b`. Is it possible to express this in Coq? How?

---

<div class="post-metadata">

**Author:** ![mattam82](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mattam82/32/11_2.png) [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Post date:** [June 10, 2019, 8:50am UTC](https://discourse.rocq-prover.org/t/decidable-variable-equality-in-coq/323/2 "2019-06-10T08:50:44Z")

</div>

I’m not sure I understand your question fully, but you might be mixing two things. One is expressing equality as a proposition `a = b` which is indeed reflexive so you have `a = a` for any term ˋa ˋ, the other is deciding equality for a given type, i.e. deciding if `a = b + a <> b`, which depends on the type (some types, e.g. universes and most function types, don’t have decidable equality). Another way to say this is that one cannot construct a parametrically polymorphic decider of equality in the theory (nor in any sufficiently expressive programming language I believe).

---

<div class="post-metadata">

**Author:** ![uma](https://avatars.discourse-cdn.com/v4/letter/u/ba9def/32.png) [@uma](https://discourse.rocq-prover.org/u/uma)\
**Post date:** [June 10, 2019, 5:20pm UTC](https://discourse.rocq-prover.org/t/decidable-variable-equality-in-coq/323/3 "2019-06-10T17:20:31Z")

</div>

Hey, thanks for your answer! I did a very poor job at explaining myself. I think it might be easier for me if I used an example:

```
Section Meh.
  Variable T : Type.
                                    
  Inductive Base : Type :=
  | C : T → Base
  .

  Inductive Tree : Type := 
  | Foo : (Base → Tree) → Tree
  | Bar : Base → Tree
  | Baz : Tree → Tree → Tree
  .
End Meh.

Arguments Foo [T].
Arguments Bar [T].
Arguments Baz [T].

Check fun T => Foo (fun a => Foo (fun b => Baz (Bar a) (Bar b))).

```

In this last `Tree T`, `a` and `b` are values of type `Base T`. Is it possible to know where `a` and `b` “go” without requiring decidable equality on the parametric type `T`? My thoughts are that because `a` and `b` are syntactically equal to their variable binding, there might be a way, probably in the metalanguage, to track their usage.

Sorry for the confusion!

---

<div class="post-metadata">

**Author:** ![mattam82](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mattam82/32/11_2.png) [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Post date:** [June 11, 2019, 1:10am UTC](https://discourse.rocq-prover.org/t/decidable-variable-equality-in-coq/323/4 "2019-06-11T01:10:46Z")

</div>

I see, indeed `a` and `b` refer to different bindings so they can be distinguished at the meta level, using term inspection facilities from Ltac for example. However you cannot inspect terms like this in Coq without a decidable equality test, which can’t even be defined here as you have a non-finite function type `Base T -> Tree T`: no program can decide if two functions of this type are equal because that would require infinite time.