Problem in lemma writing · Coq users

Fixpoint num_lt (n: nat) (l: list nat) : nat :=
match l with
| nil => 0
| a::tl => if a <? n then S (num_lt n tl) else num_lt n tl
end.
Fixpoint tot_numb (grt: nat) (l: list nat) : nat :=
match grt with
| O => 0
| S z' => (num_lt grt l) + (tot_numb z' l)
end.
Compute (tot_numb 6 (6::5::nil)).
Output of tot_numb is 1 when we give 6(maximum of list) as input argument. When this number is greater than maximum(6) of list we get greater number than the previous one. I want to write some generalized lemma expressing this behaviour.

Andrey Klaus (Apr 25 2021 at 11:54):

Well, to me it looks like:
if n is greater or equal to maximum of given list and
m is greater or equal to n
then tot_numb m l >= tot_numb n l

Michael Soegtrop (Apr 25 2021 at 12:38):

Is Compute (tot_numb 10 (6::5::4::3::2::1::nil)). resulting in 39 really what you want?

I think you are approaching this from the wrong end. You should first write down what your function is supposed to do, then implement the function and then verify that the implementation fulfills this spec.

zeesha huq (Apr 26 2021 at 08:22):

zeesha huq
@ Michael ok answer is 39 . As you said write function. First I talk about function - tot_num . It simply count number of times each element of the list is less than greatest value. Then count all these numbers. Writing function detail in this way is difficult and I need two lemmas like Lemma first_l n l : In (max (n))(s:: l). Lemma snd_l n l : forall s m , (s+m=max)-> for each element of the list then add all ms.

zeesha huq (Apr 27 2021 at 04:01):

zeesha huq (Apr 27 2021 at 04:25):

zeesha huq (Apr 27 2021 at 06:34):

I can write lemma about the function num_lt as Lemma g_1 n l : forall m,
num_lt (max s l)(s::l) = m -> m number of elements <(max s l).

zeesha huq (Apr 27 2021 at 11:55):

I want to write lemma about function (tot_numb) in this way (express in english). Sum(all elements of the list)+tot_numb =max(length l). All element become same then we can take common factor in the form of max value. I have used a function which finds greatest element of the list. Here it is Fixpoint great_value (our_great : nat) (l : list nat) :=
match l with
| nil => our_great
| a :: l1 =>
if a <=? our_great then great_value our_great l1
else great_value a l1
end.

Definition grt_value l :=
match l with
| nil => 0
| a :: tl => great_value a tl
end.

Michael Soegtrop (Apr 27 2021 at 15:34):

@zeesha huq : I see. So the function is computing the sum of the differences between grt_value and the list elements (note that nat subtraction returns 0 if the result would be negative). I would consider proving this first. The lemma you want to prove follows easily from that.

zeesha huq (Apr 29 2021 at 03:40):

Thank you for your response.I am newly joining zulip. I have checked(marked) email preferences. I want to correspond via mail.Yes function returns zero because I am using nat data type.

zeesha huq (Apr 30 2021 at 17:00):

@ Michael Soegtrop . I want to link greatest value and function num_lt. I can write lemma in this way? Lemma grt_1 n l : forall a,
num_lt (a l) <= (num_lt (max a l)l). Secondly I want to compare output of tot_num function against two different inputs. What simplest lemma can be helpful?

Michael Soegtrop (Apr 30 2021 at 17:25):

Your question would be easier to answer if you would post Coq code which parses. (num_lt (max a l)l) does not parse unless you have a non standard max function since the second argument of num_lt is a list and the arguments of may are nat. You can paste a few 10 lines of code here - please code which parses in Coq as is in one piece. If it gets longer, you can put it e.g. in a github gist.

zeesha huq (May 01 2021 at 04:34):

I am using function ( great_value) mentioned above for finding greatest /max value(27-4-2021). Lemma grt_1 n l : forall a,
num_lt a (a::l) <= num_lt (max a (a::l))(a::l). It have two input arguments(one nat second list) and output argument is nat.Simply want to show that function- num_lt output value is greater when max value is given as input and its output would be less or equal when any other element of the list is given as input to this function.

zeesha huq (May 01 2021 at 07:26):

