CODEWITHSUNDEEP
isabelleinduction
Attila Karoly
Attila Karoly

Reputation: 1021

Induct on two variables?

Given a function that generates a list of identical items I wish to prove that the generated lists consist the given natural number at all positions independent of list length.

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"

It seems obvious that the proof should be based on induction on the length of the generated list but pos also seems to be an induction variable candidate. I'd appreciate any help on how to proceed with this proof.

Upvotes: 1

Views: 665

Answers (1)

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1941

The function pattern_n is equivalent to the function replicate from the standard library (theory List). The standard library also contains the theorem nth_replicate for the function replicate that is nearly identical to the theorem that you are trying to prove:

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

UPDATE

Alternatively, you can use induction to prove the result. Usually it is more convenient to use the definition in the form that is provided by the function pattern_n' below, because the theorems that are generated automatically when you define the function are more consistent with this form.

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 version: Isabelle2020

Upvotes: 1

Related Questions