Stream: Beginner Questions

Topic: something better than auto

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.

Mathias Fleury (Jan 20 2021 at 10:01):

What is unreadable about by auto?

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.

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.

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.

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?

Gergely Buday (Jan 20 2021 at 10:24):

Oh well.

Last updated: Dec 21 2024 at 16:20 UTC