I have defined lemma like this :how to move next? Lemma num_count n l : forall e, In e (n :: l) -> num_lt e l <= num_lt(great_value n l)l.
Proof.
revert n; induction l as [ | a l' IH]. simpl; intros n e [n_eq_e | []]. auto. simpl; intros n e e_in. simpl.
destruct(a <? e) eqn:c1. simpl in *. destruct e_in as [a1 | [ a2 | a3]].

Michael Soegtrop (May 01 2021 at 18:02):

Definition great_value (our_great : nat) (l : list nat) := list_max (our_great :: l).
Definition grt_value l := list_max l.

If so, your lemma is not difficult to prove using the lemmas list_max_le and Forall_forall as follows:

Require Import Nat.
Require Import List.
Require Import Lia.

Import ListNotations.

Open Scope nat_scope.

(* counts number of elements in list l less than n *)

Fixpoint num_lt (n: nat) (l: list nat) : nat :=
match l with
| nil => 0
| a::tl => if a <? n then S (num_lt n tl) else num_lt n tl
end.

Definition great_value (our_great : nat) (l : list nat) := list_max (our_great :: l).

Definition grt_value l := list_max l.

Lemma num_lt_le: forall (n1 n2 : nat) (l : list nat),
  n1 <= n2 ->
  num_lt n1 l <= num_lt n2 l.
Proof.
  intros n1 n2 l H.
  induction l.
  - reflexivity.
  - simpl.
    destruct (PeanoNat.Nat.ltb_spec0 a n1), (PeanoNat.Nat.ltb_spec0 a n2); lia.
Qed.

Lemma num_count n l : forall e, In e (n :: l) -> num_lt e l <= num_lt(grt_value (n::l)) l.
Proof.
  intros e Hin.
  apply num_lt_le.
  apply (Forall_forall (fun k : nat => k <= list_max (n :: l)) (n::l)).
  apply (list_max_le (n :: l) (list_max (n :: l))).
  lia.
  exact Hin.
Qed.

Proving such a lemma directly with induction is really hard. As I already said, you first need to prove simpler properties of the involved functions.

Also you should avoid defining functions like great_value as recursive functions. You should try to find predefined functions for which useful lemmas are already defined and define your function as simple definition based on these. E.g. list_max is trivial to find with Search list "max"..

zeesha huq (May 02 2021 at 04:29):

I have imported these libraries Require Import Nat. Require Import List. Require Import Lia. Import ListNotations.Open Scope nat_scope I am using list_max ,but still I get the message "The reference list_max was not found in the current environment. Same message for list_max_le . I am using CoqIDE 8.8.0

Michael Soegtrop (May 02 2021 at 05:48):

I would suggest that you move on to a recent version of Coq (we are at version 8.13). Using a years old version of Coq does involve a certain amount of "reinventing the wheel". If you are stuck with 8.8 cause of compatibility with some other project I would consider investing the time to update that project to 8.13. It is well invested time. Of cause you can also prove a lemma like list_max_le for your definition of list_max, but you will find yourself in this situation more than once if you stay with 8.8. E.g. Lia is substantially weaker in 8.8 than it is in 8.13 - especially for working with nat. My above proof of num_lt_le is not likely to work in this way in 8.8 - expect much more manual work.

Please understand that I am not going to help you find a prove which works for 8.8. I personally invested a lot of time into making recent versions of Coq easy to install, so I hope installing Coq 8.13 is not what keeps you from using it.

A last thought on this: the project you are working on is doomed to bit rot if you start out with 8.8.

zeesha huq (May 02 2021 at 07:07):

Thank you. Is it possible to have both versions(8.8 &8.13) at same time in PC ? Secondly I want to compare output of tot_num function against two different inputs( maximum value of the list & any other value of the list). What simplest lemma could be helpful? If I write lemma from this statement [ Sum(all elements of the list)+tot_numb =max(length l)]It would be helpful? In this way all element become same then we can take common factor in the form of max value . You said about this function-grt_value(27-april) "that note that nat subtraction returns 0 if the result would be negative". I have proved this but how to connect it with our required lemma which is about the sum of the differences between grt_value and the list elements.

Stefan Wils (May 02 2021 at 07:15):

With OPAM switches, you should be able to get a different version of Coq per project. Not sure about PC, but I’d say it works?

Michael Soegtrop (May 02 2021 at 08:04):

@zeesha huq : as Stefan mentioned, you can create independent switches with the opam switch command and install different Coq versions in each switch. If you install Coq Platform (https://github.com/coq/platform) the scripts will automatically create a new opam switch for Coq 8.13. You can have different switches active in different shells using eval $(opam config env --switch <switch-name>).

In the near future I want to support old Coq versions in Coq platform especially for the purpose of porting old Coq developments.

Definition tot_numb_alt (grt: nat) (l: list nat) := list_sum (map (fun x => grt-x) l).

Lemma tot_numb_alt_eq : forall (n : nat) (l : list nat),
  tot_numb n l = tot_numb_alt n l.

This might be tricky to prove immediately because tot_numb would need an induction over n while tot_numb_alt needs an induction over l. This is exactly the reason why I would do such an alternate definition, so that you can switch definitions depending on what induction other parts in some proof prefer. To prove this easily, you might need a helper lemma which shows what happens with tot_numb if you add one element to the front of a list. And I think for that you might need another helper lemma which tells what happens with tot_numb if n is increased by one. In general: if you try to prove this and come across something you need during your induction step which is not obvious (or not obvious how to prove), don't try to prove it inline, but make an extra lemma out of it. In case your proof doesn't work out as expected, you at least have this helper lemma then which might still be useful and also give you insight into what proofs might work. If you try to do "all in one" proofs, you keep redoing the same proof steps again and again.

Michael Soegtrop (May 02 2021 at 08:08):

Of cause it might also work for you to use upfront definitions of your functions, which are easier to work with. E.g. functions over lists like tot_numb where even the empty list case does not simplify might be more tricky to work with than other definitions. But then if you usually need induction over n in your proofs, your definition might be the right choice.

Michael Soegtrop (May 02 2021 at 08:12):

Also when you use definitions based on map and foldr (as list_max and list_sum), you have plenty of generic lemmas about foldr and map. If you write your own recursive functions for everything, you have to prove every little lemma yourself.

zeesha huq (May 02 2021 at 08:47):

I have few other lemmas that have been proved by function-great_value.When I replaced it with list_max. All lemmas get distrub.This is because of arguments differences in both functions. Is it possible first I use function great_value for all previous lemmas. When move for proving lemma (Lemma num_count n l : forall e, In e (n :: l) -> num_lt e l <= num_lt(grt_value (n::l)) l).Then use above two definition of equality.Use list_max for lemma(num_count.) ? But error message occurs that this function is already used.

Michael Soegtrop (May 02 2021 at 16:03):

You can't redefine a function or lemma. If you want to have the same lemma for two different implementations of the same function, the lemma must have a different name.

zeesha huq (May 05 2021 at 07:49):

Now talk about function-tot_numb. These two lemmas are ok? If we provide nat argument equal to or greater than great_value then it has no effect on the output of tot_numb else it gives greater nat value at the output. Definition add (v:nat) (l:list nat) : list nat := v :: s. Lemma our_values_1: forall (a b n:nat)(l:list nat),
a>=(great_value n l) -> tot_numb (great_value n l) l = tot_numb (great_value n l)(add a l)-> a < (great_value n l) ->tot_numb (great_value n l) l < tot_numb (great_value n l)(add a l).
Second - Lemma our_values_2 : forall (a n:nat)(l:list nat), a>=(great_value n l) ->
tot_numb (great_value n l) l = tot_numb (great_value n l)(add (a+1) l).

Michael Soegtrop (May 05 2021 at 08:21):

@zeesha huq : please user verbatim mode to post code - it is unreadable as is. Verbatim mode starts and ends with three back ticks in a separate line ```.

Your lemma our_values_1 is useless since it has contradicting hypothesis - you could never apply it because you can never full both a>=b and a<b. I guess you wanted 2 separate lemmas.

I am not sure what you mean with OK. Provable? Formulated in a way which will be useful? I honestly think you should try to answer these questions yourself and come back with more concrete questions about Coq.

zeesha huq (May 07 2021 at 02:41):

Definition add (v:nat) (l:list nat) : list nat := v :: s.

Lemma our_values_1: forall (a n:nat)(l:list nat),
a < (great_value n l) ->
tot_numb (great_value n l) l < tot_numb (great_value n l)(add a l). ``` . I mean this lemma statement is provable. Change in this variable effects the output of the function.

Michael Soegtrop (May 07 2021 at 06:58):

@zeesha huq : if you are unsure if the lemma is provable, I would suggest that you first try it with a few examples. A quick way of doing this would be:

Example Test1:
  let a := 2 in
  let n := 3 in
  let l := [1; 2] in
  (a < (great_value n l)) -> tot_numb (great_value n l) l < tot_numb (great_value n l)(add a l).
Proof. cbv; easy. Qed.

Play with the numbers and see if the special case proof goes through (easy should be able to handle also cases where the premise does not hold). There is also a Coq plugin called QuickChick which allows automated randomized generation of counter examples. It is a bit of effort to set it up for specific cases, but for lists of nats it should be easy. See (https://github.com/QuickChick/QuickChick).

Btw.: there is a preview button (the eye directly below the edit field) which let's you check if you got the formatting right before you post something. It is good practice to use it before every post.

zeesha huq (May 08 2021 at 06:41):

Thank you. I have not checked the output of function in this way.But before writing helping lemma , I have checked the output against different numbers by first writing with pen on paper then cross check it with the output of function . As you suggested both lemma statements(our_values_1 & our_values_2... May 05) get executed . After unfolding the function, easy command automatically check each case statement?Next time I will use Btw command. Now actual statement of lemma is : tot_numb n l = tot_numb_alt n l)(2 May). To prove this you said first prove tot_numb is zero for value equal to zero or less than zero ( Lemma tot_num_0 : forall (n:nat)(l:list nat),
n <= 0 ->tot_numb(n) l =0). I have done this. What do next?

Michael Soegtrop (May 09 2021 at 15:34):

As you already wrote: try to prove tot_numb n l = tot_numb_alt n l. What you already have proven should be helpful for that.

zeesha huq (May 22 2021 at 07:05):

To solve above I have reached upto this point.
Lemma our_values_2: forall (v a:nat)(l:list nat),
v > (grt_value (a::l)) ->
tot_numb (grt_value (a::l)) l < tot_numb v (a::l).
Proof.
intros. unfold grt_value.
destruct (Nat.eq_dec (great_value a l)0).
rewrite e. simpl in *. destruct v. lia.
simpl in *. destruct (a <? S v) eqn:cmp.
lia.
Admitted.
Lemma our_values_1: forall (v :nat)(l:list nat),
v < (grt_value l) ->
tot_numb (grt_value l) l < tot_numb (grt_value l)(add v l).
Proof.
intros. unfold grt_value.
induction l. inversion H. simpl in *.
destruct (Nat.eq_dec (great_value a l)0).
rewrite e . simpl. lia. simpl in *.
Admitted.

Definition list_sum l := fold_right plus 0 l.

Definition tot_numb_alt (n: nat) (l: list nat) :=
list_sum (map (fun x => (grt_value l)-x) l).

Lemma tot_numb_alt_eq : forall (n a: nat) (l : list nat),
tot_numb n (a::l) = tot_numb_alt n (a::l).
Proof.
intros. unfold tot_numb_alt.
unfold list_sum. unfold grt_value.
simpl in *. induction l as [|x l IH]; simpl.

Michael Soegtrop (May 25 2021 at 07:45):

@zeesha huq : you changed the definition of tot_num_alt to something where the lemma doesn't hold any more, as this example shows:

Example Test:
  let n:=3 in
  let a := 2 in
  let l := [1;2] in
  tot_numb n (a::l) = tot_numb_alt n (a::l).
  cbv.

Definition tot_numb_alt (grt: nat) (l: list nat) := list_sum (map (fun x => grt-x) l).

this does work. So in short you are stuck because you want to prove something which is wrong. As I said before, it does make sense to test a lemma at a few cases before you try to prove it.

Please use verbatim mode (three back quotes), use the Preview button before you post something and post complete code - you can't expect people to pick together stuff from a month long discussion and even if they do so, chances are good that they end up with something different than you have. This might be the case here - possibly some of your other definitions changed as well, so that your new tot_numb_alt is consistent with them. As I said before, you should put this in a github gist - you can edit it there. See (https://gist.github.com).

zeesha huq (May 27 2021 at 02:34):

three back quotes at the start and at the end of each line or just at the start or at the end of code? Like this "'lemma ........................lemma2........"'.Secondly background colour changes after verbatim mode?

Paolo Giarrusso (May 27 2021 at 06:24):

three back quotes at the start and end, on a separate line. Having a (slightly) different background is intended, since it's necessary for readability.

zeesha huq (May 27 2021 at 15:58):

zeesha huq (May 27 2021 at 16:03):

Paolo Giarrusso (May 27 2021 at 17:24):

those are ticks ', not backticks. You can google "how to type backtick" (depends on your keyboard and OS, I can't tell you).

zeesha huq (May 28 2021 at 06:05):

zeesha huq (May 28 2021 at 06:13):

Michael Soegtrop (May 28 2021 at 07:34):

@zeesha huq : it is just one set of three back quotes in a single line at the begin and end of a block of verbatim code.

As I said before, please create a github gist, where you post complete code which compiles to the point you ask a question about. I assembled your distributed pieces now more than 10 times and won't do so again, first because this takes a considerable amount of time but also because this starts to lead to errors because you change definitions and it is unclear which definition you use. You can also post code here if it is not more than 100 lines - but then please three backquotes in a single line before and after the block of code and code which compiles as is - including Require statements and everything.

zeesha huq (May 28 2021 at 13:51):

In above code I have used three back quotes , now it is in right format? Secondly code is below 100 lines, therefore I can post here. Thank you.

Michael Soegtrop (May 28 2021 at 17:01):

@zeesha huq : again: please use a single line with three backquotes, then a block (several lines of code) then another line with three backquotes. Don't use backquotes on each line!

The code is below 100 lines, but it does not compile as is. You expect people to find Require statements and all sorts of Definitions from posts you did over a long time. You can't expect anyone on the forum to spend as much time on your questions as you do. I won't answer any questions on code which does not compile in coq up to the proof you are interested in.

Gaëtan Gilbert (May 28 2021 at 17:22):

zeesha huq (May 29 2021 at 05:12):

Require Import Nat.
Require Import Lia.
Require Import Coq.Init.Tactics.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Arith.Arith.
Require Import PeanoNat.
Require Import List Arith.
Import ListNotations.


Fixpoint great_value (our_great : nat) (l : list nat) :=
match l with
| nil => our_great
| a :: l1 =>
if a <=? our_great then great_value our_great l1
else great_value a l1
end.

Definition grt_value l :=
match l with
| nil => 0
| a :: tl => great_value a tl
end.

Fixpoint num_lt (n: nat) (l: list nat) : nat :=
 match l with
 |  nil => 0
 | a::tl => if a <? n then S (num_lt n tl) else num_lt n tl
 end.

Fixpoint tot_numb (grt: nat) (l: list nat) : nat :=
 match grt with
 | O => 0
 | S z' => (num_lt grt l) + (tot_numb z' l)
 end.

