The Coq mailing list

[Caitlin McGregor <caitlin.mcgregor AT anu.edu.au>]

Hi there,

I'm fairly new to Coq and I have been working with a fragment of first order logic as my object logic (see below for definitions). I'd like to be able to rename my FO variables so that no two quantifiers bind the same variable. Does anyone know if this has been done before and if so where I could find the code?

Here is a snippet of my code:

(* Countably many unary predicates P *)
Inductive predicate : Type :=
  Pred (n:nat) : predicate.

(* Countably many FO variables x *)
Inductive FOvariable : Type :=
  Var (n:nat) : FOvariable.

(* Definition of first order formula *)
Inductive FOF:=
    predFO : predicate -> FOvariable -> FOF (* unary predicates P x *)
  | relatFO : FOvariable -> FOvariable -> FOF (* single binary relation R x y *)
  | eqFO : FOvariable -> FOvariable -> FOF (* equality x = y *)
  | allFO : FOvariable -> FOF -> FOF (* universal quantifier *)
  | exFO : FOvariable -> FOF -> FOF (* existential quantifier *)
  | negFO : FOF -> FOF
  | conjFO : FOF -> FOF -> FOF
  | disjFO : FOF -> FOF -> FOF
  | implFO : FOF -> FOF -> FOF.

Any help you could provide would be greatly appreciated.

Regards,
Caitlin