Блог

Главная - Вопросы по программированию - Индуцировать по двум переменным?

Индуцировать по двум переменным?

#isabelle #induction

#isabelle #индукция

Вопрос:

Учитывая функцию, которая генерирует список идентичных элементов, я хочу доказать, что сгенерированные списки содержат заданное натуральное число во всех позициях, независимо от длины списка.

 fun pattern_n :: "nat ⇒ nat ⇒ nat list" where
"pattern_n _ 0  = []" |
"pattern_n n lng = n # (pattern_n n (lng - 1))"

lemma pattern_n_1: "lng > 0 ∧ pos ≥ 0 ∧ pos < lng ∧ n ≥ 0 ⟹ (pattern_n n lng ! pos) = n"

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

Комментарии:

1. Что вы уже пробовали? Что не сработало / где вы застряли? Попробуйте применить индукцию так, как вы считаете правильным. Что происходит?

2. В третий раз я попытался индуцировать по lng с помощью apply(induction lng произвольно: n) и apply (simp), после чего Изабель все еще требует доказательства для шага индукции. В случае простой функции, такой как pattern_n, какие дополнительные знания можно было бы добавить для доказательства шага индукции? Моя единственная идея заключается в том, что каким-то образом позиция элемента также должна использоваться в качестве переменной индукции.

Ответ №1:

Функция pattern_n эквивалентна функции replicate из стандартной библиотеки (теория List ). Стандартная библиотека также содержит теорему nth_replicate для функции replicate , которая почти идентична теореме, которую вы пытаетесь доказать:

 fun pattern_n :: "nat ⇒ nat ⇒ nat list" where
  "pattern_n _ 0  = []" |
  "pattern_n n lng = n # (pattern_n n (lng - 1))"
    
lemma "pattern_n n k = replicate k n"
  by (induction k) auto
    
thm nth_replicate

Обновить

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

 fun pattern_n :: "nat ⇒ nat ⇒ nat list" where
  "pattern_n _ 0  = []" |
  "pattern_n n lng = n # (pattern_n n (lng - 1))"

fun pattern_n' :: "nat ⇒ nat ⇒ nat list" where
  "pattern_n' n 0  = []" |
  "pattern_n' n (Suc lng) = n # (pattern_n' n lng)"

lemma "pattern_n n lng = pattern_n' n lng"
  by (induct lng) auto

lemma pattern_n_1_via_replicate: 
  "pos < lng ⟹ (pattern_n val lng) ! pos = val"
proof(induct lng arbitrary: pos)
  case 0 then show ?case by simp
next
  case (Suc lng) then show ?case by (fastforce simp: less_Suc_eq_0_disj)
qed

Версия Isabelle: Isabelle2020

Комментарии:

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

2. @AttilaKaroly Спасибо за ваш комментарий. Я предоставил обновление. Кроме того, вам все еще может быть полезно использовать мой первый ответ, чтобы вывести методологию, которая использовалась для доказательства идентичной теоремы в стандартной библиотеке.

3. xanonec, pattern_n_1_via_replicate — это то, что я искал. Спасибо за вашу любезную помощь.

4. Дополнительный вопрос: где я мог бы узнать больше о правилах, таких как less_Suc_eq_0_disj? Я ничего не нахожу об этом в материалах Isabelle, а другие подобные правила, похоже, очень слабо документированы.

5. @AttilaKaroly less_Suc_eq_0_disj определяется в теории Nat . На случай, если вы не знали, если вы используете jEdit, то у вас должна быть возможность навести курсор на less_Suc_eq_0_disj в доказательстве и использовать cntrl lmb (может отличаться для разных ОС), чтобы быстро перейти к теории, где указано правило. В качестве дополнительного замечания, существует много разных способов доказать теорему, которую вы хотели доказать. Возможно, наилучшую методологию можно вывести, если вы изучите доказательство nth_replicate из стандартной библиотеки, как я уже упоминал в своем первом комментарии.