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?

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.

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.

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)

which `count`

function are you using?

Can you give us the definition?

What Coq tells you when you do `About count.`

What is the supposed meaning of `(n1 n2 true false)`

? Is `n1`

a function ?

If you don't send us a correct script we can copy, replay and understand, we can't help you.

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.

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

(cf. CPDT) means?

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: Jun 18 2024 at 22:01 UTC