```
b0 : nat
b: nat
l : list nat
l1: list nat
H : length (b :: l1) > 0
IHl : count_occ Nat.eq_dec l (S k) <= S (count_occ Nat.eq_dec l 0)
Goal:
count_occ Nat.eq_dec (b0 :: l) (S k) <= S (count_occ Nat.eq_dec (b0 :: l) 0).
```

To prove above which command i should apply? At this stage count_occ Nat.eq_dec l k <=

count_occ Nat.eq_dec l 0 is also required?

Your goal is not provable: Take `l=[3]`

, `k=2`

, and `b0=3`

for instance.

Perhaps the lemma you want to prove doesn't hold, or the tactics which led to this proof state were not appropriate.

After your reply, i have made changes. I want to know given hypothesis are enough(i have only these)?

```
Require Import List Arith.
Import ListNotations.
Section Req.
Variables c k m h: nat.
Variables l1 : list nat.
Variables d : list nat.
Hypothesis H1 : h < list_max (h :: l1).
Hypothesis H2 : h > nth k l1 0.
Hypothesis H3 : c = (S k).
Hypothesis H4 : c <> 0.
Goal S(count_occ Nat.eq_dec (firstn m d) (S k)) <= count_occ Nat.eq_dec (firstn m d) 0.
```

Looks strange. You have hypotheses on a list l1 and a conclusion on another list d. Moreover, the same variable k is used in the hypotheses as an index in the list, and as an element of d in the conclusion.

I don’t think it’s a good practice to accumulate artificially so many new hypotheses. You risk to get an inconsistent context and a useless lemma when you get out the section. It would be better to start with the property of count_occ you want to prove. New hypotheses will appear naturally along the interactive proof. As we already mentioned, we cannot give many explanations if we don’t have the lemma statement and the problematic proof script.

I think it would be useful to look in library List at a few proofs of properties of count_occ, then edit your own proofs of the same and/or similar lemmas.

l1 is main list and d is locally generated list .Moreover, I am storing k in d after test condition.Therefore it appear twice. Ok,i look at library for some similar lemma. Lastly, if you don't mind just give two lines comments,plz. (To prove such statement what hypotheis i should have ?).

```
Require Import List Arith.
Import ListNotations.
Section goal.
Variables m k: nat.
Variables l1 l2 : list nat.
Hypothesis H1 :length l1 > 0.
Hypothesis H2: S k < length l1 ->
count_occ Nat.eq_dec
(firstn (S m) l2) (S k) <= count_occ Nat.eq_dec (firstn (S m) l2) 0 .
Goal
count_occ Nat.eq_dec
(0:: firstn m l2) (S k) <= count_occ Nat.eq_dec (0:: firstn m l2) 0.
```

Thank for your reply.

At first sight, `H1`

looks to be too weak for being used with `H2`

. There is little information about the roles of `l1`

and `l2`

.

But, I would prefer not to comment on subgoals without knowing by which script they were generated. In order to complete your proof, you will probably have to look at properties of `firstn`

and `count_occ`

, and have several cases to consider.

Hypothesis and goal statement both involves l2. H2 shows l2 contains greater count of 0 than (S k).

Now addition of 0 will not effect the previous relation of l2. Because count of 0 is greater and it will remain greater. Is this not enough information? If look at H2 , it has (S m) and it has been reduce to m. Actually there is addition of an element ,therefore it should be (S m)+1. Is this a problem Or from l2 which have (S m) number of element when extract first element then it would be 0 (on what basis)? Thanks.

I think `l1`

is useless in your goal. You may remove `H1`

and the hypothesis `S k <= length l1`

from `H2`

.

After removing H1 & H2,remaining hypthesises are enough to prove statement of the goal? If not , then what type of hypotheis will help me?

Not removing H2, just remove the part « S k <= length l1 -> » from H2.

Last updated: Jun 18 2024 at 22:01 UTC