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.

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)
```

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