From Undecidability.L.Tactics Require Import LTactics.
From Undecidability.L Require Import UpToC.
From Undecidability.L.Datatypes Require Export List_enc LBool.
Set Default Proof Using "Type".
Section forallb.
Variable (X : Type).
Context (H : registered X).
Definition c__forallb := 15.
Definition forallb_time (fT : X -> nat) (l : list X) := sumn (map (fun elm => fT elm + c__forallb) l) + c__forallb.
Global Instance term_forallb : computableTime' (@forallb X) (fun f fT => (1, fun l _ => (forallb_time (callTime fT) l, tt))).
Proof.
extract.
solverec.
all: unfold forallb_time, c__forallb; solverec.
Qed.
Lemma forallb_time_eq f (l:list X):
forallb_time f l = sumn (map f l) + length l * c__forallb + c__forallb.
Proof.
induction l as [ | x l IH];cbn -[c__forallb]. lia. unfold forallb_time in IH. nia.
Qed.
Lemma forallb_time_const c (l:list X):
forallb_time (fun _ => c) l = length l * (c+c__forallb) + c__forallb.
Proof.
induction l as [ | x l IH];cbn -[c__forallb]. lia. unfold forallb_time in IH; nia.
Qed.
End forallb.
Section foldl_time.
Context {X Y : Type}.
Context {H : registered X}.
Context {F : registered Y}.
Definition c__fold_left := 15.
Definition c__fold_left2 := 5.
Fixpoint fold_left_time (f : X -> Y -> X) (t__f : X -> Y -> nat) (l : list Y) (acc : X) :=
(match l with
| [] =>c__fold_left
| (l :: ls) => t__f acc l + c__fold_left + fold_left_time f t__f ls (f acc l)
end ).
Global Instance term_fold_left :
computableTime' (@fold_left X Y) (fun f fT => (c__fold_left2, fun l _ => (c__fold_left2, fun acc _ => (fold_left_time f (callTime2 fT) l acc, tt)))).
Proof.
extract.
solverec. all: unfold c__fold_left, c__fold_left2; solverec.
Qed.
End foldl_time.
Section foldr_time.
Context {X Y: Type}.
Context {H:registered X}.
Context {H0: registered Y}.
Definition c__fold_right := 15.
Fixpoint fold_right_time (f : Y -> X -> X) (tf : Y -> X -> nat) (l : list Y) (acc : X) :=
match l with [] => c__fold_right
| l::ls => tf l (fold_right f acc ls) + c__fold_right + fold_right_time f tf ls acc
end.
Global Instance term_fold_right : computableTime' (@fold_right X Y) (fun f fT => (1, fun acc _ => (1, fun l _ => (fold_right_time f (callTime2 fT) l acc + c__fold_right, tt)))).
Proof.
extract. solverec. all: unfold fold_right, c__fold_right; solverec.
Qed.
End foldr_time.
From Undecidability.L Require Import UpToC.
From Undecidability.L.Datatypes Require Export List_enc LBool.
Set Default Proof Using "Type".
Section forallb.
Variable (X : Type).
Context (H : registered X).
Definition c__forallb := 15.
Definition forallb_time (fT : X -> nat) (l : list X) := sumn (map (fun elm => fT elm + c__forallb) l) + c__forallb.
Global Instance term_forallb : computableTime' (@forallb X) (fun f fT => (1, fun l _ => (forallb_time (callTime fT) l, tt))).
Proof.
extract.
solverec.
all: unfold forallb_time, c__forallb; solverec.
Qed.
Lemma forallb_time_eq f (l:list X):
forallb_time f l = sumn (map f l) + length l * c__forallb + c__forallb.
Proof.
induction l as [ | x l IH];cbn -[c__forallb]. lia. unfold forallb_time in IH. nia.
Qed.
Lemma forallb_time_const c (l:list X):
forallb_time (fun _ => c) l = length l * (c+c__forallb) + c__forallb.
Proof.
induction l as [ | x l IH];cbn -[c__forallb]. lia. unfold forallb_time in IH; nia.
Qed.
End forallb.
Section foldl_time.
Context {X Y : Type}.
Context {H : registered X}.
Context {F : registered Y}.
Definition c__fold_left := 15.
Definition c__fold_left2 := 5.
Fixpoint fold_left_time (f : X -> Y -> X) (t__f : X -> Y -> nat) (l : list Y) (acc : X) :=
(match l with
| [] =>c__fold_left
| (l :: ls) => t__f acc l + c__fold_left + fold_left_time f t__f ls (f acc l)
end ).
Global Instance term_fold_left :
computableTime' (@fold_left X Y) (fun f fT => (c__fold_left2, fun l _ => (c__fold_left2, fun acc _ => (fold_left_time f (callTime2 fT) l acc, tt)))).
Proof.
extract.
solverec. all: unfold c__fold_left, c__fold_left2; solverec.
Qed.
End foldl_time.
Section foldr_time.
Context {X Y: Type}.
Context {H:registered X}.
Context {H0: registered Y}.
Definition c__fold_right := 15.
Fixpoint fold_right_time (f : Y -> X -> X) (tf : Y -> X -> nat) (l : list Y) (acc : X) :=
match l with [] => c__fold_right
| l::ls => tf l (fold_right f acc ls) + c__fold_right + fold_right_time f tf ls acc
end.
Global Instance term_fold_right : computableTime' (@fold_right X Y) (fun f fT => (1, fun acc _ => (1, fun l _ => (fold_right_time f (callTime2 fT) l acc + c__fold_right, tt)))).
Proof.
extract. solverec. all: unfold fold_right, c__fold_right; solverec.
Qed.
End foldr_time.