时间戳

首页 > 解决方案 > 如何告诉 simp 实例化原理图变量？

isabelle - 如何告诉 simp 实例化原理图变量？

问题描述

在下面的示例中，我想使用 simp 来证明来自简单类型 lambda 演算类型检查的一些术语。我将每个类型检查规则添加为 simp 的重写规则，因此 simp 执行条件重写并在此过程中创建示意图变量。但是，在为某些重写重写附带条件时，simp 卡在涉及原理图变量的重写术语上，因为它没有实例化它们：

theory Stlc imports Main
begin

type_synonym var = string

datatype exp =
    Var var
  | Const nat
  | Plus exp exp
  | Abs var exp
  | App exp exp

datatype type =
   Nat |
   Fun type type

type_synonym ('k, 'v) fmap = "'k ⇒ 'v option"

definition lookup :: "('k, 'v) fmap ⇒ 'k ⇒ 'v option" where
  "lookup m x = m x"

definition add :: "('k, 'v) fmap ⇒ 'k ⇒ 'v ⇒ ('k, 'v) fmap" where
  "add m x a = (λy. if y = x then Some a else m y)"

definition empty :: "('k, 'v) fmap" where
  "empty = (λy. None)"

notation
  lookup (infix "$?" 60) and
  add ("_ $+ '( _ ', _ ')") and
  empty ("$0")

inductive hasty :: "(var, type) fmap ⇒ exp ⇒ type ⇒ bool" where
  HtVar:
    "G $? x = Some t
    ⟹ hasty G (Var x) t" |
  HtConst:
    "hasty G (Const n) Nat" |
  HtPlus:
    "⟦ hasty G e1 Nat;
       hasty G e2 Nat ⟧
    ⟹ hasty G (Plus e1 e2) Nat" |
  HtAbs:
    "hasty (G $+ (x, t1)) e1 t2
    ⟹ hasty G (Abs x e1) (Fun t1 t2)" |
  HtApp:
    "⟦ hasty G e1 (Fun t1 t2);
       hasty G e2 t1 ⟧
    ⟹ hasty G (App e1 e2) t2"

named_theorems my_simps "simplification rules for typechecking"

declare HtVar [my_simps]
declare HtConst [my_simps]
declare HtPlus [my_simps]
declare HtAbs [my_simps]
declare HtApp [my_simps]

declare lookup_def [my_simps]
declare add_def [my_simps]

lemma "hasty $0 (Plus (Const 1) (Const 1)) Nat"
  using [[simp_trace_new mode=full]]
  apply(simp add: my_simps)
  done

lemma "hasty $0 (Abs ''n'' (Abs ''m'' (Plus (Var ''n'') (Var ''m''))))
             (Fun Nat (Fun Nat Nat))"
  apply (simp add: my_simps)
  done

lemma "⟦P ∧ Q ⟧ ⟹ Q"
  apply (rule conjE)
  apply(simp) (* note: this simp step does instantiate schematic variables *)
  apply assumption
  done

(* but here, it seems that simp does not instantiate schematic variables: *)
lemma eleven: "hasty $0 (App (App 
    (Abs ''n'' (Abs ''m'' (Plus (Var ''n'') (Var ''m''))))
    (Const 7)) (Const 4)) Nat"
  using [[simp_trace_new mode=full]]
  apply (simp add: my_simps) (* seems to fail on unifying "?t1.3 = type.Nat" *)

简化器跟踪的相关部分（我猜）如下：

    Apply rewrite rule? 
      Instance of Option.option.inject: Some ?t1.3 = Some type.Nat ≡ ?t1.3 = type.Nat
      Trying to rewrite: Some ?t1.3 = Some type.Nat 
        Successfully rewrote 
          Some ?t1.3 = Some type.Nat ≡ ?t1.3 = type.Nat 
Step failed 
  In an instance of Stlc.hasty.HtVar:
    (λy. if y = ''m'' then Some ?t1.1 else if y = ''n'' then Some ?t1.3 else $0 y) $? ''n'' = Some type.Nat ⟹
    hasty (λy. if y = ''m'' then Some ?t1.1 else if y = ''n'' then Some ?t1.3 else $0 y) (Var ''n'') type.Nat ≡ True
  Was trying to rewrite:
    hasty (λy. if y = ''m'' then Some ?t1.1 else if y = ''n'' then Some ?t1.3 else $0 y) (Var ''n'') type.Nat

就在失败的步骤之前，重写停止在?t1.3 = type.Nat. 但是，我想?t1.3 = type.Nat被重写为True，并 在此过程?t1.3中被实例化type.Nat。我怎样才能做到这一点？

标签： isabelle

解决方案

对于这种可以通过重复应用推理规则来解决的证明目标，应该使用经典推理器（auto）而不是重写器（simpl）。

如果我将所有打字规则声明为安全介绍规则：

declare HtVar [intro!]
declare HtConst [intro!]
declare HtPlus [intro!]
declare HtAbs [intro!]
declare HtApp [intro!]

然后我的大部分引理由 证明auto，这留下了两个可以通过以下方式解决的查找目标simp：

lemma eleven: "hasty $0 (App (App 
    (Abs ''n'' (Abs ''m'' (Plus (Var ''n'') (Var ''m''))))
    (Const 7)) (Const 4)) Nat"
  apply(auto)
  apply(simp_all add: my_simps)
  done

此外，给定一个经典的推理器，例如auto，可以很容易地指定在其余子目标上使用什么重写器，如下所示，因此上述证明可以浓缩为一行：

apply(auto simp add: my_simps)

然而，给定诸如 之类的重写器simp，指定在其余子目标上使用哪种方法似乎更复杂一些。

推荐阅读