Greater or less relation · Coq users

b0 : nat
b: nat
l : list nat
l1: list nat
H : length (b :: l1) > 0

IHl : count_occ Nat.eq_dec l (S k) <= S (count_occ Nat.eq_dec l 0)
Goal:
count_occ Nat.eq_dec (b0 :: l) (S k) <= S (count_occ Nat.eq_dec (b0 :: l) 0).

To prove above which command i should apply? At this stage count_occ Nat.eq_dec l k <=
count_occ Nat.eq_dec l 0 is also required?

Pierre Castéran (Jul 30 2022 at 11:08):

Your goal is not provable: Take l=[3], k=2, and b0=3 for instance.
Perhaps the lemma you want to prove doesn't hold, or the tactics which led to this proof state were not appropriate.

pianke (Jul 31 2022 at 07:57):

After your reply, i have made changes. I want to know given hypothesis are enough(i have only these)?

Require Import List Arith.
 Import ListNotations.
Section Req.
Variables c k m h: nat.
Variables l1 : list nat.
Variables d : list nat.
Hypothesis H1 : h < list_max (h :: l1).
Hypothesis H2 : h > nth k l1 0.
Hypothesis H3 : c = (S k).
Hypothesis H4 : c <> 0.
Goal S(count_occ Nat.eq_dec (firstn m d)  (S k)) <= count_occ Nat.eq_dec (firstn m d) 0.

Pierre Castéran (Jul 31 2022 at 09:12):

Looks strange. You have hypotheses on a list l1 and a conclusion on another list d. Moreover, the same variable k is used in the hypotheses as an index in the list, and as an element of d in the conclusion.

I don’t think it’s a good practice to accumulate artificially so many new hypotheses. You risk to get an inconsistent context and a useless lemma when you get out the section. It would be better to start with the property of count_occ you want to prove. New hypotheses will appear naturally along the interactive proof. As we already mentioned, we cannot give many explanations if we don’t have the lemma statement and the problematic proof script.

I think it would be useful to look in library List at a few proofs of properties of count_occ, then edit your own proofs of the same and/or similar lemmas.

pianke (Jul 31 2022 at 14:26):

l1 is main list and d is locally generated list .Moreover, I am storing k in d after test condition.Therefore it appear twice. Ok,i look at library for some similar lemma. Lastly, if you don't mind just give two lines comments,plz. (To prove such statement what hypotheis i should have ?).

Require Import List Arith.
 Import ListNotations.
 Section goal.
Variables  m k: nat.
Variables l1 l2 : list nat.
Hypothesis H1 :length l1 > 0.
Hypothesis H2: S k < length l1 ->
 count_occ Nat.eq_dec
 (firstn (S m) l2)  (S k) <= count_occ Nat.eq_dec (firstn (S m) l2)  0 .
Goal
count_occ Nat.eq_dec
  (0:: firstn m l2) (S k) <= count_occ Nat.eq_dec   (0:: firstn m l2) 0.

Pierre Castéran (Jul 31 2022 at 18:23):

At first sight, H1 looks to be too weak for being used with H2. There is little information about the roles of l1and l2.

But, I would prefer not to comment on subgoals without knowing by which script they were generated. In order to complete your proof, you will probably have to look at properties of firstnand count_occ, and have several cases to consider.

pianke (Aug 01 2022 at 17:30):

Hypothesis and goal statement both involves l2. H2 shows l2 contains greater count of 0 than (S k).
Now addition of 0 will not effect the previous relation of l2. Because count of 0 is greater and it will remain greater. Is this not enough information? If look at H2 , it has (S m) and it has been reduce to m. Actually there is addition of an element ,therefore it should be (S m)+1. Is this a problem Or from l2 which have (S m) number of element when extract first element then it would be 0 (on what basis)? Thanks.

Pierre Castéran (Aug 01 2022 at 19:34):

I think l1 is useless in your goal. You may remove H1 and the hypothesis S k <= length l1 from H2.

pianke (Aug 02 2022 at 18:09):

After removing H1 & H2,remaining hypthesises are enough to prove statement of the goal? If not , then what type of hypotheis will help me?

Stream: Coq users

Topic: Greater or less relation

pianke (Jul 30 2022 at 05:07):