Definition add (v:nat) (l:list nat) : list nat := v :: l.

Lemma tot_num_1: forall (n a:nat)(l:list nat),
a<n ->
0<tot_numb n [a].
Proof.
intros. destruct n. lia.  simpl in *.
destruct (a <? S n). simpl in *. lia.
simpl . unfold tot_numb.
Admitted.

Lemma tot_numb_values_1: forall (n a:nat)(l:list nat),
(a < (great_value n l)) ->
tot_numb (great_value n l) l < tot_numb (great_value n l)(add a l).
Proof.
intros.
induction l. unfold add. simpl in *.
Admitted.

Definition list_sum l := fold_right plus 0 l.

Definition tot_numb_alt (grt: nat) (l: list nat) :=
list_sum (map (fun x => grt-x) l).

Lemma tot_numb_alt_eq : forall (n a: nat) (l : list nat),
 tot_numb n l = tot_numb_alt n l.
Proof.
intros. unfold tot_numb_alt.
unfold list_sum.
  induction l as [|x l IH]; simpl. destruct n.
simpl. auto. simpl. unfold tot_numb.

Michael Soegtrop (May 29 2021 at 07:04):

@zeesha huq : I only prved the last lemma - I hope this shows you how to approach this. As I already said on stack overflow, if your lemma gets to complicated, proof pieces in a separate lemma.

