Stream: Coq users

Topic: which one is greater


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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_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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 rewritedid not solve completely the sub-goal.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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