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_occand 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.

Pierre Castéran (Sep 19 2022 at 20:32):

(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: Oct 13 2024 at 01:02 UTC