# Re: [isabelle] remdups_adj crucial lemma

```On 26.08.2014 10:05, René Thiemann wrote:
> Dear all,
>
>> It seems to me that we need an abstract nonrecursive characterisation of
>> remdups_adj from which specific lemmas follow easily. Is the following correct?
>>
>> remdups_adj xs = ys <->
>> EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
>>  & (ALL i < size xs. xs!i = ys!(f i)
>>       & (xs!i = xs!(i+1) <-> f i = f(i+1)))
>> It should be sound (-->), but is it complete (<--)?
> At least there needs to be one more implication added, since
> otherwise the reference to xs!(i+1) is critical.
>
> remdups_adj xs = ys <->
> EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
>  & (ALL i < size xs. xs!i = ys!(f i)
>       & (i + 1 < size xs --> (xs!i = xs!(i+1) <-> f i = f(i+1))))
>
> Otherwise, it looks good (soundness and completeness can easily be proven
> for lists upto length 1, but the inductive case became quite tedious in my proof attempt)
I've got a (lenghty, but otherwise straightforward) proof of
completeness for the modified theorem.
```
```theory Scratch imports Main begin

lemma "(\<exists>f :: nat \<Rightarrow> nat. mono f \<and> f ` {0 ..< size xs} = {0 ..< size ys}
\<and> (\<forall>i < size xs. xs!i = ys! (f i))
\<and> (\<forall>i. i + 1 < size xs \<longrightarrow> (xs!i = xs!(i+1) \<longleftrightarrow> f i = f(i+1))))
proof (induct xs arbitrary: ys rule: remdups_adj.induct)
case 1 then show ?case by auto
next
case (2 x) then obtain f where f_img: "f ` {0 ..< size [x]} = {0 ..< size ys}"
and f_nth: "\<And>i. i < size [x] \<Longrightarrow> [x]!i = ys!(f i)"
by metis

have "length ys = card (f ` {0 ..< size [x]})"
using f_img by auto
then have "length ys = 1" by auto
moreover
then have "f 0 = 0" using f_img by auto
ultimately show ?case using f_nth by (cases ys) auto
next
case (3 x1 x2 xs)
from "3.prems" obtain f where f_mono: "mono f"
and f_img: "f ` {0..<length (x1 # x2 # xs)} = {0..<length ys}"
and f_nth1: "\<And>i. i < length (x1 # x2 # xs) \<Longrightarrow> (x1 # x2 # xs) ! i = ys ! f i"
and f_nth2: "\<And>i. i + 1 < length (x1 # x2 #xs) \<Longrightarrow>
((x1 # x2 # xs) ! i = (x1 # x2 # xs) ! (i + 1)) = (f i = f (i + 1))"
by metis

show ?case
proof cases
assume "x1 = x2"

let ?f' = "f o Suc"

have "remdups_adj (x1 # xs) = ys"
proof (intro "3.hyps" exI conjI impI allI)
show "x1 = x2" by fact
next
show "mono ?f'"
using f_mono by (simp add: mono_iff_le_Suc)
next
have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
by safe (fastforce, rename_tac x, case_tac x, auto)
also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
proof -
have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth2[of 0] by simp
then show ?thesis by safe (fastforce, rename_tac x, case_tac x, auto)
qed
also have "\<dots> = {0 ..< length ys}" by fact
finally show  "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
next
fix i assume "i < length (x1 # xs)"
then show "(x1 # xs) ! i = ys ! ?f' i"
using f_nth1[of "Suc i"] \<open>x1 = x2\<close> by simp
next
fix i assume "i + 1 < length (x1 # xs)"
then show "((x1 # xs) ! i = (x1 # xs) ! (i + 1)) = (?f' i = ?f' (i + 1))"
using f_nth2[of "Suc i"] \<open>x1 = x2\<close> by simp_all
qed
then show ?thesis using \<open>x1 = x2\<close> by simp
next
assume "x1 \<noteq> x2"

then have "f 0 \<noteq> f (Suc 0)" using f_nth2[of 0] by auto

have "2 \<le> length ys"
proof -
have "2 = card {f 0, f 1}" using \<open>f 0 \<noteq> _\<close> by simp
also have "\<dots> \<le> card (f ` ({0, 1} \<union> {2..< Suc (Suc (length xs))}))" (is "_ \<le> card (f ` ?S)")
by (rule card_mono) auto
also have "?S = {0..<Suc (Suc (length xs))}" by auto
also have "card (f ` \<dots>) = length ys" using f_img by simp
finally show "2 \<le> length ys" .
qed

have "f 0 = 0"
proof (rule ccontr)
assume "f 0 \<noteq> 0"
then have "\<And>i. 0 \<noteq> f i"
using f_mono by (metis le0 le_0_eq monoD)
then have "0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}"
by (auto simp del: neq0_conv)
then show False using f_img by auto
qed

have "f (Suc 0) = Suc 0"
proof (rule ccontr)
assume "f (Suc 0) \<noteq> Suc 0"
then have "Suc 0 < f (Suc 0)" using f_nth2[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto
then have "\<And>i. Suc 0 < f (Suc i)"
using f_mono by (metis Suc_le_mono le0 less_le_trans monoD)
then have "\<And>i. Suc 0 \<noteq> f i" using \<open>f 0 = 0\<close>
by (metis less_irrefl_nat not0_implies_Suc)
then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
then show False using f_img \<open>2 \<le> length ys\<close> by auto
qed

obtain ys' where "ys = x1 # x2 # ys'"
using \<open>2 \<le> length ys\<close> f_nth1[of 0] f_nth1[of 1]
apply (cases ys)
apply (rename_tac  ys', case_tac  ys')
by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)

def f' \<equiv> "\<lambda>x. f (Suc x) - 1"

{ fix i
have "Suc 0 \<le> f (Suc 0)" using f_nth2[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close>  by auto
also have "\<dots> \<le> f (Suc i)" using f_mono by (rule monoD) arith
finally have "Suc 0 \<le> f (Suc i)" . }
note X = this

{ fix i have "f (Suc i) = Suc (f' i)"
using X[of i] by (auto simp: f'_def) }
note f_Suc = this

have "remdups_adj (x2 # xs) = (x2 # ys')"
proof (intro "3.hyps" exI conjI impI allI)
show "x1 \<noteq> x2" by fact
next
show "mono f'"
using X f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff)
next
have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}"
apply safe
apply (rename_tac [!] n,  case_tac [!] n)
apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI)
done
also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}"
by (auto simp: image_comp)
also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}"
by (simp only: f_img)
also have "\<dots> = {0 ..< length (x2 # ys')}"
using \<open>ys = _\<close> by (fastforce intro: rev_image_eqI)
finally show  "f' ` {0 ..< length (x2 # xs)} = {0 ..< length (x2 # ys')}" .
next
fix i assume  "i < length (x2 # xs)"
then show "(x2 # xs) ! i = (x2 # ys') ! f' i"
using f_nth1[of "Suc i"] \<open>x1 \<noteq> x2\<close> f_Suc by (simp add: \<open>ys = _\<close>)
next
fix i assume "i + 1 < length (x2 # xs)"
then show "((x2 # xs) ! i = (x2 # xs) ! (i + 1)) = (f' i = f' (i + 1))"
using f_nth2[of "Suc i"] \<open>x1 \<noteq> x2\<close> f_Suc by (auto simp: \<open>ys = _\<close>)
qed
then show ?case using \<open>ys = _\<close> \<open>x1 \<noteq> x2\<close> by simp
qed
qed

end
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.