Decidable variable equality in Coq

Using Coq
1

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?

2

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).

3

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!

4

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.