Require Import Nat.
Require Import Lia.
Require Import Coq.Init.Tactics.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Arith.Arith.
Require Import PeanoNat.
Require Import List Arith.
Import ListNotations.


Fixpoint great_value (our_great : nat) (l : list nat) :=
match l with
| nil => our_great
| a :: l1 =>
if a <=? our_great then great_value our_great l1
else great_value a l1
end.

Definition grt_value l :=
match l with
| nil => 0
| a :: tl => great_value a tl
end.

Fixpoint num_lt (n: nat) (l: list nat) : nat :=
 match l with
 |  nil => 0
 | a::tl => if a <? n then S (num_lt n tl) else num_lt n tl
 end.

Fixpoint tot_numb (grt: nat) (l: list nat) : nat :=
 match grt with
 | O => 0
 | S z' => (num_lt grt l) + (tot_numb z' l)
 end.

Definition add (v:nat) (l:list nat) : list nat := v :: l.

(** ** Lemmas about num_lt *)

Lemma num_lt_cons: forall (n a : nat) (l : list nat),
  num_lt n (a :: l) = num_lt n l + (if a <? n then 1 else 0).
Proof.
  intros n a l.
  simpl.
  destruct (a <? n); lia.
Qed.

(** ** Lemmas about tot_numb *)

Lemma tot_numb_empty: forall (n : nat),
  tot_numb n [] = 0.
Proof.
  induction n.
  - reflexivity.
  - cbn. apply IHn.
Qed.

Lemma tot_numb_succ: forall (n: nat) (l : list nat),
  tot_numb (S n) l = tot_numb n l + num_lt (S n) l.
Proof.
  intros n l.
  cbn.
  lia.
Qed.

Lemma tot_numb_cons: forall (n a: nat) (l : list nat),
  tot_numb n (a::l) = tot_numb n l + (n-a).
Proof.
  intros n a l.
  induction n.
  - reflexivity.
  - rewrite! tot_numb_succ. rewrite IHn.
    rewrite num_lt_cons.
    (* Note: the (if ...) on the left side is compensated by the (S n - a) vs (n - a)
       Nat subtraction needs to get used to ... *)
    destruct (Nat.ltb_spec0 a (S n)); lia.
Qed.

(** ** Alternative formulation of tot_numb, which allows induction over l (rather than n) *)

Definition list_sum l := fold_right plus 0 l.

Definition tot_numb_alt (grt: nat) (l: list nat) :=
  list_sum (map (fun x => grt-x) l).

Lemma tot_numb_alt_eq : forall (n : nat) (l : list nat),
 tot_numb n l = tot_numb_alt n l.
Proof.
  intros n l.
  induction l as [|x l IH].
  - cbn. rewrite tot_numb_empty. reflexivity.
  - rewrite tot_numb_cons, IH.
    unfold tot_numb_alt. simpl. ring.
Qed.

Michael Soegtrop (May 29 2021 at 07:19):

P.S.: just to remind you of the purpose of the lemma tot_numb_alt_eq: in cases you want to prove something which is more naturally done by induction over the list rather than n, you can now rewrite tot_numb with tot_numb_alt, which is much easier to handle in inductions over the list. It might also be that the lemma tot_numb_cons is good enough for such cases. The bottom line is: prove some small lemmas about your functions, which are useful in proves and also convince you that the functions compute what you want. E.g. I find the tot_numb_alt definition much easier to understand than tot_numb, but this might depend on the context. Such alternative definitions make both, proofs and discussions easier.

zeesha huq (May 29 2021 at 17:05):

Thank you so much. I know rewrite <- & rewrite -> command. What is the meaning of rewrite! & ring command? Actually I want to write a lemma about tot_numb , which may be helpful in finding/comparing/deciding smaller and bigger
element of list OR linking grt-value(greatest value)and tot_numb. I can write lemma which says
sum l + tot_numb = grt-value(length l)?
Compute (tot_numb 6 (6::4::nil)). (Ans 2)

Michael Soegtrop (May 30 2021 at 05:31):

If you want to know what a tactic or tactic variant does, you should first look into the reference manual (https://coq.inria.fr/refman/). At the left side bottom click on "Indexes", then "Tactic index" then the start letter at the top, say "r" and then ring or rewrite.

Sorry, I don't understand your English description, e.g. what is 10 +2=6(2). supposed to mean? Please write the lemma statement in Coq rather than describing it in English. If you don't change any of the existing definitions, it is ok to just post the part which I need to append to my latest post.

zeesha huq (May 30 2021 at 19:25):

Lemma list_sum_tot_num : forall l,
l<>nil ->
plus (list_sum l)(tot_numb (grt_value l) l)= (grt_value l) *(length l).

zeesha huq (May 31 2021 at 03:48):

Actually I want to write lemma about tot_numb & grt_value. There may be any another lemma that help in this situation.

zeesha huq (May 31 2021 at 03:56):

Michael Soegtrop (May 31 2021 at 09:24):

@zeesha huq : first I would replace your function grt_value with the standard library function list_max. As far as I can tell this is what it computes. You seem to have a tendency to find complicated definitions for simple functions, which doesn't make it easier to prove something about them. You really need to work on finding simple definitions before you try to prove something about them.

Lemma list_sum_tot_num : forall (l : list nat) (n : nat),
  n >= list_max l ->
  (list_sum l) + (tot_numb n l) = (length l) * n.

because n does not vary over the induction, while list_max n does. Your lemma easily follows from it, since you can just instantiate it with n = list_max l. It might be counter intuitive but it is common that more general lemmas are easier to prove than more specific lemmas. The reason is that e.g. in this case, the more general lemma is simpler than the more specific lemma - it replaces the complicated function list_max l in two places with just an opaque number.

zeesha huq (Jun 02 2021 at 01:44):

One more question. Would you think this lemma will help us in finding (less or equal ) relation between two elements of list.

zeesha huq (Jun 03 2021 at 17:11):

Definition list_sum l := fold_right plus 0 l.
Definition list_max l := fold_right max 0 l.

Fixpoint num_lt (n: nat) (l: list nat) : nat :=
 match l with
 |  nil => 0
 | a::tl => if a <? n then S (num_lt n tl) else num_lt n tl
 end.

Fixpoint tot_numb (grt: nat) (l: list nat) : nat :=
 match grt with
 | O => 0
 | S z' => (num_lt grt l) + (tot_numb z' l)
 end.

Lemma tot_numb_empty: forall (n : nat),
  tot_numb n [] = 0.
Proof.
  induction n. simpl.  reflexivity. cbn. apply IHn.
Qed.
Lemma tot_numb_succ: forall (n: nat) (l : list nat),
  tot_numb (S n) l = tot_numb n l + num_lt (S n) l.
Proof.
  intros n l. cbn. lia.
