pianke (Jul 25 2022 at 03:54): 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" ? 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.
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? Plz give an example like above.
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. 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_decis 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 rewritedid 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.
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: Oct 13 2024 at 01:02 UTC