zohaze (May 21 2022 at 05:14): 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].
Pierre Castéran (May 21 2022 at 07:10):I don't understand which lemma you want to prove.
lThe left hand side of your implication count_occ Nat.eq_dec [2;4;2;8] 2 > count_occ Nat.eq_dec [2;4;2;8] 8 reduces to 2 > 1 (just try cbn)
thus is trivially provable.
Please note also that there were syntax errors (list notations) in your question.
zohaze (May 21 2022 at 15:59):cbn works .Thanks.
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?
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: Oct 03 2023 at 04:02 UTC