Qed.
Lemma num_lt_cons: forall (n a : nat) (l : list nat),
  num_lt n (a :: l) = num_lt n l + (if a <? n then 1 else 0).
Proof.
  intros n a l. simpl. destruct (a <? n). lia. lia.
Qed.

Lemma tot_numb_cons: forall (n a: nat) (l : list nat),
  tot_numb n (a::l) = tot_numb n l + (n-a).
Proof.
  intros n a l. induction n. simpl.  reflexivity.
  rewrite! tot_numb_succ. rewrite IHn. rewrite num_lt_cons.
    destruct (Nat.ltb_spec0 a (S n)). lia. lia.
Qed.

Definition tot_numb_alt (grt: nat) (l: list nat) :=
  list_sum (map (fun x => grt-x) l).

Lemma tot_numb_alt_eq : forall (n : nat) (l : list nat),
 tot_numb n l = tot_numb_alt n l.
Proof.
 Admitted.

Lemma list_maxi_le : forall l n,
list_max l <= n <-> Forall (fun k => k <= n) l.
Proof.
intro l; induction l as [|a l IHl]; simpl; intros n; split.
- now intros.
- intros. now apply Nat.le_0_l.
- intros [? ?] %Nat.max_lub_iff. now constructor; [|apply IHl].
- intros H. apply Nat.max_lub_iff.
Admitted.

Lemma list_sum_tot_num : forall (l : list nat) (n : nat),
  n >= list_max l ->
  (list_sum l) + (tot_numb n l) = (length l) * n.
Proof.
intros. induction l as [ |a l]. simpl.
apply tot_numb_empty.
rewrite tot_numb_cons.
rewrite  tot_numb_alt_eq.
simpl. unfold tot_numb_alt. unfold list_sum.

Michael Soegtrop (Jun 05 2021 at 13:07):

Sorry, I don't understand where you want to go to. There is a standard library lemma list_max_le with the statement you want. If you want to see how to prove it, you can look at the proof in the standard library.

zeesha huq (Jun 06 2021 at 05:35):

First,I am unable to add lemma ( list_max_le) in my code,might be version difference.Therefore I am copying the definition of list_max_le from standard lib to my file. Problem occurs when I execute last line of this function(exact (Forall_inv_tail H. Although I have added the this definition/lemma also).Secondly , goal is to prove lemma of 31May. To prove this you said start with n = list_max l. You mean reverse order of this function( Forall (fun k => k <= n) l -> list_max l <= n). That is why I am talking about the proof of this function. Third to prove the lemma I can use alternate definition tot_numb_alt(As I used in above code).

zeesha huq (Jun 06 2021 at 12:30):

If I donot use alternate definition of tot_numb function(tot_numb_alt), then I can solve lemma in this way?

Require Import Nat.
Require Import Lia.
Require Import List Arith.
Import ListNotations.

Fixpoint num_lt (n: nat) (l: list nat) : nat :=
 match l with
 |  nil => 0
 | a::tl => if a <? n then S (num_lt n tl) else num_lt n tl
 end.

Fixpoint tot_numb (grt: nat) (l: list nat) : nat :=
 match grt with
 | O => 0
 | S z' => (num_lt grt l) + (tot_numb z' l)
 end.

Lemma tot_numb_cons: forall (n a: nat) (l : list nat),
  tot_numb n (a::l) = tot_numb n l + (n-a).
Proof.
Admitted.
Lemma tot_numb_empty: forall (n : nat),
  tot_numb n [] = 0.
Proof.
  induction n.
  - simpl.  reflexivity.
  - cbn. apply IHn.
Qed.

Lemma list_Sn : forall (n : nat),
  tot_numb (S n) [] = 0.
Proof.
intros. simpl in *. apply tot_numb_empty.
Qed.

Definition list_max l := fold_right max 0 l.
Definition list_sum l := fold_right plus 0 l.

Lemma list_sum_tot_num : forall (l : list nat) (n : nat),
  n >= list_max l ->
  (list_sum l) + (tot_numb n l) = (length l) * n.
Proof.
intros.
 induction l. simpl. induction n. simpl. auto.
apply list_Sn. simpl in *. rewrite tot_numb_cons.
rewrite <- IHl.  lia.

zeesha huq (Jun 07 2021 at 03:45):

Require Import List Arith.
Import ListNotations.

Definition list_max l := fold_right max 0 l.
Lemma list_maxi_le : forall l n,
list_max l <= n <-> Forall (fun k => k <= n) l.
Proof.
intro l; induction l as [|a l IHl]; simpl; intros n; split.
- now intros.
- intros. now apply Nat.le_0_l.
- intros [? ?] %Nat.max_lub_iff.  now constructor; [|apply IHl].
- intros H. apply Nat.max_lub_iff.
constructor; [exact (Forall_inv H)|apply IHl].
rewrite <- IHl.

Olivier Laurent (Jun 07 2021 at 06:37):

The last rewrite <- IHl is somehow contradicting apply IHl just above. So you can conclude by replacing this last rewrite <- IHl by now inversion H.

zeesha huq (Jun 08 2021 at 11:36):

Sorry for stupid question,but I want to clear the difference between following two statements

list_max l <= n .
n <=list_max l

zeesha huq (Jun 08 2021 at 11:39):

All elements in the list can be less or equal to the list_max. But no value can be greater than list_max.Then why following lemma holds. What is its meaning? When we should use it? This lemma hold only equal relation(true). Then why we write <= relation instead of = only. If greatest value present at the head of list ,then we can apply it ?

Lemma list_le : forall l n,
Forall (fun k => k <= n) l->
list_max l <= n .

Olivier Laurent (Jun 08 2021 at 11:49):

The statement forall l n, Forall (fun k => k <= n) l -> list_max l <= n says that: if all elements of the list l are smaller or equal to a given value n then list_max l as well.
It looks reasonable: assume you want to prove list_max [4; 1; 3] <= 6, it is sufficient to prove 4 <= 6, 1 <= 6 and 3 <= 6.

zeesha huq (Jun 08 2021 at 11:54):

Olivier Laurent (Jun 08 2021 at 11:56):

Nothing in the statement mentions that n should be in the list. But it can... and even 8 could (but then the assumption Forall (fun k => k <= 6) l would not hold...).

zeesha huq (Jun 08 2021 at 11:59):

zeesha huq (Jun 08 2021 at 12:08):

It means that If i want to prove ( list_max l <= n) then (forall l n, Forall (fun k => k <= n) l) should be in hypothesis. Instead of this hypothesis I have this one (H : max a (list_max l) <= n). Now I can prove

Lemma list_maximum : forall (l : list nat) (n a: nat),
  max a (list_max l) <= n->
   list_max l <= n.

Olivier Laurent (Jun 08 2021 at 12:30):

NO, just Forall (fun k => k <= n) l).
In the discussed statement parentheses are: forall l n, (Forall (fun k => k <= n) l -> list_max l <= n).

Olivier Laurent (Jun 08 2021 at 12:33):

