Stream: Coq users

Topic: Library module


view this post on Zulip zeesha huq (Apr 17 2021 at 12:05):

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.

view this post on Zulip Ana de Almeida Borges (Apr 19 2021 at 12:20):

Require Import List.
Check count_occ.

This works for me.

view this post on Zulip zeesha huq (Apr 23 2021 at 16:28):

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?

view this post on Zulip zeesha huq (Apr 23 2021 at 16:31):

(deleted)

view this post on Zulip Li-yao (Apr 23 2021 at 16:48):

The first argument of count_occmust be an equality comparison function, and you passed it a list instead.

view this post on Zulip zeesha huq (Apr 23 2021 at 17:55):

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.

view this post on Zulip Li-yao (Apr 23 2021 at 18:05):

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.

view this post on Zulip Li-yao (Apr 23 2021 at 18:06):

From Coq Require Import Arith List.

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

view this post on Zulip zeesha huq (Apr 23 2021 at 18:08):

Ok,thank you.


Last updated: Feb 04 2023 at 21:02 UTC