how to prove below lemma · Beginner Questions

fun insert_sorted :: "'a :: linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "insert_sorted x Nil = Cons x Nil"
| "insert_sorted x (Cons y ys) = (case x \<le> y of
      True \<Rightarrow> Cons x (Cons y ys)
    | False \<Rightarrow> Cons y (insert_sorted x ys))"

fun ins_sort :: "'a :: linorder list \<Rightarrow> 'a list" where
  "ins_sort Nil = Nil"
| "ins_sort (Cons x xs) = insert_sorted x (ins_sort xs)"

lemma length_ins_sort: "length (ins_sort xs) = length xs"

Yong Kiam (Mar 06 2024 at 14:33):

Hongjian Jiang (Mar 06 2024 at 14:36):

Yes, I am trying to learn isabelle from begining. I am really struggling to figure out auxiliary lemma. This lemma I try to prove by induction twice, and compare first two elements. But not work.

Hongjian Jiang (Mar 06 2024 at 14:38):

lemma length_ins_sort: "length (ins_sort xs) = length xs"
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a ys)
  then show ?case apply auto
  proof(induct ys)
    case Nil
    then show ?case apply auto done
  next
    case (Cons b zs)
    then show ?case
    proof (cases "a ≤ b")
      case True
      then show ?thesis  apply simp  sorry
    next
      case False
      then show ?thesis sorry
    qed
  qed
qed

Yong Kiam (Mar 06 2024 at 14:38):

you're on the right track: in this case, you probably want to start with an auxliary lemma about insert_sorted to keep things nicer --- you could think of a length property that holds for insert_sorted

Hongjian Jiang (Mar 06 2024 at 14:43):

Thanks, it works now. Is there any basic idea to think about these auxiliar lemma?

Yong Kiam (Mar 06 2024 at 14:45):

in this case, insert_sorted is an auxiliary function for your insertion sort, so it makes sense that you would want to write an auxiliary lemma for it

Hongjian Jiang (Mar 07 2024 at 09:24):

lemma sqrt_2_irrational: "\<not> (\<exists> q :: rat. q^2 = 2)"
proof
  text \<open>Each sorry can be removed by a proof search via @{command try} or @{command sledgehammer}.\<close>
  assume "\<exists> q :: rat. q^2 = 2"
  then obtain q :: rat where "q^2 = 2"
    by blast
  obtain m n where "q = of_int m / of_int n"  "coprime m n"
    by (metis Fract_of_int_quotient Rat_cases)
  then have "of_int m ^ 2 = (2::rat) * of_int n ^ 2"
    by (metis ‹q⇧2 = 2› divide_eq_0_iff nonzero_eq_divide_eq power_divide zero_neq_numeral)
  then have "2 dvd m"
    by (metis (mono_tags, lifting) even_mult_iff even_numeral of_int_eq_iff of_int_mult of_int_numeral power2_eq_square)
  then obtain r where "m = 2*r"
    by blast
  then have "(2 :: rat) * of_int r ^ 2 = of_int n ^ 2"
    using ‹(rat_of_int m)⇧2 = 2 * (rat_of_int n)⇧2› by auto
  then have "2 dvd n"
    by (metis (mono_tags, lifting) even_mult_iff even_numeral of_int_eq_iff of_int_mult of_int_numeral power2_eq_square)
  then show False
    using ‹coprime m n› ‹even m› by auto
qed


lemma sqrt_2_irrational_main: "\<not> (\<exists> (q :: real) \<in> \<rat>. q^2 = 2)"
  sorry

Yong Kiam (Mar 07 2024 at 15:18):

Mathias Fleury (Mar 07 2024 at 15:25):

My guess is that: if this is an Isabelle question, then the answer to the question is Rats_cases. If the question is "how do I start here", then the answer is: how would you start on paper?

Stream: Beginner Questions

Topic: how to prove below lemma

Hongjian Jiang (Mar 06 2024 at 14:32):