Stream: General

Topic: Multi-sort atoms in Nominal2

Javier Diaz (Jan 23 2023 at 16:18):

I'm experimenting with Nominal2's support for multi-sort atoms (see this example in the Nominal package and the discussion in Section 5 of this paper). The idea is to define a toy typed λ-calculus in Church's style, that is, where each variable includes its type (e.g. λxₒ. xₒ). So, I came up with the following code:

theory Scratch
  imports "Nominal2.Nominal2" "Nominal2.Atoms"
begin

(* In this example I'm using "var", "ty" and "Var" from Nominal2.Atoms *)

nominal_datatype exp =
    EVar var
  | EApp exp exp
  | EAbs x::var M::exp binds x in M

(* I want to prove that λxₒ. xₒ = λyₒ. yₒ *)
lemma "EAbs (Var x (TVar ''o'')) (EVar (Var x (TVar ''o''))) = EAbs (Var y (TVar ''o'')) (EVar (Var y (TVar ''o'')))"
  sorry (* cannot prove this! *)

end

As shown in the code above, the problem I found is that I cannot even prove the equality of two α-equivalent terms, which, I think, should work out of the box as is the case for single-sort atoms. Having a look at the Nominal2's implementation, it seems to me that the root cause is the lacking of a simproc similar to alpha_lst that works on at_base instead of at. However, since I'm not an expert in the Nominal package, I may very well be missing something.

Dmitriy Traytel (Jan 23 2023 at 16:59):

It is possible to prove it in a rather low-level fashion (see below). But generally, I agree with the assessment that as soon one leaves at, things are much more painful than they should be. For starters the various Abs1_eq_iff... lemmas that are available for at are lacking for at_base.

lemma supp_Var: "supp (Var x T) = {Atom (sort_of_ty T) x}"
  by (simp add: Abs_var_inverse Var_def atom_var_def supp_at_base)

lemma Rep_var_Var: "Rep_var (Var x T) = Atom (sort_of_ty T) x"
  using Rep_var[of "Var x T"]
  by (auto simp: Var_def Abs_var_inverse)

(* I want to prove that λxₒ. xₒ = λyₒ. yₒ *)
lemma "EAbs (Var x (TVar ''o'')) (EVar (Var x (TVar ''o''))) = EAbs (Var y (TVar ''o'')) (EVar (Var y (TVar ''o'')))"
  by (auto simp add: Abs_eq_iff2 alpha_lst exp.supp supp_Var Rep_var_Var atom_var_def
    Var_def[symmetric] supp_swap fresh_star_def permute_var_def
    intro!: exI[of _ "(atom (Var x (TVar ''o'')) ⇌ atom (Var y (TVar ''o'')))"]
    split: if_splits)

Javier Diaz (Jan 23 2023 at 17:06):

Dmitriy Traytel said:

It is possible to prove it in a rather low-level fashion (see below). But generally, I agree with the assessment that as soon one leaves at, things are much more painful than they should be. For starters the various Abs1_eq_iff... lemmas that are available for at are lacking for at_base.

lemma supp_Var: "supp (Var x T) = {Atom (sort_of_ty T) x}"
  by (simp add: Abs_var_inverse Var_def atom_var_def supp_at_base)

lemma Rep_var_Var: "Rep_var (Var x T) = Atom (sort_of_ty T) x"
  using Rep_var[of "Var x T"]
  by (auto simp: Var_def Abs_var_inverse)

(* I want to prove that λxₒ. xₒ = λyₒ. yₒ *)
lemma "EAbs (Var x (TVar ''o'')) (EVar (Var x (TVar ''o''))) = EAbs (Var y (TVar ''o'')) (EVar (Var y (TVar ''o'')))"
  by (auto simp add: Abs_eq_iff2 alpha_lst exp.supp supp_Var Rep_var_Var atom_var_def
    Var_def[symmetric] supp_swap fresh_star_def permute_var_def
    intro!: exI[of _ "(atom (Var x (TVar ''o'')) ⇌ atom (Var y (TVar ''o'')))"]
    split: if_splits)

Thanks a lot, Dmitriy. Your answer is very helpful. It seems to me that the current Nominal package is not yet ready for a serious formalization using multi-sort atoms. :oh_no:

Last updated: Apr 19 2024 at 16:20 UTC