The Coq mailing list

[Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>]

Hi Caitlin, 

This is a commonly arising issue. Here’s a snippet that I believe does what you want (although rather inefficiently):

Definition inc (x : FOvariable) : FOvariable :=

  match x with

    | Var x => Var (x+1)

  end.

Definition extend (f : FOvariable -> FOvariable) (x y : FOvariable)

: FOvariable -> FOvariable :=

  fun z =>

    match z with

      | Var n1 =>

        match x with

          | Var n2 => if Nat.eqb n1 n2 then y else f z

        end

    end.

Fixpoint renameFOF (fof : FOF) (next : FOvariable) (subst : FOvariable -> FOvariable)

: FOF * FOvariable:=

  match fof with

    | predFO P x =>

      (predFO P (subst x), next)

    | relatFO x y =>

      (relatFO (subst x) (subst y), next)

    | eqFO x y =>

      (eqFO (subst x) (subst y), next)

    | allFO x fof1 =>

      let (fof1', next') := renameFOF fof1 (inc next) (extend subst x next) in

      (allFO next fof1', next')

    | exFO x fof1 =>

      let (fof1', next') := renameFOF fof1 (inc next) (extend subst x next) in

      (exFO next fof1', next')

    | negFO fof1 =>

      let (fof1', next') := renameFOF fof1 next subst in

      (negFO fof1', next')

    | conjFO fof1 fof2 =>

      let (fof1', next') := renameFOF fof1 next subst in

      let (fof2', next'') := renameFOF fof2 next' subst in

      (conjFO fof1' fof2', next'')

    | disjFO fof1 fof2 =>

      let (fof1', next') := renameFOF fof1 next subst in

      let (fof2', next'') := renameFOF fof2 next' subst in

      (disjFO fof1' fof2', next'')

    | implFO fof1 fof2 =>

      let (fof1', next') := renameFOF fof1 next subst in

      let (fof2', next'') := renameFOF fof2 next' subst in

      (implFO fof1' fof2', next'')

  end.

What remains to do in order to perform the renaming is to call the renameFOF function with the successor of the maximum free identifier of the formula (to avoid capturing) and the identity substitution. Note that you can avoid the renaming altogether by adopting a different binder representation, such as De Bruijn. 

Best,

Zoe

On Nov 15, 2016, at 6:39 PM, Caitlin McGregor <caitlin.mcgregor AT anu.edu.au> wrote:

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