Stream: Coq users

Topic: How to simplify?

view this post on Zulip zohaze (Dec 26 2022 at 19:04):

I have a function f whose output is nat list l1 (n1 n2 true false) , with two nat ,two bool arguments. I have hypothesis

 count 2 ( (n1 n2 true false)  < count 3  (n1 n2 true false) .
Goal :count 2 (5:: (n1 n2 false false) ) < count 3 (5:: (n1 n2 false false) ).

Plz someone help me in solving this and clear my points
1) Addition of 5 in the list will not disturb the previous reation.Therefore it should be solve by lia. But this command is not working. What could be reason?
2) How to handle difference of input argument in l1(true in l1 and false in goal statement) ? I have to write in hypothesis, the reason of this chang?
3) Is there need of some other hypothesis to solve this?

view this post on Zulip Pierre Courtieu (Dec 26 2022 at 19:30):

Please give a complete example that we can execute.
You mention a function f but it seems your code is about function count. Without the context I think it is hard to help.

view this post on Zulip Michael Soegtrop (Dec 27 2022 at 10:29):

Your code is not standard syntax Coq (what is (a b c d)) so as Pierre already wrote it is hard to tell what it is supposed to mean. My guess is that what you are looking for is in the standard library the lemma count_occ_cons_neq. You seem to have your own count function for list like structures, so you need to prove lemmas like count_occ_cons_neq for your own count function, which should be easy. Or better use the standard library functions (which afair I already recommended quite a while back). You can replace your definition of count with one based on standard library count_occ - then you don't need to change all of your code, but still can use standard library lemmas about count_occ.

view this post on Zulip zohaze (Jan 04 2023 at 15:39):

I am using standard count function where l is natural number list. l have just replaced it with my own l (combination of natural numbers & bool). To clear my point i am giving example of standard count function & way i am using it
l:list nat
H : count 2 l < count 3 l.
Goal: count 2 (5::l) ) < count 3 (5::l)). It can be easily solve(because addition of 5 have no effect on the presence of 2 and 3) . But when i replaced l with my list,then commands which were applicable in above case ,were no more applicable here.
l: (n1 n2 true false) )
H: count 2 (n1 n2 true false) ) < count 3 (n1 n2 false false ).
Goal: count 2 (5:: (n1 n2 false false) ) < count 3 (5:: (n1 n2 false false) ).
I am asking ,every thing is same then why this problems have occured. How to remove them? Give some suggestions to solve it.(Thanks)

view this post on Zulip Laurent Théry (Jan 04 2023 at 17:29):

which countfunction are you using?
Can you give us the definition?
What Coq tells you when you do About count.

view this post on Zulip Pierre Castéran (Jan 04 2023 at 17:39):

What is the supposed meaning of (n1 n2 true false) ? Is n1a function ?
If you don't send us a correct script we can copy, replay and understand, we can't help you.

view this post on Zulip zohaze (Jan 22 2023 at 08:45):

First, lot of thanks. count from library as
Fixpoint count (v:nat) (l:list nat) : nat := match l with | [] => 0 | h :: t => (if beq_nat h v then 1 else 0) + (count v t) end.
1) I am unable / don't know how to use above given hypothesis to close the above given goal statement.
2)Every thing is same only difference lies in list input arguments,which is not purely nat argument but have nats and bool s arguments.
3)@ Pierre Casteran from standard library count n l and in my code l is list of two nat values n1 n2 and two bool values.No other function is there. As i said ,i have simple above hypothesis. List having different natural numbers and few bool values and i want to count natural numbers only. Plz some one help me from where i should start.

view this post on Zulip Pierre Castéran (Jan 22 2023 at 11:24):

Could you make precise which kind of list do you consider ?
You cannot simply mix numbers and booleans in the same list.

Fail Check [3;4;true;false].

Note that you may build a type "nat or bool" as follows:

Inductive nat_or_bool : Set :=
  num (n: nat) | boolean (b: bool).

Check [num 3; num 4; boolean true].

There is also a much more complex notion of "heterogeneous list" (cf. CPDT (*) )

Note that if you have always the same number of natural numbers and booleans (as your example suggests),
you may re-organize your data structure as a list of pairs:

Check [(3,true); (4, false)].

Once again, it's almost impossible to give a useful answer if you don't share the Coq code.

(*) Certified Programming with Dependent Types (Adam Chlipala, 2008), a textbook about practical engineering with Coq, teaches advanced practical tricks and a very specific style of proof.
(cf. )

view this post on Zulip zohaze (Jan 22 2023 at 12:16):

(cf. CPDT) means?

view this post on Zulip zohaze (Jan 22 2023 at 12:37):

I have tried list pair also. In that case output is as like (8* l).Where 8 is the number of elements in the output list,which i have separatly counted and displayed and l is heterogeneous list. I could solve now?

Last updated: Oct 04 2023 at 23:01 UTC