Stream: Beginner Questions

Topic: something better than auto


view this post on Zulip Gergely Buday (Jan 20 2021 at 09:57):

Define a function count :: 'a ⇒ 'a list ⇒ nat that counts the number of occurrences of an element in a list. Prove count x xs ≤ length xs.

  "count x [] = 0"
| "count x (y#xs) = (if (x=y) then (1 + count x xs) else (count x xs))"

lemma count_cons: "count x (y#xs) ≤ 1 + count x xs"
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed

lemma count_less: "count x xs ≤ length xs"
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (simp add:count_cons)
qed

This does not work on the Cons case. by auto works but that is not very readable or elegant.

Can you give me a hint what is missing? Not a solution.

view this post on Zulip Mathias Fleury (Jan 20 2021 at 10:01):

What is unreadable about by auto?

view this post on Zulip Gergely Buday (Jan 20 2021 at 10:02):

update: ```Failed to finish proof⌂:
goal (1 subgoal):

  1. count x xs ≤ length xs ⟹ x = a ⟶ count a xs ≤ length xs```

@Mathias Fleury I would like to show the used lemmas other than trivial arithmetic equalities.

view this post on Zulip Gergely Buday (Jan 20 2021 at 10:03):

Also, one of the goals of theorem proving is to understand what's going on and that is not possible with auto.

view this post on Zulip Mathias Fleury (Jan 20 2021 at 10:16):

lemma count_less: "count x xs ≤ length xs"
  by (induction xs) auto

works on Isabelle2020 and RC2.

view this post on Zulip Mathias Fleury (Jan 20 2021 at 10:20):

Gergely Buday said:

Also, one of the goals of theorem proving is to understand what's going on and that is not possible with auto.

So you prefer

lemma count_less: "count x xs ≤ length xs"
  by (induction xs) (simp, smt?)+

because you can understand what is going on?

view this post on Zulip Gergely Buday (Jan 20 2021 at 10:24):

Oh well.


Last updated: Mar 29 2024 at 12:28 UTC