Доказательство равенства двух привязок в Номинальной Изабель - PullRequest
Новая
       54

Доказательство равенства двух привязок в Номинальной Изабель

2 голосов
/ 11 июля 2020

Рассмотрим следующие типы данных с привязками в 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

Я хочу доказать, что две привязки, появляющиеся в отношении, равны. Я вижу два способа, которыми пользователь Isabelle может помочь:

  1. Если вы знаете Nominal Isabelle, возможно ли это сделать?
  2. В противном случае, равны ли два вхождения x в правиле T_Abs для помощника или это какая-то связанная переменная с другим идентификатором?

1 Ответ

1 голос
/ 11 июля 2020
  1. Если вы знаете Номинал Изабель, возможно ли это сделать?

К сожалению, доказать теорему, которую вы пытаетесь доказать, невозможно. Вот контрпример (доказательства были Sledgehammer ред.): 

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
В противном случае, равны ли два вхождения x в правиле T_Abs для помощника или они являются своего рода связанной переменной с разными идентификаторами?

Я считаю, что вы думаете о правильные линии и, надеюсь, приведенный выше пример прояснит любую путаницу, которая может у вас возникнуть. Как правило, вы можете интерпретировать значение Abs x t1 = Abs y t2 как альфа-эквивалент (λx. t1) и (λy. t2). Конечно, (λx. t1) и (λy. t2) могут быть альфа-эквивалентами, но x и y не равны.

...