Stream: Coq users

Topic: list & bool

pianke (Jan 16 2022 at 13:34):

I have a function f1 with (nat & nat list input arguments)and gives bool data type at output.Now I want to define another function f2 with two nat lists and bool output.Want to provide each element of l1 to f1 so that function f2 gives true only when all elements of l1 given to f1 gives true. Nil gives false . Problem is that when (f2 t l2) terminates it also gives false which may be true.

Fixpoint f2 (l1 l2:list nat): bool :=
match l1 with
| nil =>false
| cons p t=> if (f1 p l1) then f2 t l2
                                   else false
end.

Pierre Castéran (Jan 16 2022 at 15:22):

Your function f2always returns false.

Goal forall l1 l2,  f2 l1 l2 = false.
Proof.
  induction l1 as [| a l1]; cbn; [trivial |].
  intro l2;  rewrite IHl1; now destruct (f1 a (a::l1)).
Qed.

Perhaps you should change the definition and return true when l1is empty.
Please compare with the definition of forallb in https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html. You may try the following code:

Require Import Bool.
Fixpoint f2 (l1 l2:list nat): bool :=
match l1 with
| nil =>true (* here *)
| cons p t => f1 p l1  &&  f2 t l2
end.

pianke (Jan 17 2022 at 14:44):

Thank you

Last updated: Oct 13 2024 at 01:02 UTC