Stream: Coq users

Topic: constructor


view this post on Zulip pianke (Mar 03 2023 at 17:00):

Fixpoint check ( x y :nat)(l : list nat):bool :=
  | nil => false
  | x ::nil=> true
  |a1::a2::t=> if.....then check a1 a2 t else false

Out put bool value should be false when there exist one element. If i do that then it give false for all the cases because of recursive function. How i can solve it ,so that it gives false incase of one element not for the case where list goes to its end .

view this post on Zulip Laurent Théry (Mar 03 2023 at 18:35):

using 2 functions ?

Fixpoint check1 ( x y :nat)(l : list nat):bool :=
  | nil => false
  | x ::nil=> true
  |a1::a2::t=> if.....then check1 a1 a2 t else false

Definition  check ( x y :nat)(l : list nat):bool :=
match l with
  | nil => false
  | x ::nil=> false
  |_::_:: _ =>  check1 x y l
end

view this post on Zulip pianke (Mar 04 2023 at 08:34):

Only problem in check1 is that it gives true in case of single element, but i want to have false in that case. If i replace second constructor with false then it give false in case of third constructor,when it reaches the end of list. As a result i get one correct statement at a time.

view this post on Zulip Laurent Théry (Mar 04 2023 at 09:56):

no check1 returns true in the case of the recursion of a list of more than one element. checkreturns false in the case of a list of one element. The final function is check not check1

view this post on Zulip pianke (Mar 05 2023 at 06:32):

Ok, thank you. Problem of single element get solved. If multiple elements lie in the list then it works properly. Even when two elements left then it works. But when list have two elements it gives true but i need false here (in this situation only). When modify a1::a2::nil=> false then every thing goes wrong. May i bring this change at this particular point?

Fixpoint  check3 (x y  : nat)( l  : list nat) : bool :=
  match  l   with
     | nil => false
     | [c] =>false
     | a1::a2::nil=> true
     | a1::((a2::t) as t2)  =>
                               if (.....)  check3 x y t2  else false
end.

view this post on Zulip Pierre Castéran (Mar 05 2023 at 08:58):

You may use the pattern we discussed recently in the following conversations:

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/list.20is.20empty.20or.20not
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/constructor

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

Definition main p l :=
  match l with
   nil | [_ ] | [_ ;  _] => false
  |  _ => helper p l
end.
Compute main (fun x y => Nat.eqb y (3 + x)) [5;8].
Compute main (fun x y => Nat.eqb y (3 + x)) [5;8;11].

Last updated: Oct 04 2023 at 23:01 UTC