Stream: Coq users

Topic: Nat counting


view this post on Zulip zohaze (May 21 2022 at 05:14):

I have list of natural numbers , want to extract list information from below .Please guide me how to write it(in form of lemma).
count_occ Nat.eq_dec [2,4,2,8] 2 > count_occ Nat.eq_dec [2,4,2,8] 8 ->
l= [2,4,2,8].

view this post on Zulip Pierre Castéran (May 21 2022 at 07:10):

I don't understand which lemma you want to prove.

view this post on Zulip zohaze (May 21 2022 at 15:59):

cbn works .Thanks.

view this post on Zulip pianke (Jun 20 2022 at 13:30):

l is non empty list of nat.
H: count_occ Nat.eq_dec l 2 > count_occ Nat.eq_dec l 8
Goal: count_occ Nat.eq_dec (2::l ) 2 > count_occ Nat.eq_dec (2::l) 8. lia should solve it but it is not working .How to prove it?

view this post on Zulip Pierre Castéran (Jun 20 2022 at 14:31):

May be lia did not find H. You may reintroduce it in the current goal.
generalize H. cbn. lia. works.


Last updated: Jan 29 2023 at 06:02 UTC