## Stream: Coq users

### Topic: which one is greater

#### pianke (Jul 25 2022 at 03:54):

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.

#### Pierre Castéran (Jul 25 2022 at 06:23):

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.

#### pianke (Jul 26 2022 at 13:55):

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?

#### Erik Martin-Dorel (Jul 26 2022 at 15:03):

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.

#### Pierre Castéran (Jul 26 2022 at 15:45):

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

#### pianke (Jul 26 2022 at 17:10):

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

#### pianke (Jul 26 2022 at 17:26):

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

#### Pierre Castéran (Jul 26 2022 at 17:44):

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.

#### pianke (Jul 27 2022 at 14:27):

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).
``````

#### Pierre Castéran (Jul 27 2022 at 14:51):

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.

#### pianke (Jul 28 2022 at 17:23):

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

#### pianke (Jul 28 2022 at 17:33):

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.

#### sara lee (Aug 08 2022 at 05:34):

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

Last updated: Feb 05 2023 at 22:03 UTC