Stream: Beginner Questions

Topic: Wellorder instance of char


view this post on Zulip Robert Soeldner (Jul 18 2021 at 11:15):

I'm stuck at proving the wellorder properties for char. The current goal is

proof (prove)
goal (1 subgoal):
 1. (P::char  bool) a::char. (x::char. (y::char. of_char y < of_char x  P y)  P x)  P a

I would assume this should be pretty straightforward since there exist a wellorder instance for nat?

view this post on Zulip Alexander Taepper (Jul 18 2021 at 16:27):

I played around a bit and came up with this instantiation proof:

lemma wellorder_char:
  "class.wellorder (λc d. of_char c ≤ (of_char d :: nat)) (λc d. of_char c < (of_char d :: nat))"
proof (standard, auto)
  fix P a
  assume step: "(⋀y. (of_char y :: nat) < (of_char x :: nat) ⟹ P y) ⟹ P x" for x :: char
  define n where "n = (of_char a :: nat)"
  have "⋀q. (of_char q :: nat) ≤ n ⟹ P q"
  proof (induction n rule: less_induct)
    case (less x)
    then show ?case
      by (metis step nat_less_le)
    qed
  then show "P a"
    by (simp add: n_def)
qed

I assume it can be simplified, but hope this helps :)

view this post on Zulip Manuel Eberl (Jul 18 2021 at 16:33):

proof (standard, auto)? I see you like to live dangerously. :smiling_devil:

view this post on Zulip Manuel Eberl (Jul 18 2021 at 16:55):

Note that if you want a linorder instance for char, you should import HOL-Library.Char_ord.

view this post on Zulip Manuel Eberl (Jul 18 2021 at 16:56):

As for wellorder, here's a more general solution that works for any finite types:

class finite_linorder = finite + linorder
begin

subclass wellorder
proof
  fix P :: "'a ⇒ bool" and x :: 'a
  assume IH: "⋀x. (⋀y. y < x ⟹ P y) ⟹ P x"
  define xs where "xs = sorted_list_of_set (UNIV :: 'a set)"
  define f where "f = (λi. xs ! i)"
  define n where "n = card (UNIV :: 'a set)"
  have xs: "set xs = UNIV" "sorted xs" "distinct xs" and n: "length xs = n"
    unfolding xs_def using finite[of UNIV] by (simp_all add: n_def)

  have range_f: "∃j<n. f j = y" for y
    using xs unfolding f_def by (metis UNIV_I in_set_conv_nth n)
  from xs have less_iff: "f i < f j ⟷ i < j" if "i < n" "j < n" for i j
    using that n unfolding f_def
    by (metis linorder_class.not_le local.antisym_conv1 local.not_less local.sorted_nth_mono
              nth_eq_iff_index_eq order_class.less_le)

  from range_f obtain i where "i < n" "f i = x"
    by blast
  moreover have "P (f i)" if "i < n"
    using that by (induction i rule: less_induct) (use IH range_f less_iff in metis)
  ultimately show "P x"
    by blast
qed

end

instance char :: finite_linorder ..

view this post on Zulip Manuel Eberl (Jul 18 2021 at 16:58):

Or, alternative solution without the extra type class:

lemma finite_linorder_is_wellorder:
  assumes "SORT_CONSTRAINT('a :: {finite, linorder})"
  shows   "OFCLASS('a, wellorder_class)"
proof
  fix P :: "'a ⇒ bool" and x :: 'a
  assume IH: "⋀x. (⋀y. y < x ⟹ P y) ⟹ P x"
  define xs where "xs = sorted_list_of_set (UNIV :: 'a set)"
  define f where "f = (λi. xs ! i)"
  define n where "n = card (UNIV :: 'a set)"
  have xs: "set xs = UNIV" "sorted xs" "distinct xs" and n: "length xs = n"
    unfolding xs_def using finite[of UNIV] by (simp_all add: n_def)

  have range_f: "∃j<n. f j = y" for y
    using xs unfolding f_def by (metis UNIV_I in_set_conv_nth n)
  from xs have less_iff: "f i < f j ⟷ i < j" if "i < n" "j < n" for i j
    using that n unfolding f_def
    by (metis not_less sorted_nth_mono nth_eq_iff_index_eq less_le)

  from range_f obtain i where "i < n" "f i = x"
    by blast
  moreover have "P (f i)" if "i < n"
    using that by (induction i rule: less_induct) (use IH range_f less_iff in metis)
  ultimately show "P x"
    by blast
qed

instance char :: wellorder
  by (rule finite_linorder_is_wellorder)

view this post on Zulip Robert Soeldner (Jul 18 2021 at 17:41):

Thank you for this. Impressive how fast you found the proof :)


Last updated: Sep 25 2021 at 08:21 UTC