Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proof of well-foundedness of lexicographic lists

Email Gateway (Aug 22 2022 at 19:55):

From: Martin Desharnais <martin.desharnais@gmail.com>
Hi Mathias, Mark, and Lawrence,

Thank you for your help. I now realize that the lists I am using just
happen to be of equal size but that I never actually used this property.

I reformulated my formalization to use wf_lex and it now works
perfectly. I should have searched more thoroughly for these definitions
and not only in the Wellfounded theory.

Thank you very much,
Martin Desharnais

Email Gateway (Aug 22 2022 at 20:05):

From: Martin Desharnais <martin.desharnais@gmail.com>
Dear Isabelle users,

I am badly in need of help to prove a lemma about well-foundedness. I
defined the lexicographic ordering of two lists of equal length as follows.

fun lex_list :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
"lex_list order (x # xs) (y # ys) =
(order x y ∨ x = y ∧ lex_list order xs ys)" |
"lex_list order _ _ = False"

I now want to show that, if the ordering relation is well-founded, so
will be its lexicographic lifting to lists.

lemma lex_list_wfP:
assumes "wfP order"
shows "wfP (lex_list order)"
oops

Sadly, I fail to find the correct way to prove this. My first strategy
without induction [1] obviously failed in the recursive case. I then
tried various proofs by functional induction over lex_list, but always
painted myself into a corner. Does someone knows what the correct proof
would be?

Regards,
Martin Desharnais

[1]: First (incorrect) strategy without induction.
lemma lex_list_wfP:
assumes "wfP order"
shows "wfP (lex_list order)"
proof (rule wfPUNIVI)
fix P
assume hyps0: "∀x. (∀y. lex_list order y x ⟶ P y) ⟶ P x"
hence hyps1: "(⋀y. lex_list order y x ⟹ P y) ⟹ P x" for x by simp
hence hyps2: "(⋀y ys. lex_list order (y # ys) (x # xs) ⟹ P (y # ys))
⟹ P (x # xs)" for x xs
by (metis (full_types) lex_list.simps(3) neq_Nil_conv)
have 0: "(⋀y. order y xa ⟹ ∀xs. P (y # xs)) ⟹ lex_list order (y # ys)
(xa # xs) ⟹ P (y # ys)" for x xa xs y ys
apply simp
apply (erule disjE)
apply simp
sorry
have "P []"
using hyps0 by fastforce
moreover have "⋀x xs. P (x # xs)"
apply (atomize (full))
apply (rule allI)
apply (rule wfP_induct_rule[OF assms(1), of "λx. ∀xs. P (x # xs)"])
apply (rule allI)
apply (rule hyps1)
using 0 by (metis lex_list.elims(2))
ultimately show "P xs" for xs
by (cases xs) simp_all
qed

Email Gateway (Aug 22 2022 at 20:05):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Martin,

Unless I am mistaken, your definition does not entail that the lists have the same length and therefore the theorem does not hold:

fun lex_list :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
"lex_list order (x # xs) (y # ys) =
(order x y \<or> x = y \<and> lex_list order xs ys)" |
"lex_list order _ _ = False"

fun f where "f n = replicate n (0 :: nat) @ [1, 0]"

lemma H: "lex_list (<) (f (Suc n)) (f n)"
by (induction n) auto

lemma "\<not>wfP (lex_list ((<) :: nat \<Rightarrow> _))"
unfolding wfP_def wf_iff_no_infinite_down_chain
apply auto
apply (rule exI[of _ f])
using H apply auto
done

Best,
Mathias

Email Gateway (Aug 22 2022 at 20:05):

From: Mark Wassell <mpwassell@gmail.com>
Hi,

Would HOL/List.thy help and in particular the section titled "Length
Lexicographic Ordering"?

Cheers

Mark

Email Gateway (Aug 22 2022 at 20:05):

From: Lawrence Paulson <lp15@cam.ac.uk>
Indeed, the required theorem is probably wf_lenlex.
Larry

Last updated: Apr 18 2024 at 08:19 UTC