证明关于解析器组合子的定理

Question

我写了一些简单的解析器组合器（没有回溯等）。以下是我的问题的重要定义。

type_synonym ('a, 's) parser = "'s list ⇒ ('a * 's list) option"

definition sequenceP :: "('a, 's) parser
                       ⇒ ('b, 's) parser
                       ⇒ ('b, 's) parser" (infixl ">>P" 60) where
  "sequenceP p q ≡ λ i . 
    (case p i of
        None ⇒ None
      | Some v ⇒ q (snd v))"

definition consumerP :: "('a, 's) parser ⇒ bool" where
  "consumerP p ≡ (∀ i . (case p i of 
    None ⇒ True |
    Some v ⇒ length (snd v) ≤ length i))"

我确实想证明以下引理。

lemma consumerPI: "consumerP p ⟹ consumerP q ⟹ consumerP (p >>P q)"
apply (unfold sequenceP_def)
apply (simp (no_asm) add:consumerP_def)
apply clarsimp
apply (case_tac "case p i of None ⇒ None | Some v ⇒ q (snd v)")
apply simp
apply clarsimp
apply (case_tac "p i")
apply simp
apply clarsimp
apply (unfold consumerP_def)

我到达了这个证明状态，我无法继续。

goal (1 subgoal):
 1. ⋀i a b aa ba.
       ⟦∀i. case p i of None ⇒ True | Some v ⇒ length (snd v) ≤ length i;
        ∀i. case q i of None ⇒ True | Some v ⇒ length (snd v) ≤ length i; q ba = Some (a, b); p i = Some (aa, ba)⟧
       ⟹ length b ≤ length i

任何人都可以告诉我如何解决这个目标吗？提前致谢！

Answer 1

事实证明，如果你只是想证明引理，没有进一步的洞察力，那么

lemma consumerPI: "consumerP p ⟹ consumerP q ⟹ consumerP (p >>P q)"
by (smt consumerP_def le_trans option.case_eq_if sequenceP_def)

完成任务。

如果您想获得洞察力，则需要结构化证明。首先确定一些关于 consumerP 的有用引理，然后写一个 Isar 证明，详细说明必要的步骤。

lemma consumerPI[intro!]:
  assumes "⋀ i x r . p i = Some (x,r) ⟹ length r ≤ length i"
  shows "consumerP p"
 unfolding consumerP_def by (auto split: option.split elim: assms)

lemma consumerPE[elim, consumes 1]:
  assumes "consumerP p"
  assumes "p i = Some (x,r)"
  shows "length r ≤ length i"
  using assms by (auto simp add: consumerP_def split: option.split_asm)

lemma consumerP_sequencePI: "consumerP p ⟹ consumerP q ⟹ consumerP (p >>P q)"
proof-
  assume "consumerP p"
  assume "consumerP q"
  show "consumerP (p >>P q)"
  proof(rule consumerPI)
    fix i x r
    assume "(p >>P q) i = Some (x, r)"
    then obtain x' r' where "p i = Some (x', r')" and "q r' = Some (x,r)"
      by (auto simp add: sequenceP_def split:option.split_asm)

    from `consumerP q` and `q r' = Some (x, r)`
    have "length r ≤ length r'" by (rule consumerPE)
    also
    from `consumerP p` and `p i = Some (x', r')`
    have "length r' ≤ length i" by (rule consumerPE)
    finally
    show "length r ≤ length i".
  qed
qed

事实上，对于此定义，您可以非常好地使用 inductive 命令，并免费获得 intro 和 elim 规则：

inductive consumerP where
  consumerPI: "(⋀ i x r . p i = Some (x,r) ⟹ length r ≤ length i) ⟹ consumerP p"

在上面的证明中，您可以将 by (rule consumerPE) 替换为 by cases 并且有效。

证明关于解析器组合子的定理

Proving a theorem about parser combinators

isabelle