count_occ function exist in the library. I have included list module. I am unable to use lemma related to this.If I copy this function in the script then it works.My question is why I redefine function when i have included library.

```
Require Import List.
Check count_occ.
```

This works for me.

I have Import List and check the presence of cont_occ. Function exist in the library.But still when I write lemma related to count_occ

get this message

In environment

l : list ?A

x : ?T

The term "l" has type "list ?A"

while it is expected to have type

"forall x0 y : ?A0, {x0 = y} + {x0 <> y}".

How to remove it and directly write lemma without defining count_occ?

(deleted)

The first argument of `count_occ`

must be an equality comparison function, and you passed it a list instead.

Require Import List Arith.

Import ListNotations.

Hypothesis eq_dec : forall x y : nat, {x = y}+{x <> y}.

Fixpoint count_occ (l : list nat) (x : nat) : nat :=

match l with

| [] => 0

| y :: tl =>

let n := count_occ tl x in

if eq_dec y x then S n else n

end.

Theorem count_occ_In l x : In x l <-> count_occ l x > 0.

I have defined eq_dec first then maintained the order of input arguments to this function.Now this code has no issue. But when I remove definitation of count_occ then it has above error message.

Yes, that's because `count_occ`

is defined in a section, so hypotheses become extra arguments when the section is closed. But when you are still in the same section (as you are when you copy the definition), that argument does not yet need to be supplied.

```
From Coq Require Import Arith List.
Theorem count_occ_In l x : In x l <-> count_occ Nat.eq_dec l x > 0.
```

Ok,thank you.

Last updated: Feb 04 2023 at 21:02 UTC