Stream: Coq users

Topic: natural number counting

zeesha huq (Apr 17 2021 at 18:27):

Want to count two natural numbers(k1 and k2)that exist in the list. On the basis of this count I want to to find greater element.(count k1 l < count k2 l).

pianke (Aug 05 2022 at 18:48):

I have (a::l0) list nat. There is function f, whose input is (c::l0) and output is l1. During recursive call number of elements
in l1 are going to increase.( m ,c,c0 & k are nat).

H: (m > 0 ->
count_occ Nat.eq_dec (firstn m 11) 0 <= count_occ Nat.eq_dec (firstn m 11) (S k) ->
count_occ Nat.eq_dec (firstn (S m) l1 0 <= count_occ Nat.eq_dec (firstn (S m) l1 (S k)))).

When (c::c0::l0) is given to function f, then

Goal: count_occ Nat.eq_dec  (firstn (S m) l1 0 <= count_occ Nat.eq_dec (firstn (S m) l1 (S k).

To prove above i should focuss on role of c0 in f? How to proceed? I have already asked but might be not properly asked.

Last updated: Feb 01 2023 at 13:03 UTC