## Stream: Coq users

### Topic: succ of number

#### zohaze (Sep 19 2022 at 14:53):

With the help of given inductive hypothesis ,i want to solve goal statement. Is it enough inforamation or what more hypothesis i should have?

``````IH1 : count_occ (firstn m l) 0  <=    S (count_occ (firstn m l) (S k))

Goal:count_occ (firstn m (b :: l)) 0 <=  S ( count_occ (firstn m (b :: l)) (S k))
``````

#### James Wood (Sep 19 2022 at 15:01):

Consider `m := 3`, `l := [0; 0; 1]`, `k := 0`, `b := 0`. You might want to double-check, but I think that's a counterexample.

#### James Wood (Sep 19 2022 at 15:02):

As for extra hypotheses you could want, it doesn't seem like a very natural goal, so I wouldn't know what to suggest. What's the bigger picture?

#### Pierre Castéran (Sep 19 2022 at 18:59):

There was a recent stream about lists, `count_occ`and `firstn`:
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/which.20one.20is.20greater

A few of us mentionned that it's almost impossible to study a partially given sub-goal, without any possibility of reproducing the given issue.

#### Paolo Giarrusso (Sep 19 2022 at 20:17):

I've been tempted for a while to try suggesting rules about this, since these questions are unhelpful to everybody, but no idea how to phrase them. For now, I have resorted to muting a bunch of users.

(deleted)

#### zohaze (Sep 20 2022 at 01:40):

@James Wood you given an example. In this example if i add k cannot be zero then could i prove it? Because i have only information that two non equal numbers have <= relation ,while count them in list. Secondly, what type of information about b is required? Like b=0 b=s k or what basis b is at head of the list or information about list arrangement? induction on b is require here?

#### James Wood (Sep 20 2022 at 06:45):

`b = S k` should do it, yeah.

#### James Wood (Sep 20 2022 at 06:51):

`b` and `k` are acting more like identifiers than numbers, so it wouldn't really make sense to do induction on them. You could try proving this in a more general setting where `b` and `S k` are of some type with decidable equality, and you have the inequality `0 <> S k`.

#### zohaze (Sep 21 2022 at 01:04):

Would you like to give an example of command using count_occ_cons_neq for case when b=0 & S k in above case /question?

Last updated: Jan 28 2023 at 05:02 UTC