The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I don't know of anything like nominal Isabelle in Coq. However, many of the ideas underlying that framework are available for free in Coq, thanks to parametricity.
As far as I understand, in general, nominal reasoning is mainly about proving equivariance. For functions, equivariance means that you can commute the function with permutations of atoms (variables in the context of nominal Isabelle).

(In the context of security, they seem to use the word atom)

More formally, equivariant (f) := for any permutation P of atoms, P (f x) is the same as f (P x). P is lifted appropriately for type constructors such as list.

In Coq, ALL closed (some axioms such as function extensionality, proof irrelevance are allowed) functions that are parametric over (T:Type) (eqdec: T->T->bool) are equivariant. eqdec is supposed to be the equality decider for T.

Intuitively, while writing such functions, if you have a t:T, you can't do anything with it except applying the equality decider.
Parametricity plugins for Coq can produce free proofs of equivariance. Here is an example:

Declare ML Module "paramcoq". (* assuming you have installed paramcoq. An 8.6 version of paramcoq with some bugfixes can be found at https://github.com/aa755/paramcoq/tree/v86FullNames *)

Definition DoWhateverYouLikeWithListVars (T:Type) (eqdec : T->T->bool) (l : list T) : list T := ...

(* Now, you invoke the parametricity plugin as follows: *)

Parametricity Recursive DoWhateverYouLikeWithListVars.

(* The above command creates the following definitions : *)

Inductive bool_R : bool -> bool -> Set :=

    bool_R_true_R : bool_R true true | bool_R_false_R : bool_R false false

Inductive

list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type)

  : list A₁ -> list A₂ -> Type :=

    list_R_nil_R : list_R A₁ A₂ A_R nil nil

  | list_R_cons_R : forall (H : A₁) (H0 : A₂),

                    A_R H H0 ->

                    forall (H1 : list A₁) (H2 : list A₂),

                    list_R A₁ A₂ A_R H1 H2 ->

                    list_R A₁ A₂ A_R (H :: H1) (H0 :: H2)

DoWhateverYouLikeWithListVars_R:

forall (T₁ T₂ : Type) (T_R : T₁ -> T₂ -> Type)

         (eqdec₁ : T₁ -> T₁ -> bool) (eqdec₂ : T₂ -> T₂ -> bool),

       (forall (H : T₁) (H0 : T₂),

        T_R H H0 ->

        forall (H1 : T₁) (H2 : T₂),

        T_R H1 H2 -> bool_R (eqdec₁ H H1) (eqdec₂ H0 H2)) ->

       forall (l₁ : list T₁) (l₂ : list T₂),

       list_R T₁ T₂ T_R l₁ l₂ ->

       list_R T₁ T₂ T_R (DoWhateverYouLikeWithListVars T₁ eqdec₁ l₁)

         (DoWhateverYouLikeWithListVars T₂ eqdec₂ l₂)

(* The body of DoWhateverYouLikeWithListVars_R depends on the body of DoWhateverYouLikeWithListVars. But, no matter what the body of DoWhateverYouLikeWithListVars is,

the type of  DoWhateverYouLikeWithListVars_R  would be exactly as shown above.

It is straightforward to derive equivariance from DoWhateverYouLikeWithListVars_R.

Let V be the type of atoms (variables in the context of nominal Isabelle). You could, for example, choose nat to represent atoms. 

Instantiate DoWhateverYouLikeWithListVars_R with T₁:= V, T₂ := V, T_R := fun v1 v2 => P v1 = v2. P is supposed to be a bijection (permutation of variables).

No matter what the body of DoWhateverYouLikeWithListVars is, the above instantiation of DoWhateverYouLikeWithListVars_R would easily imply that DoWhateverYouLikeWithListVars is equivariant.

 *)

One problem with paramcoq is that it cannot prove equivariance of undecidable relations (in general, relations that return a Prop and not a bool). 

For example, if you define some R:{T:Type} {eqdec : T->T->bool} (t1 t2: T) : Prop,

paramcoq cannot prove that forall v1 v2:V, R v1 v2 <-> R (P v1) (P v2). 

Undecidable relations such as observational equivalence show up frequently in PL metatheory.

The above problem is solved by paramcoq-iff, which is explained in the following tech report: https://arxiv.org/abs/1705.01163

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Aug 23, 2017 at 2:04 PM, Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi all,

I'm wondering if something like nominal Isabelle exists in Coq. I've found an extended abstract that discusses this, but I am yet to find follow-up work. I know there is a documented need for it, so I'm wondering if anyone further work exists, and especially if there are any tools that people use, since I know that Nominal Isabelle is very popular.

If there is no analogue, I'm curious if anyone knows whether this is fundamental to the difference in logics between Coq and Isabelle, or whether this is "just" a matter of someone building an analogous effective tool in Coq itself.

Thanks!

Talia