## 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: Dec 07 2023 at 08:19 UTC