How to simplify? · Coq users · Zulip Chat Archive

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?

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.

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.

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)

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.

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.

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.

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

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. https://coq.inria.fr/documentation )

zohaze (Jan 22 2023 at 12:16):

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?

Stream: Coq users

Topic: How to simplify?

zohaze (Dec 26 2022 at 19:04):