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.
```

Your function `f2`

always 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 `l1`

is 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.
```

Thank you

Last updated: Jun 16 2024 at 02:41 UTC