Stream: Coq users

Topic: list is empty or not


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

view this post on Zulip Pierre Castéran (Mar 04 2023 at 17:01):

You simply have to adapt Laurent's answer in:
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].

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

view this post on Zulip 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 iin 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 truewhen 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 trues with falsein same_pattern, you lose the function's correctness.

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

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

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: Mar 28 2024 at 18:02 UTC