Stream: Coq users

Topic: repeat function

zohaze (Mar 14 2022 at 17:56):

I am splitting a natural number list at particular position then pass first five numbers to Coq code to perform different function on it. Result is fine. Now want to repeat same function on next five elements of the list and so on. What command I should use and how I should apply it?

Pierre Castéran (Mar 14 2022 at 20:31):

The following code is written under two assumptions (which can be changed)

• You build the list of images of your fonction
• If the length of the list is not a multiple of 5, the extra elements are ignored.

Require Import List.

Fixpoint take_five {A B} (f : A -> A -> A -> A -> A -> B)
         (l: list A) : list B :=
  match  l with
    (a:: b :: c:: d :: e:: rest) =>  f a b c d e :: take_five f rest
  | _ => nil
  end.

Fixpoint iota n :=
  match n with
    0 => nil
  | S p => n:: iota p
  end.

Compute take_five  (fun a b c d e =>  (a , e)) (List.rev (iota 17)).

zohaze (Mar 15 2022 at 18:04):

Thank you. There are multiple functions in the code . It might be difficult to do above for each and every function.
Is there any command which I can apply on whole block of code(which i want to repeat) ? Simply command repeat all functions on specific input and when input change then do the same as multiple time as user define it. Secondly, instead of pair ,may I get list of five elements.

Last updated: Apr 18 2024 at 18:01 UTC