I have list

```
(b::firstn m l) ,b=k2 & b<>5
H:count_occ (b::firstn m l) k2 <= 5
Goal: S(count_occ (firstn m l) k2 <= 5
```

I am applying count_occ_cons_eq(lemma from standard lib) but it is not working.

What do you mean by "it is not working" ? Did you get an error message, for instance?

At first sight, looks like the lemma you quote could be used in rewriting in `H`

.

It is difficult to be more precise, in absence of a copy of the code which led to this issue.

Not working means when i apply above command it does not help me in closing goal statement . I want to ask when i have above hypothesis

and have relation between two terms then writing it in the form of goal statement will not disturb the previous relation. Which command i should apply to solve the statement? Plz give an example like above.

The goal you provided is not complete (e.g., the definitions of firstn and count_occ are missing).

But count_occ is certainly a recursive function which contains a "match…with", so given its argument is in constructor form, a tactic to try on this goal is:

`simpl in H.`

(after rewriting k2 to b)

However as mentioned by Pierre, a copy of the code which led to this goal would be helpful to give more precise hints.

Here is a possible correct way of asking a question.

First, you present an exact, complete copy of the declarations , definitions and goal. Then, we can copy this snippet into our favorite Coq environment, and analyse the problem.

```
Require Import List Arith.
Import ListNotations.
Section MyGoal.
Variables b k2 m : nat.
Variables l : list nat.
Hypothesis H_b_k2 : b = k2.
Hypothesis H : count_occ Nat.eq_dec (b:: firstn m l) k2 <= 5.
Goal S(count_occ Nat.eq_dec (firstn m l) k2) <= 5.
```

Note that in your post, the argument `Nat.eq_dec`

is missing, and there is a syntax error, which makes it time-consuming for us to correct errors and add missing information.

Then, it could have been easy to answer in a few seconds:

```
now rewrite count_occ_cons_eq in H.
Qed.
End MyGoal.
```

Thanks for lot of correction. But why same relation with another value give error " Tactic failure: Cannot solve this goal." like below

```
Require Import List Arith.
Import ListNotations.
Section MyGoal.
Variables b k2 m : nat.
Variables l : list nat.
Hypothesis H_b_k2 : b = (k2).
Hypothesis H_k2 : k2 > 0.
Hypothesis H_0 : b <> 0.
Hypothesis H : count_occ Nat.eq_dec (b:: firstn m l) k2 <=
count_occ Nat.eq_dec (b:: firstn m l) 0.
Goal S(count_occ Nat.eq_dec (firstn m l) k2) <=
count_occ Nat.eq_dec (firstn m l) 0.
now rewrite count_occ_cons_eq in H.
```

```
Require Import List Arith.
Import ListNotations.
Section MyGoal.
Variables k2 m : nat.
Variables l : list nat.
Hypothesis H_k2 : k2 > 0.
Hypothesis H : count_occ Nat.eq_dec ( firstn m l) k2 <=
count_occ Nat.eq_dec (firstn m l) 0.
Goal count_occ Nat.eq_dec (0:: firstn m l) k2 <=
count_occ Nat.eq_dec (0:: firstn m l) 0.
now rewrite count_occ_cons_eq in H.
```

In your first snippet, you have to apply two library lemmas (one for `H_b_k2`

, the other for `H_0`

).

```
rewrite (count_occ_cons_eq _ _ H_b_k2) in H.
now rewrite (count_occ_cons_neq _ _ H_0) in H.
```

The error came from `now`

, because the first `rewrite`

did not solve completely the sub-goal. In such situations, you may replace `now <tac>`

with `<tac>; trivial`

then complete the current sub-goal.

In your second snippet, the goal can be solved as follows:

```
destruct k2.
- inversion H_k2. (* or lia, or reflexivity *)
- cbn; now apply le_S.
```

In second case , I have replaced the H (used above) with new H and all other things ( including goal statement) remain the same. now le_S command does not close the sub goal.What could be the reason?

```
(new )Hypothesis H :
m>0 ->
(length l > 0 ->
k2 < length l ->
nth 0 l 0 > 5 ->
count_occ Nat.eq_dec ( firstn m l) k2 <= count_occ Nat.eq_dec (firstn m l) 0).
```

Perhaps it comes from the condition `m > 0`

. Is it inferable from the context ?

I'm quite lost: The hypotheses are changing too often. We don't know which lemma you want to prove yet, nor which commands led you to these goals.

Trying to guess these commands would be uselessly time-consuming, and perhaps preventing us to give the best answer.

```
Require Import List Arith.
Import ListNotations.
Section MyGoal.
Variables k2 m : nat.
Variables l : list nat.
Hypothesis H_k2 : k2 > 0.
Hypothesis H : m > 0 ->
(length l > 0 ->
k2 < length l ->
nth 0 l 0 > 5 ->
count_occ Nat.eq_dec ( firstn m l) k2 <=
count_occ Nat.eq_dec (firstn m l) 0).
Goal count_occ Nat.eq_dec (0:: firstn m l) k2 <=
count_occ Nat.eq_dec (0:: firstn m l) 0.
```

Now applying command " now rewrite count_occ_cons_eq in H." is not helpful in closing sub goal.

I have hypothesis H (including m > 0, like above). In this case why i am unable to apply "count_occ_cons_eq in H". I want to apply this command in present situation.

Plz, explain the difference between two statements.

```
1) H: S m > 0
H2: length l > 0 ->
k2 < length l ->
count_occ Nat.eq_dec (firstn (S m) l) k2 <= 5
2) m > 0 ->
length l > 0 ->
k2 < length l ->
count_occ Nat.eq_dec (firstn m l) k2 <= 5 ->
count_occ Nat.eq_dec (firstn m (a::l)) k2 <= 5
```

a k2 m are nat.

(Ref:26 july post). Reverse statement is also possible? Replace H statement with goal statement?

Last updated: Jun 14 2024 at 18:01 UTC