I want to use lemma (count_occ_In)related to count_occ function from library.I have Imported library in the Coq Script. But still I am unable to use it. If I copy count_occ & eq_dec from library in the scipt,then it works. My question is why I should redefine function when I have included library module. Please guide me how to write lemma by adding the library module only(Not defining the functions again)?.
1 Answers
With the additional information this should work for you:
Require Import List Arith.
Import ListNotations.
Check count_occ.
Search nat ({?x = ?y} + {?x <> ?y}).
Definition count_occ_nat := count_occ Nat.eq_dec.
Definition count_occ_In_nat := count_occ_In Nat.eq_dec.
Check count_occ_nat.
Check count_occ_In_nat.
See how I used Check to find which arguments count_occ takes and how I used Search to find a suitable instance for the decidability of equality function.
count_occ is written like this because it should work for lists of any type with decidable equality, but then to use it, you need a proof that for your type equality is decidable, and you have to give this explicitly.
In modern definitions one makes such arguments implicit and uses type classes to automatically fill in information like decidable equality, but count_occ has an explicit argument for that, so you have to supply it.
Related