Как я могу сказать Simp для создания экземпляров схематических переменных?

Question

В приведенном ниже примере я хочу использовать simp, чтобы доказать, что некоторые термины из простой типизированной проверки типа лямбда-исчисления.Я добавляю каждое правило проверки типов в качестве правила перезаписи для 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 по пути.Как мне этого добиться?

Answer 1

Похоже, что для такого рода целей доказательства, которые могут быть решены путем многократного применения правила вывода, следует использовать классический аргумент (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, представляется более сложным указать, какой метод использовать в оставшихся подцелях.

Answer 2

Упрощающий Изабель сам по себе никогда не создает никаких схематических переменных в цели.Это делают только так называемые решатели.например, решатель HOL unsafe пробует среди прочих тактику rule refl и assumption.Вот почему пример с ⟦P ∧ Q ⟧ ⟹ Q работает с simp.

. Для решения допущений правил условного переписывания, таких как HtVar, субголер также играет роль.Субголер определяет, как должны быть решены условия.По умолчанию в HOL это asm_simp_tac, т. Е. Эквивалентно методу simp (no_asm_simp).Этот subgoaler не может обрабатывать создание схем в предположении.Это можно увидеть, включив другую трассировку упрощения:

using [[simp_trace]] supply [[simp_trace_depth_limit=10]]
apply (simp add: my_simps)

выдает следующее сообщение трассировки:

[6]Proved wrong theorem (bad subgoaler?)
hasty (λy. if y = ''m'' then Some ?t1.1 else if y = ''n'' then Some type.Nat else $0 y) (Var ''n'') type.Nat ≡ True
Should have proved:
hasty (λy. if y = ''m'' then Some ?t1.1 else if y = ''n'' then Some ?t1.3 else $0 y) (Var ''n'') type.Nat

Так что, если вы хотите использовать упрощитель для такого типа проверки типа,вам нужен другой subgoaler.Мне не хватает эксперта, чтобы помочь тебе с этим.Вы можете найти больше документации в справочном руководстве Изабель / Изар, раздел 9.3.6.

Вместо этого я рекомендую вам написать свой собственный метод вывода типов (например, с использованием Eisbach), который применяет правила вывода типов и вызовыУпрощение по мере необходимости.Это позволяет избежать проблем с subgoaler.