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" ? At first sight, looks like the quoted lemma 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?

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. We can copy this snippet into our favorite Coq environment.

```
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 last goal, 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 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.

```
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: Feb 05 2023 at 22:03 UTC