Proving two bindings equal in Nominal Isabelle

Question

Consider the following datatypes with bindings in Nominal Isabelle:

theory Example
  imports "Nominal2.Nominal2" 
begin

atom_decl vrs

nominal_datatype ty = 
    Tvar   "vrs"
  | Arrow x::vrs T::"ty" binds x in T

nominal_datatype trm = 
    Var   "vrs"
  | Abs   x::"vrs" t::"trm"  binds x in t 

inductive
  typing :: "trm ⇒ ty ⇒ bool" ("_ , _" [60,60] 60) 
where
 T_Abs[intro]: "(Abs x t) , (Arrow x T)"

equivariance typing
nominal_inductive typing done 

lemma 
  assumes "(Abs x t), (Arrow y T)"
  shows "x = y"
  using assms

I want to prove that the two bindings appearing in the relation are equal. I see two ways an Isabelle user could help:

If you know Nominal Isabelle is it possible to do this?
Otherwise, are the two occurrences of x in the rule T_Abs equal for the assistant or are they sort of bound variable with different identity?

user9716869 user9716869 · Accepted Answer · 2020-07-11T12:47:05

If you know Nominal Isabelle is it possible to do this?

Unfortunately, it is not possible to prove the theorem that you are trying to prove. Here is a counterexample (the proofs were Sledgehammered):

theory Scratch
  imports "Nominal2.Nominal2" 
begin

atom_decl vrs

nominal_datatype ty = 
    Tvar   "vrs"
    | Arrow x::vrs T::"ty" binds x in T

nominal_datatype trm = 
    Var   "vrs"
    | Abs   x::"vrs" t::"trm"  binds x in t 

inductive
  typing :: "trm ⇒ ty ⇒ bool" ("_ , _" [60,60] 60) 
where
 T_Abs[intro]: "(Abs x t) , (Arrow x T)"

equivariance typing
nominal_inductive typing . 

abbreviation s where "s ≡ Sort ''Scratch.vrs'' []"
abbreviation v where "v n ≡ Abs_vrs (Atom s n)"

lemma neq: "Abs (v 1) (Var (v 0)), Arrow (v (Suc (Suc 0))) (Tvar (v 0))"
  (is "?a, ?b")
proof-
  have a_def: "Abs (v 1) (Var (v 0)) = Abs (v (Suc (Suc 0))) (Var (v 0))"
    (*Sledgehammered*)
    by simp (smt Abs_vrs_inverse atom.inject flip_at_base_simps(3) fresh_PairD(2) 
        fresh_at_base(2) mem_Collect_eq nat.distinct(1) sort_of.simps trm.fresh(1))
  from typing.simps[of ?a ?b, unfolded this, THEN iffD2] have
    "Abs (v (Suc (Suc 0))) (Var (v 0)) , Arrow (v (Suc (Suc 0))) (Tvar (v 0))"
    by auto
  then show ?thesis unfolding a_def by clarsimp
qed

lemma "∃x y t T. x ≠ y ∧ (Abs x t), (Arrow y T)"
proof(intro exI conjI)
  show "v 1 ≠ v (Suc (Suc 0))" 
    (*Sledgehammered*)
    by (smt Abs_vrs_inverse One_nat_def atom.inject mem_Collect_eq n_not_Suc_n 
        sort_of.simps)
  show "Abs (v 1) (Var (v 0)) , Arrow (v (Suc (Suc 0))) (Tvar (v 0))"
    by (rule neq)
qed

end

Otherwise, are the two occurrences of x in the rule T_Abs equal for the assistant or are they sort of bound variable with different identity?

I believe that you are thinking along the right lines and, hopefully, the example above will clarify any confusion that you might have. Generally, you could interpret the meaning of Abs x t1 = Abs y t2 as the alpha-equivalence of (λx. t1) and (λy. t2). Of course, (λx. t1) and (λy. t2) may be alpha equivalent without x and y being equal.

Proving two bindings equal in Nominal Isabelle

1 Answers