This lemma has nothing to do with lists and is just an instance of PeanoNat.Nat.max_lub_r : forall n m p : nat, Nat.max n m <= p -> m <= p.

zeesha huq (Jun 08 2021 at 12:35):

I can find the proof of this in standard library.(not in the form of if and only if)

Olivier Laurent (Jun 08 2021 at 12:35):

zeesha huq (Jun 08 2021 at 12:37):

Michael Soegtrop (Jun 08 2021 at 12:41):

You can use the <-> variant with apply and most other tactics. Coq will pick the right direction automatically. There is also a apply -> and apply <- to choose a direction, but I am not sure if Coq 8.8 behaved the same.
Worst case you can trivially prove the one directional lemma from the <-> lemma, e.g. with tauto.

zeesha huq (Jun 08 2021 at 12:48):

@ Michael Soegtrop. This question is related to the question of 6 June 17:30. Last line of the code.

Olivier Laurent (Jun 08 2021 at 12:55):

list_max has been introduced in Coq 8.12. The proof of list_max_le is here. As mentioned by Michael, you can easily apply it even if you do not need <->.
If you want to integrate a proof to a Coq 8.8 development, you can use:

From Coq Require Import List PeanoNat.

Definition list_max l := fold_right max 0 l.

Lemma list_max_le : forall l n,
  Forall (fun k => k <= n) l -> list_max l <= n.
Proof.
  intro l; induction l as [|a l IHl]; cbn; intros n HF.
  - now apply Nat.le_0_l.
  - inversion_clear HF.
    apply Nat.max_lub_iff; intuition.
Qed.

Michael Soegtrop (Jun 08 2021 at 13:05):

@zeesha huq : well @Olivier Laurent already answered this question. You did an apply IHl just before. The rewrite undoes it. You can rewrite hence and forth as many times as you want, but it won't bring you forward.

Your goal at this point is Forall (fun k : nat => k <= n) l which is part of H : Forall (fun k : nat => k <= n) (a :: l). As Olivier explained, you can do inversion H to separate the case for a and l and then the goal follows trivially by assumption.

zeesha huq (Jun 08 2021 at 13:05):

zeesha huq (Jun 08 2021 at 13:27):

Lemma list_sum_tot_num : forall (l : list nat) (n : nat),
  n >= list_max l ->
  (list_sum l) + (tot_numb n l) = (length l) * n.
Proof.
intros.
 induction l. simpl. induction n. simpl. auto.
apply list_Sn. simpl in *. rewrite tot_numb_cons.
rewrite <- IHl.  lia. eauto.
assert(Forall (fun k => k <= n) l -> list_max l <= n).
 { apply list_max_le. }
apply H0.

zeesha huq (Jun 09 2021 at 03:20):

zeesha huq (Jun 09 2021 at 04:23):

Lemma max_In : forall (l : list nat) (n : nat),
forall e, In e l ->
e <= list_max l.
Proof.
intros. apply (Forall_forall (fun k : nat => k <= (list_max l)) l).
apply (list_max_le l (list_max l)). auto. apply H.
Qed.

zeesha huq (Jun 10 2021 at 11:32):

In order to prove a lemma ,I have written lemmas related to its different functions.But I don't know how to relate them.Because order is also important. What sequence is helpful,means first write lemmas related to inner most function then outer one....till last.How it came to know that I am in write direction.

Michael Soegtrop (Jun 10 2021 at 12:16):

You should think what you need to try your top level lemmas (or try to prove it). Then you see what auxiliary lemmas you need. Then you prove these, which in turn might require additional lemmas. When you are stuck in a proof, think what would help you to get forward and prove that. If things get too complicated it also makes sense to start bottom up and see what you can prove, and then build on that.

zeesha huq (Jun 11 2021 at 07:19):

I want to prove the following goal, (grt l) gives greatest value of l and values_out is another function. I struck here I don't know
how to simplify it more. I want to apply these lemmas to simplify it but error occurs. How i can apply thes lemma and simplify
it any more ?.

Lemma tot_numb_cons: forall (n a: nat) (l : list nat),
  tot_numb n (a::l) = tot_numb n l + (n-a).

Lemma tot_numb_succ: forall (n: nat) (l : list nat),
  tot_numb (S n) l = tot_numb n l + num_lt (S n) l.

count_occ Nat.eq_dec
(1 ::2:: values_out false  true 0 (grt l) 1
(num_lt(S(grt l + choc)) l +
tot_numb (grt l + choc)(a :: l))
(S choc) (a :: l)) z2 <
count_occ Nat.eq_dec
(1 ::2::values_out false true 0 (grt l) 1
(num_lt(S(grt l + choc)) l +
tot_numb (grt l + choc)(a :: l))
(S choc) (a :: l)) z1.

 (* After applying tot_numb_cons *)

count_occ Nat.eq_dec
(1 ::2:: values_out false true 0 (grt l) 1
(num_lt(S(grt l + choc)) l +
tot_numb (grt l + choc)l + (grt l + choc-a))
(S choc) (a :: l)) z2 <
count_occ Nat.eq_dec
(1 ::2:: values_out false true 0 (grt l) 1
(num_lt(S(grt l + choc)) l +
tot_numb (grt l + choc)l + (grt l + choc-a))
(S choc) (a :: l)) z1.

 (* After applying tot_numb_succ *)

count_occ Nat.eq_dec
(1 :: 2::values_out false true 0 (grt l) 1
(tot_numb (S (grt l + choc)) l +(grt l + choc-a))
(S choc) (a :: l)) z2 <
count_occ Nat.eq_dec
(1 :: 2::values_out false true 0 (grt l) 1
(tot_numb (S (grt l + choc)) l +(grt l + choc-a))
(S choc) (a :: l)) z1.

 Lemma num_count n l : forall e, In e (n :: l) ->
num_lt e l <= num_lt(grt (n::l)) l.
Above lemma may be helpful when I have hypothesis that n1 < n2.

Olivier Laurent (Jun 11 2021 at 08:24):

@zeesha huq This does not seem to be valid Coq code. As already suggested, if you want people to be able to help, you should provide complete valid Coq code (including Require).
Note also that Coq code is best pretty-printed in the chat if you use ```coq rather than just ``` at the beginning of your code.

Michael Soegtrop (Jun 11 2021 at 09:34):

zeesha huq (Jun 12 2021 at 05:41):

