Search code examples
coqcoercionformal-verification

Coq difficulties in defining constructors using coerced types

Definitions

I'm working on formalizing a typed lambda calculus in Coq, and to keep the notation manageable I've come to rely a lot on coercions. However, I've been running into some difficulties which seem odd.

Right now I'm trying to work with the following types:

  • type: A descriptor of an allowable type in the language (like function, Unit, etc...)
  • var: A variable type, defined as nat
  • VarSets: set of vars
  • Judgement: a var/my_type pair
  • ty_ctx: Lists of judgements.
  • ctx_join: Pairs of ty_ctx's describing disjoint sets of variables

The actual definitions are all given below, except for ctx_join which is given in the next block

(* Imports *)
Require Import lang_spec.
From Coq Require Import MSets.
Require Import List.
Import ListNotations.

Module VarSet := Make(Nat_as_OT).

Inductive Judgement : Type :=
| judge (v : var) (t : type)
.

Definition ty_ctx := (list Judgement).

Definition disj_vars (s1 s2 : VarSet.t) := VarSet.Empty (VarSet.inter s1 s2).

Often I'd like to make statements like "this var does not appear in the set of vars bound by ty_ctx", and to that end I've set up a bunch of coercions between these types below.


(* Functions to convert between the different types listed above *)

Fixpoint var_to_varset (v : var) : VarSet.t :=
  VarSet.singleton v.
Coercion var_to_varset : var >-> VarSet.t.

Fixpoint bound_variables (g : ty_ctx) : VarSet.t :=
  match g with
  | nil => VarSet.empty
  | cons (judge v _) g' =>VarSet.union (VarSet.singleton v) (bound_variables g')
  end.
Coercion bound_variables : ty_ctx >-> VarSet.t.

Inductive ctx_join :=
| join_single (g : ty_ctx)
| join_double (g1 g2 : ty_ctx)
              (disjoint_proof : disj_vars g1 g2)
.

Fixpoint coerce_ctx_join (dj : ctx_join) : ty_ctx :=
  match dj with
  | join_single g => g
  | join_double g1 g2 _ => g1 ++ g2
  end.
Coercion coerce_ctx_join : ctx_join >-> ty_ctx.

Fixpoint coerce_judgement_to_ty_ctx (j : Judgement) : ty_ctx :=
  cons j nil.
Coercion coerce_judgement_to_ty_ctx : Judgement >-> ty_ctx.

You'll notice that the definition of ctx_join relies on coercing its arguments from ty_ctx to VarSet.

I've drawn up the conversion hierarchy just to make things clear enter image description here

The Problem

I'd like to define an inductive type with the following constructor

Inductive expr_has_type : ty_ctx -> nat -> type -> Prop :=
(* General Expressions *)
| ty_var (g : ty_ctx) (x : var) (t : type) (xfree : disj_vars x g)
  : expr_has_type (join_double (judge x t) g xfree) x t
.

The problem is that when I do, I get the following error: 

Error:
In environment
expr_has_type : ty_ctx -> nat -> type -> Prop
g : ty_ctx
x : var
t : type
xfree : disj_vars x g
The term "xfree" has type "disj_vars x g" while it is expected to have type
 "disj_vars (judge x t) g" (cannot unify "VarSet.In a (VarSet.inter (judge x t) g)" and
"VarSet.In a (VarSet.inter x g)").

However, if I change the type of xfree to disj_vars (VarSet.singleton x) g, then the definition works fine! This seems very odd, as disj_vars is defined only on VarSets, and so it seems like x should automatically be converted toVarSet.singleton x since that's how the coercion is set up.

Even weirder is the fact that if I don't set up the coercion from vars to varsets, then Coq correctly complains about applying dis_vars to a var instead of a VarSet. So the coercion is definitely doing something

Can someone explain to me why the first definition fails? Given the coercions I've set up, to me it like all the definitions above should be equivalent

Note

Changing the type of xfree to disj_vars (judge x t) g also fixes the error. This seems odd too, since to be able to apply disj_vars to j := (judge x t), it first needs to be coerced to a ty_ctx via cons j nil, then to a VarSet via bound_variables, which should produce a VarSet containing only x (which is equivalent to VarSet.singleton x?). So this coercion chain seems to go off without a hitch, while the other one fails even though it's simpler

Solution

  • If you use Set Printing Coercions., the error message will be much more informative about the problem:

    The term "xfree" has type "disj_vars (var_to_varset x) (bound_variables g)"
while it is expected to have type
 "disj_vars (bound_variables (coerce_judgement_to_ty_ctx (judge x t)))
    (bound_variables g)"

    The problem is that the coercion of x into a VarSet.t is equal to Var.singleton x, while the coercion in judge reduces to VarSet.union (VarSet.singleton x) VarSet.empty. While these two are propositionally equal, they are not judgmentally equal, so as far as Coq is concerned, the term it came up with is ill-typed.