Stream: Coq users

Topic: list nat


view this post on Zulip zohaze (Feb 03 2023 at 16:40):

Fixpoint   myfunction ( l: list nat) : list nat :=
  match l  with
     | nil => nil
     |h::t   =>   match (here code requires h and next of h) with
                                         |false => []
                                         |true => h1:: myfunction t

 end
end.

Want to keep list of h1 in true (case). e.g l=[2,33,41,5,66,7] require list [33,41,5,66,7] .
If i write h::h1::t then i have to add third constructor h::nil . This case gives wrong results when there are
odd elements in input list.

view this post on Zulip Michael Soegtrop (Feb 03 2023 at 18:23):

You need to define what happens in the case the list has exactly 1 element, because if the list length is odd, you will end up in this case. So you need a match structure like:

match l with
| nil => nil
| h::nil => what do we do here?
| h1::h2::t => the usual case
end

view this post on Zulip zohaze (Feb 04 2023 at 05:26):

Fixpoint   myfunction ( l l2: list nat) : list nat :=
  match l  with
     | nil => nil
     ||h::nil => [h]
     |h1::h2::t   =>   match (leb h2 ( count h1 l2) ) with
                                         |false => []
                                         |true => h2:: myfunction t l2

 end
end.

I need first &next element of complete list for comaparison (list may contain even or odd elements).
1) h1::h2::t ->during recursive call there is jump/skip of two elements.
e.g l=[2,33,41,5,66,7,8] output list = [33 ] t=[41,5,66,7,8].

During next recursion h1=41 & h2= 5 output list = [33,5 ]
But i need [33,41, 5 ]
2) How i should append element of constructor 2 with list of constructor 3, or correct the above?

view this post on Zulip Michael Soegtrop (Feb 04 2023 at 09:51):

You can pass (h2::t) as argument to the recursive call (or (h1::t) since you prepend h2 in the recursive call). You need to give a measure then (as explained before). Coq won't be able to figure out automatically that the list is decreasing, but the proof will be trivial.

view this post on Zulip Pierre Castéran (Feb 04 2023 at 09:56):

You may use the askeyword like in

Fixpoint f (l: list nat) :list nat :=
  match l with
  | nil => nil
  | [x] => [x]
  | h1::((h2::t) as tl) => if p h1 h2
                         then h1 :: f tl   (* skips 1 element *)
                         else h2 :: h1 :: f t  (* skips 2 elements *)
  end.

view this post on Zulip zohaze (Feb 04 2023 at 14:21):

Lot of thanks.

view this post on Zulip zohaze (Feb 25 2023 at 11:30):

I want to adjust function (fun a b l) in above . Output
of this function is list which gives nil in case of one element in the list and in empty case). I am replacing l with (fun a b l) then second constructor [x]=> [x] gives problem. May i address it? error msg: cannot find decreasing value.

Fixpoint f (a b:nat) (l: list nat) :list nat :=
  match (fun a b l)  with
  | nil => nil
  | [x] => [x]   (* according to modification it should be nil in case of one element *)
  | h1::((h2::t) as tl) => if p h1 h2
                         then h1 :: f  a b tl   (* skips 1 element *)
                         else h2 :: h1 :: f a b t  (* skips 2 elements *)
  end.

view this post on Zulip Laurent Théry (Feb 25 2023 at 12:37):

This looks ok :

Require Import List.
Import ListNotations.

Parameter p : nat -> nat -> bool.

Fixpoint f (a b:nat) (l: list nat) : list nat :=
  match l  with
  | nil => nil
  | [x] => [x]   (* according to modification it should be nil in case of one element *)
  | h1::((h2::t) as tl) => if p h1 h2
                         then h1 :: f  a b tl   (* skips 1 element *)
                         else h2 :: h1 :: f a b t  (* skips 2 elements *)
  end.

view this post on Zulip zohaze (Feb 25 2023 at 14:10):

output list of (fun a b l) is different list than input argument list l.Secondly, output of (fun a b l) is empty when it contains one element and or when it is empty. But input argument list l is empty only when this list is empty.Third,in recursive call tl should be assign to input argument list l which causes conflict with output of (fun a b l). Introduction of two lists , one for fun ab l and second for recursive call . (could be solution?0
Fixpoint f (a b:nat) (l l2: list nat) :list nat :=
match (F a b l) with
| nil => nil
| [x] => [x] (* problem here, according to modification it should be nil in case of one element in new definition *)
| h1::((h2::t) as tl) => if eq h1 h2
then h1 :: f a b l tl (* skips 1 element *)
else h2 :: h1 :: f a b l t

view this post on Zulip Pierre Castéran (Feb 25 2023 at 17:32):

May be you should assume (or prove with your example) that length (F a b l) <= length l. (I renamed funinto Fbecause funis a Coq keyword). Here's a simple example (you may have to change the definitions of Fand p).
Note that your definitions present some problems (in addition to the recursion):
The arguments a, band l keep the same value during all the computation, and l2 is unused.
So, it's extremely difficult to understand and comment what you wanted to compute.

Require Import Arith Lia List Recdef .
Import ListNotations.

Definition F a b l := map (fun x => x + a + b) l.

Remark Fdecr : forall a b l, length (F a b l) <= length l.
Proof.
  intros; unfold F; now rewrite map_length.
Qed.

Definition  p : nat -> nat -> bool := Nat.ltb.


Function f (a b: nat) (l: list nat) {measure length l} : list nat :=
  match (F a b l) with
    nil | [_] => nil
  | x:: ( (y:: t) as tl) => if p x y then x :: f a b tl
                            else y :: x :: f a b  t
  end.
Proof.
  intros.
  generalize  (Fdecr  a b l) ;rewrite teq; simpl; lia.
  intros.
  generalize (Fdecr  a b l); rewrite teq; simpl; lia.
Defined.

(* Example *)

Compute f  10 20 [4;6;3;7].

view this post on Zulip zohaze (Feb 26 2023 at 17:22):

(deleted)


Last updated: Jun 18 2024 at 08:01 UTC