## 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: Sep 25 2021 at 09:17 UTC