Thank you. Feel the difference in the above code(after applying ```coq )? Now its ok ? I need next command to simplify the code. Code is lengthy that is why I have selected goal (to be prove) only. May I share complete file in private message as attached file? I know only this(simplest way). Is any other? I am new one, currently learning how to chat on zulip,therefore I don't want to go towards github . Secondly, function will be simplify if number of used functions get reduce. In above tot_num & num_lt reduce to tot_num. Now need another lemma which link values_out and tot_num . Give output in the form of one function? Third these two hypothese can be prove contradictory?

H1 : nth 0 (a::l) 0 <  nth (S z1) (a::l) 0
H3 : list_max l <= nth 0 (a::l) 0

Olivier Laurent (Jun 12 2021 at 07:57):

From Coq Require Import List Lia.

Goal forall a l z1,
  nth 0 (a::l) 0 <  nth (S z1) (a::l) 0 ->
  list_max l <= nth 0 (a::l) 0 -> False.
Proof.
intros a l z1 H1 H3; cbn in H1, H3.
enough (nth z1 l 0 <= list_max l) by lia; clear.
revert z1; induction l; intros [|z1]; cbn; [lia|lia|lia|].
specialize (IHl z1); fold (list_max l); lia.
Qed.

zeesha huq (Jun 12 2021 at 12:03):

No reply for second question.If it takes lot of time then discard my request. Atleast I will get some hint
These hypotheses may be helpful in proceding or linking with lemma based on list_max l <= n. I struct here,I don't know what lemma will help me. Simply greatest value at head location of list

H1 : a <= list_max l
H2: list_max l <= nth 0 (a::l) 0.

Olivier Laurent (Jun 13 2021 at 08:31):

count_occ Nat.eq_dec
(1 :: 2::values_out false true 0 (grt l) 1
(tot_numb (S (grt l + choc)) l +(grt l + choc-a))
(S choc) (a :: l)) z2 <
count_occ Nat.eq_dec
(1 :: 2::values_out false true 0 (grt l) 1
(tot_numb (S (grt l + choc)) l +(grt l + choc-a))
(S choc) (a :: l)) z1

which looks like count_occ Nat.eq_dec L z2 < count_occ Nat.eq_dec L z1 for a given L and is in general false since for example you could have z1 = z2.

H1 : a <= list_max l
H2 : list_max l <= nth 0 (a::l) 0.

they are equivalent to a = list_max l, but this does not tell us what you would like to do with them.
As mentioned before:
Michael Soegtrop said:

zeesha huq (Jun 13 2021 at 16:41):

acount_occ Nat.eq_dec L z2 < count_occ Nat.eq_dec L z1 .....false for z1=z2. These (z1 &z2) are list indexes . I have defined no constraint on indexes but have constraints on values(nth z2 l 0 <nth z1 l 0) and greatest value of list.

zeesha huq (Jun 13 2021 at 17:18):

Lemma count_elem_1: forall (n1 n2 : nat) (l : list nat),
  n1 <= n2 ->
  num_lt n1 l <= num_lt n2 l.

Lemma count_elem_2 n l : forall e, In e (n :: l) ->
num_lt e l <= num_lt( list_maxs (n::l)) l.

zeesha huq (Jun 15 2021 at 04:31):

Michael Soegtrop (Jun 15 2021 at 06:46):

Sorry your English description is very hard to understand and for most people here it is at least 10x more effort to read it than Coq. As explained many times, it is very time consuming to help you if you don't post code which compiles to the point of your question and I won't answer any question which is posted in another form any more.

zeesha huq (Jun 15 2021 at 13:58):

Matthieu Sozeau (Jun 16 2021 at 09:03):

@Emilio Jesús Gallego Arias don't we have a JSCoq instance somewhere with pastebin where people could debug collaboratively in situations like this?

Emilio Jesús Gallego Arias (Jun 16 2021 at 15:32):

We indeed do have collacoq, which can be accessed from the "edit" link in documents, or directly https://x80.org/collacoq/

Emilio Jesús Gallego Arias (Jun 16 2021 at 15:32):

Emilio Jesús Gallego Arias (Jun 16 2021 at 15:35):

I'd be great if we could add some collab edit mode, see https://github.com/jscoq/jscoq/issues/176 , indeed the base editing tech we use [codemirror] has quite advanced, so there is hope this could be fixed.

zeesha huq (Jun 23 2021 at 13:34):

I am defining function (cal_turn). It has four nat arguments(a,zc,bars,turns). a is calculated as a= a mod length l first time only,but for all other times it calculted as a= a+1 mod length l .It means whenever a= length l ,i get zero. Therefore I can apply (n+k*m)mod= n mod m.But don't know how to apply. Secondly I want to call my recursive function (no of time)=turns and it also equal to bars.

zeesha huq (Jun 24 2021 at 01:27):

Michael Soegtrop (Jun 24 2021 at 07:44):

Sorry, I have as much difficulty reading your Coq code as your English. It would help if you would post syntactical Coq code which doesn't quite do what you want and tell us what it should do.

If you want some argument of your fixpoint to have a specific value on the first call but different values in recursive calls, the best way is to define a wrapper function which calls your fixpoint with these specific arguments rather than trying to handle it within the fixpoint.

Also, as mentioned before, I think you do things in a too complicated way. Try to break down your function into several simpler functions which are clearer. There is no price in Coq for expressing something with as few functions as possible - on the contrary. Even if you manage to amend your function to do what you want, you likely will have a hard time to prove something about it.

zeesha huq (Jun 24 2021 at 14:00):

I want to know some alternate way of assigning a= a mod length l first time only,but for all other times it calculted as a= a+1 mod length l . Secondly both terms may be combine in the form (n+k*m)mod= n mod m?

Michael Soegtrop (Jun 24 2021 at 14:10):

As I said, you can just write a wrapper function which calls your fixpoint with this start value - this is common practice. Please post code which compiles for further discussion. The point is that Coq code which compiles has a well defined meaning, while Coq code which doesn't compile has no meaning, so it is not a good basis for discussions. Trying to extrapolate the intended meaning is difficult for your code - it has too many loose ends (e.g. all the recursive calls have wrong argument types).

zeesha huq (Jun 24 2021 at 14:34):

zeesha huq (Jun 24 2021 at 16:25):

Definition update_a (onetime: bool)(a: nat)(l: list nat) : nat:=
 match (onetime) with
 |(true) => a mod (length l)
 |(false) => (a+1) mod (length l)
end.

Michael Soegtrop (Jun 24 2021 at 17:05):

Definition update_a' (onetime: bool)(a: nat)(l: list nat) : nat:=
 (if onetime then a else a+1) mod (length l).

zeesha huq (Jun 27 2021 at 06:51):

You said , break down function into several simpler functions , define lemmas against functions . I have done this but my problem is still there. I have a sub goal and I have no idea which helping lemma will work here. Private message is also not allowed from your side. Waiting for some help in this situation.

Huỳnh Trần Khanh (Jun 27 2021 at 06:55):

This thread is somewhat long and I don't really get what you are trying to say. What do you need help with?

zeesha huq (Jun 27 2021 at 11:38):

Is it possible to use two functions in the code having same functionality ? One lemma is proved by using one definition and other sub lemma is proved by other definition. In this condition both function's equality have to prove?

Michael Soegtrop (Jun 28 2021 at 08:09):

@zeesha huq : yes, I have shown you before how to define two functions which do the same thing in a different way and how to use this in proofs.

Regarding the general topic: you are throwing little pieces of information at us and expect that we read the whole thread and try to make sense out of these pieces. The main problem with this is that your pieces are not a puzzle with a unique solution. Currently actually with now solution at all - I have not the slightest clue what your question is, so I don't have an answer. I told you a few times that you should post your complete code as a github gist or in some other way if you want that people are able to help you without wasting a lot of time.

zeesha huq (Jun 30 2021 at 17:03):

Fixpoint great_value (our_great : nat) (l : list nat) :=
match l with
| nil => our_great
| a :: l1 =>if a <=? our_great then great_value our_great l1
else great_value a l1
end.
Definition grt_value l :=
match l with
| nil => 0
| a :: tl => great_value a tl
end.
Definition list_max l := fold_right max 0 l.

Janno (Jun 30 2021 at 17:44):

I think you may. Are you looking for help with anything specific in this task? Maybe the lemma statement? Or the proof strategy?

Michael Soegtrop (Jul 01 2021 at 07:12):

@zeesha huq : yes, this looks provable and should be easy to prove by induction over the list since both definitions go by recursion over the list. This is unlike the lemma tot_numb_alt_eq I posted May 29th where both equivalent functions do the same thing in a quite different way.

zeesha huq (Jul 02 2021 at 16:45):

 Require Import List Lia.
Goal forall a l z1,
  nth 0 (a::l) 0 <  nth (S z1) (a::l) 0 ->
  list_max l <= nth 0 (a::l) 0 -> False.

I want to use above proof, but instead of list_max, I have great_value a l . Therefore I want to prove both are equal.

zeesha huq (Jul 03 2021 at 05:57):

I need ( In (nth k ls 0) ls ) from H1 : S k < length ls -> In (nth (S k) ls 0) ls . I can remove S from H1? By which command? \

Michael Soegtrop (Jul 05 2021 at 11:48):

May I ask why you are using the function grt_value at all? Its definition is much more complicated than necessary and this will make proofs more difficult. I would think it is easier to prove that list_max does what you want, also because there are lemmas about it in the standard library, then to prove something about grt_value. So I would simply replace grt_value with list_max everywhere else.

In case you really want to keep it, here is the equivalence proof step by step, which might give you some hints on how to approach this:

Require Import List PeanoNat Lia.

Fixpoint great_value (our_great : nat) (l : list nat) :=
match l with
| nil => our_great
| a :: l1 =>if a <=? our_great then great_value our_great l1
else great_value a l1
end.

Definition grt_value l :=
match l with
| nil => 0
| a :: tl => great_value a tl
end.
Definition list_max l := fold_right max 0 l.

Lemma grt_value_equiv: forall l : list nat, grt_value l = list_max l.
Proof.
  (* because great_value looks into one extra element,
     we need to get the first element from the list and generalize over it *)
  destruct l.
    1: reflexivity.
  generalize n; clear n.
  (* Now we do a straight forward induction *)
  induction l.
  - intros n. simpl.
    Search (Init.Nat.max ?a 0).
    rewrite Nat.max_0_r. reflexivity.
  - intros n. simpl.
    simpl in IHl.
    (* Here you need IHl for two different values - this is the reason for the above generalization *)
    do 2 rewrite IHl.
    Search (_ <=? _) "spec".
    destruct (Nat.leb_spec0 a n).
    all: lia.
Qed.

Michael Soegtrop (Jul 05 2021 at 11:52):

P.S.: if I remember right, you are using an older version of Coq - lia might be less powerful there and do not know how to handle Nat.max. In that case use Search to find the right lemmas. Or use a newer Coq :-)

Michael Soegtrop (Jul 05 2021 at 12:22):

There is a lemma nth_In which states k < length ls -> In (nth k ls 0) ls independent of the premises you gave. You can use Search In nth. to find this lemma.

It is not possible to derive it from In (nth (S k) ls 0) ls, since this talks about a different element of ls.

zeesha huq (Jul 14 2021 at 17:07):

I have defined a recursive function f (with arguments sum:nat & l=list nat).Number of times f is being called is determined by sum. After performing test relation (<=?), some elements are assigned to list l1 and some other to list l2. I want to find no of elements in each list separately. To do this I have introduced two nats a & b (both set to zero initially). A is incremented in case of l1 and b in case of l2.Now a and b show number of elements in each list. Is there any other smart way to handle the situation?

zeesha huq (Jul 14 2021 at 17:14):

Secondly, to count particular element in l2 . I should define what type of helping lemmas?( Like check the presence of that element in the list.Because a & b show total no of elements in l1 l2. But how to know about the presence of searching element in lists )

Michael Soegtrop (Jul 14 2021 at 17:54):

The functions should at first be simple. If you want to know the length of a list, you should simply use the length function, even if this means you call length 10x in each iteration of your recursive function. I think your main mistake is to write functions which are e.g. efficient. This is not how you should do things. At first you should define functions which are as simple and straight forward as possible and rely as much as possible on standard library supplied functions. It doesn't matter how efficient these functions are - you write these functions to prove something about them and not to execute them.

When you are finished with all your proofs you can define complicated efficient functions and prove equivalence to your simple functions. It is a big mistake to start with optimized functions up front. Definitely doing anything else then using length to get the length of a list seems to be very wrong.

There is a standard library function filter which splits a list into two lists based on a boolean predicate. There are lemmas about filter which are equivalent to what you ask for. So I would rewrite the function based on filterand length.

zeesha huq (Jul 31 2021 at 06:10):

Definition mod_i (onetime: bool)(i: nat)(l: list nat) : nat:=
(if onetime then i else i+1) mod (length l).

Definition up_bar (onetime: bool)(i bar: nat)(l: list nat): nat:=
update_bar (mod_i onetime i l) bar l.

Output value of up_bar is a natural number,I want to check its (<=?) relation with other natural number. Like this
up_bar( onetime i bar l)<=? 9. But there is error message that bool can't assign to nat. How I can remove this? up_bar also requires two nat and nat list as input arguments.

Michael Soegtrop (Aug 02 2021 at 11:48):

I guess you need parenthesis around up_bar( onetime i bar l)<=? 9. It would be easier to tell if you would post code which parses. How many times did I already ask you for this?

zeesha huq (Aug 07 2021 at 11:59):

You mean (up_bar( onetime i bar l)<=? 9)=true. Still get this message.. Illegal application (Non-functional construction):
The expression "onetime" of type "bool" cannot be applied to the term "i0" : "nat". Value of (update_bar (mod_i onetime i l) bar l.) is assigne to up_bar. Therefore want to use up_bar directly by passing arguments ( onetime i bar l). But when I write it in this form it works properly (update_bar (mod_i onetime a l) bar l).

Michael Soegtrop (Aug 09 2021 at 08:21):

As I said, please post code which actually reproduces the error message. The code you posted gives

The reference mod was not found
in the current environment.

and I don't have the time to figure out what require statements one needs to have this specific version of mod. I rarely work with plain nat, so I don't know.

Stream: Coq users

Topic: Problem in lemma writing

zeesha huq (Apr 24 2021 at 06:37):