Индукция по длине, а затем по индуктивному правилу для контекстной свободной грамматики (пример из прог-доказы)

Question

Я новичок в Isabelle/HOL (хотя и не в HOL), поэтому решил начать обучение, работая над примерами в отличный "prog-prove" tutorial.

Я застрял в контексте бесплатной грамматики (упражнение 3.5 на стр. 43). В этом вопросе вы получаете два контекстных бесплатных грамматики:

S → ε | aSb | SS 
T → ε | TaTb 

, и вас попросят доказать, что они описывают один и тот же язык. Доказательство того, что элементы из Т лежат на языке, описанном S, легко, но я борюсь с другим направлением. В частности, я хочу показать, что язык, описанный Т, закрывается при конкатенации.

Это неофициальное доказательство. Предположим, что u и v лежат на этом языке. Затем мы хотим доказать, что uv лежит на этом языке. Продолжайте индукцию по длине v. Если length v = 0, то v - это пустая строка и uv = u, и все готово. В противном случае рассмотрим правила производства для T. Очевидно, что v не является пустой строкой, поэтому он должен иметь вид waxb для некоторого w, x на этом языке. Поскольку w короче v, (сильная) индукция показывает, что uw должен лежать на языке. Теперь используйте второе правило производства.

Это доказательство кажется довольно сложным, поэтому я подозреваю, что это не тот, о котором говорил автор prog-proof. Поэтому у меня есть два вопроса:

1. Что (неофициально или официально) является доказательством того, что автор упражнения надеется использовать?

2. (Более технический) Как я могу выразить свое неофициальное доказательство выше в Isabelle/HOL?

Моя попытка/верчение до сих пор начинается со следующим:

lemma T_mult: "cfT u ==> cfT v ==> cfT (u @ v)" 
    apply (induction "length v") 
    apply (auto) 
    apply (induction v rule: cfT.induct) 

и второй индукционный сбой приложения, но я предполагаю, что это потому, что я прошу Изабеллу делать неправильные вещи. ..

Answer 1

Я не могу сказать, что ожидали авторы, но позвольте мне прокомментировать;) Во-первых, каково ваше определение T и S? Я просто предположим следующее:

datatype alphabet = a | b 

inductive S 
where 
    empty [simp]: "S []" | 
    betw: "S x ⟹ S (a # x @ [b])" | 
    conc: "S x ⟹ S y ⟹ S (x @ y)" 

inductive T 
where 
    empty [simp]: "T []" | 
    conc_betw: "T x ⟹ T y ⟹ T (x @ a # y @ [b])" 

Вы правы, что T x ==> T y ==> T (x @ y) является решающим лемма. Что касается доказательства этой леммы, то синус имеет эмпирические (и эвристически) индуктивные определения, их соответствующие правила поведения, скорее всего, будут полезны для доказательства фактов о них по индукции. У меня такое ощущение, что другие схемы индукции, такие как ваша индукция по натуральным числам с length v, усложняют вещи без необходимости.

неформально для доказательства

lemma 
    assumes "T x" and "T y" 
    shows "T (x @ y)" 

Я хотел бы сначала сделать анализ случая на структуру T x (по делам грамматики, соответствующий факт является T.cases), а затем индукцией по T y (с использованием правила T.induct), но могут быть другие способы сделать это. Общая структура будет

using assms 
proof (cases rule: T.cases) 
    case empty 
    ... 
next 
    case (conc_betw u v) 
    with `T y` show ?thesis 
    apply (induct rule: T.induct) 
    ... 
qed 

Update: На самом деле, случай анализа над структурой x оказывается излишним. Неформально я бы сказал следующее. Предположим, что выполнены T x и T y. Теперь примените индукцию по структуре y в соответствии с правилами формирования T.

• y = []. Затем мы делаем это с T (x @ y) = T (x @ []) = T x, что является одним из предположений.

• y = u @ a # v @ [b]. По индуктивному предположению (IH) имеем T u, T v, T (x @ u) и T (x @ v). Теперь инстанцировании второе правило формирования T мы имеем

  T (x @ u) ==> T v ==> T ((x @ u) @ a # v @ [b]) 
  

  , упрощающий к T (x @ u) ==> T v ==> T (x @ u @ a # v @ [b]) (по ассоциативности @) и, таким образом, позволяет уменьшить нашу основную цель, которая случается быть T (x @ u @ a # v @ [b]) к двум подзадач T (x @ u) и T v, которые, в свою очередь, удерживаются IH.