Индукт по двум переменным?

Question

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

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 также кажется кандидатом в переменную индукции.Буду признателен за любую помощь в том, как поступить с этим доказательством.

Answer 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