## Stream: Coq users

### Topic: list is empty or not

#### pianke (Mar 04 2023 at 16:11):

``````Fixpoint  eval (x : nat)( l : list nat) : list nat :=
match  l   with
| nil => nil
| h::t=> nil =>  if  (....)   then  h::eval x  t  else []
end.
``````

l=[7;8;9;11;12]
In if condition , i am checking test condition.If it fullfill the condition then output is complete list , otherwise it is empty.
For example testing sequence of elements in l,now 7,8,9 follow the condition.
Therefore output list =[7;8;9].
What statement i should write after else so that i get whole list at output if it is in sequence/follow the condition ,otherwise give empty.
l=[7;8;9;10;11] -> [7;8;9;10;11]
l=[7;8;9;11;12] ->[].
Simply in case found single mismatch give empty list.

#### Pierre Castéran (Mar 04 2023 at 17:01):

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/elements.20mismatch

``````Fixpoint same_pattern (p : nat -> nat -> bool) (l: list nat)
:= match l with
[] | [_] => true
| x::((y::l) as tl) => (p x y && same_pattern p tl)
end.

Definition test p l : list nat :=
if same_pattern p l then l else [].

(* A variant *)

Definition test' p l :=
match l with
[] | [_ ] => nil
| _ => test p l
end.

Compute test (fun x y => Nat.eqb y (S x)) [4;5;6;7].
Compute test (fun x y => Nat.eqb y (S x)) [4;5;6;8;7].
Compute test (fun x y => Nat.eqb y (S x)) [4].
Compute test' (fun x y => Nat.eqb y (S x)) [4].
Compute test' (fun x y => Nat.eqb y (S x)) [4;5;6;7;8].
``````

#### pianke (Mar 08 2023 at 03:41):

Thank you. It works very well. If i exclude last element from any kind of comparison then what i should do?
I have tried addition of new constructor x::y::nil=>[]. But still role of last element exist.

#### Pierre Castéran (Mar 08 2023 at 06:23):

My advice would be "don't change the function `same_pattern`, but the function which calls it".

The reason is that `same_pattern` is a correct implementation of a test of the property "for any `i` and `j`, if `j` follows immediately `i`in `l`, then `p i j` is true". Of course, this correction can be proved in Coq. This function can be used in various applications. Please note that, logically, this function must return `true`when the list has less than 2 elements.

``````Definition is_sorted l := same_pattern (fun x y => Nat.ltb x y) l.

Compute is_sorted [4].
Compute is_sorted [].
Compute is_sorted [4;5;7].

Definition is_iterates (f: nat -> nat) :=
same_pattern (fun x y => Nat.eqb y (f x)).

Compute is_iterates (fun n => 2 * n) [3;6;12;24].
Compute is_iterates  (fun n => 2 * n) [3].
``````

Now, if you want for some reason to ignore the last element of the list, you can remove it before calling `same_pattern`.

``````Fixpoint remove_last (l: list nat) :=
match l with
[] | [ _ ] => []
| x :: tl => x :: remove_last tl
end.

Compute is_sorted (remove_last [4;5;7;8;0]).
``````

Then, you will keep a correct general purpose function, and will be able to consider particular cases.

A last remark: if you change some `true`s with `false`in `same_pattern`, you lose the function's correctness.

#### pianke (Mar 09 2023 at 10:41):

Remarks are very helpful . Thank you for suggestions.
1) " this function must return true when the list has less than 2 elements." . If i need empty for the case where list contains two elements then i should define another function where introduce [x::y]=>[] and another constructor for x::((y::l) as tl) then use same_pattern for this case only . In this way i have not changed the function but the presence of another constraint
give me require result and keep it general purpose.(is this right way?)
2) "you lose the function's correctness." means customize function will be difficult to prove. I have applied them on number of lists it gives correct result.

#### Pierre Castéran (Mar 09 2023 at 13:44):

2) By "function correctness" I mean that `same_pattern p l` checks whether, for any pair `x`, `y` of numbers such that `y` follows immediately `x` in `l`, `p x y = true`holds.

Formally:

``````Fixpoint just_before (x y : nat) (l: list nat) : bool :=
match l with
[] | [_] => false
| h1::((h2::l) as tl) => Nat.eqb h1 x && Nat.eqb h2 y ||  just_before x y tl
end.

Lemma correctness p l :
same_pattern p l = true <->   (forall x y, just_before x y l = true -> p x y = true).
(* ... *)
``````

Last updated: Jun 14 2024 at 19:02 UTC