zeesha huq (Apr 17 2021 at 12:05): 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.
Ana de Almeida Borges (Apr 19 2021 at 12:20):Require Import List.
Check count_occ.
This works for me.
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?
zeesha huq (Apr 23 2021 at 16:31):(deleted)
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.
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.
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.
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.
Ok,thank you.
Last updated: Oct 13 2024 at 01:02 UTC