From Undecidability.L.Tactics Require Import LTactics.
From Undecidability.L.Datatypes Require Import LFinType LBool LProd Lists.
From Undecidability.L.Functions Require Import EqBool.
Set Default Proof Using "Type".
Section Lookup.
Variable X Y : Type.
Context {eqbX : X -> X -> bool}.
Context `{eqbClass X eqbX}.
Fixpoint lookup (x:X) (A:list (X*Y)) d: Y :=
match A with
[] => d
| (key,Lproc)::A =>
if eqb x key then Lproc else lookup x A d
end.
Context `{registered X} `{@eqbCompT X _ eqbX _}.
Definition lookupTime (x:nat) (l:list (X*Y)):=
fold_right (fun '(a,b) res => eqbTime (X:=X) x (size (enc (a:X))) + res +24) 4 l.
Global Instance term_lookup `{registered Y}:
computableTime' (lookup) (fun x _ => (5, fun l _ => (1, fun d _ => (lookupTime (size (enc x)) l,tt)))).
Proof.
unfold lookup. unfold eqb.
extract. unfold lookupTime. solverec.
Qed.
Lemma lookupTime_leq x (l:list (X*Y)):
lookupTime x l <= length l * (x* c__eqbComp X + 24) + 4.
Proof.
induction l as [ | [a b] l].
-cbn. lia.
-unfold lookupTime. cbn [fold_right]. fold (lookupTime x l).
rewrite eqbTime_le_l.
setoid_rewrite IHl. cbn [length].
ring_simplify. unfold eqb. lia.
Qed.
End Lookup.
Section funTable.
Variable X : finType.
Variable Y : Type.
Variable f : X -> Y.
Definition funTable :=
map (fun x => (x,f x)) (elem X).
Variable (eqbX : X -> X -> bool).
Context `{eqbClass X eqbX}.
Lemma lookup_funTable x d:
lookup x funTable d = f x.
Proof.
unfold funTable.
specialize (elem_spec x).
generalize (elem X) as l.
induction l;cbn;intros Hel.
-tauto.
-destruct (eqb_spec x a).
+congruence.
+destruct Hel. 1:congruence.
eauto.
Qed.
End funTable.
Lemma lookup_sound' (A: Type) (B: Type) eqbA `{eqbClass (X:=A) eqbA} (L : list (prod A B)) a b def :
(forall a' b1 b2, (a',b1) el L -> (a',b2) el L -> b1=b2) -> ( (a,b) el L \/ ((forall b', ~ (a,b') el L) /\ b = def) ) -> lookup a L def = b.
Proof.
intros H1 H2.
induction L as [ |[a' b'] L]. now intuition.
cbn.
destruct (eqb_spec a a').
-subst a. destruct H2.
2:now exfalso.
eapply H1. all:easy.
-apply IHL. all:intros.
+eapply H1. all:eauto.
+destruct H2 as [[]|]. all:easy.
Qed.
Lemma lookup_sound (A: Type) (B: Type) eqbA `{eqbClass (X:=A) eqbA} (L : list (A * B)) a b def :
(forall a' b1 b2, (a', b1) el L -> (a', b2) el L -> b1 = b2) -> (a, b) el L -> lookup a L def = b.
Proof.
intros H1 H2. induction L; cbn; [ destruct H2 | ].
destruct a0 as [a0 b0]. specialize (H a a0) as Heqb. apply reflect_iff in Heqb.
unfold EqBool.eqb.
destruct eqbA.
- specialize (proj2 Heqb eq_refl) as ->.
destruct H2 as [H2 | H2]; [easy | ].
apply (H1 a0); easy.
- assert (not (a = a0)). { intros ->. easy. }
destruct H2 as [H2 | H2]; [ congruence | ].
apply IHL in H2; [easy | intros; now eapply H1].
Qed.
Lemma lookup_complete (A: Type) (B: Type) eqbA `{eqbClass (X:=A) eqbA} (L : list (prod A B)) a def :
{(a,lookup a L def) el L } + {~(exists b, (a,b) el L) /\ lookup a L def = def}.
Proof.
induction L as [ |[a' b'] L].
-cbn. right. firstorder.
-cbn. destruct (eqb_spec a a').
1:{ do 2 left. congruence. }
destruct IHL as [|[? eq]];[left|right].
+eauto.
+split. 2:easy.
now intros (?&[]).
Qed.
Section finFun.
Context (X : finType) Y {reg__X:registered X} {reg__Y:registered Y}.
Context {eqbX : X -> X -> bool} `{eqbClass X eqbX} `{H0 : @eqbCompT X _ eqbX _}.
Lemma finFun_computableTime_const (f:X -> Y) (d:Y):
{c & computableTime' f (fun _ _ => (c,tt))}.
Proof using H0.
evar (c:nat). exists c.
apply computableTimeExt with (x:= (fun c => lookup c (funTable f) d )).
{ cbn. intros ?. now rewrite lookup_funTable. }
extract.
solverec. rewrite lookupTime_leq.
unfold funTable. rewrite map_length,size_finType_any_le. unfold c. reflexivity.
Qed.
End finFun.
From Undecidability.L.Datatypes Require Import LFinType LBool LProd Lists.
From Undecidability.L.Functions Require Import EqBool.
Set Default Proof Using "Type".
Section Lookup.
Variable X Y : Type.
Context {eqbX : X -> X -> bool}.
Context `{eqbClass X eqbX}.
Fixpoint lookup (x:X) (A:list (X*Y)) d: Y :=
match A with
[] => d
| (key,Lproc)::A =>
if eqb x key then Lproc else lookup x A d
end.
Context `{registered X} `{@eqbCompT X _ eqbX _}.
Definition lookupTime (x:nat) (l:list (X*Y)):=
fold_right (fun '(a,b) res => eqbTime (X:=X) x (size (enc (a:X))) + res +24) 4 l.
Global Instance term_lookup `{registered Y}:
computableTime' (lookup) (fun x _ => (5, fun l _ => (1, fun d _ => (lookupTime (size (enc x)) l,tt)))).
Proof.
unfold lookup. unfold eqb.
extract. unfold lookupTime. solverec.
Qed.
Lemma lookupTime_leq x (l:list (X*Y)):
lookupTime x l <= length l * (x* c__eqbComp X + 24) + 4.
Proof.
induction l as [ | [a b] l].
-cbn. lia.
-unfold lookupTime. cbn [fold_right]. fold (lookupTime x l).
rewrite eqbTime_le_l.
setoid_rewrite IHl. cbn [length].
ring_simplify. unfold eqb. lia.
Qed.
End Lookup.
Section funTable.
Variable X : finType.
Variable Y : Type.
Variable f : X -> Y.
Definition funTable :=
map (fun x => (x,f x)) (elem X).
Variable (eqbX : X -> X -> bool).
Context `{eqbClass X eqbX}.
Lemma lookup_funTable x d:
lookup x funTable d = f x.
Proof.
unfold funTable.
specialize (elem_spec x).
generalize (elem X) as l.
induction l;cbn;intros Hel.
-tauto.
-destruct (eqb_spec x a).
+congruence.
+destruct Hel. 1:congruence.
eauto.
Qed.
End funTable.
Lemma lookup_sound' (A: Type) (B: Type) eqbA `{eqbClass (X:=A) eqbA} (L : list (prod A B)) a b def :
(forall a' b1 b2, (a',b1) el L -> (a',b2) el L -> b1=b2) -> ( (a,b) el L \/ ((forall b', ~ (a,b') el L) /\ b = def) ) -> lookup a L def = b.
Proof.
intros H1 H2.
induction L as [ |[a' b'] L]. now intuition.
cbn.
destruct (eqb_spec a a').
-subst a. destruct H2.
2:now exfalso.
eapply H1. all:easy.
-apply IHL. all:intros.
+eapply H1. all:eauto.
+destruct H2 as [[]|]. all:easy.
Qed.
Lemma lookup_sound (A: Type) (B: Type) eqbA `{eqbClass (X:=A) eqbA} (L : list (A * B)) a b def :
(forall a' b1 b2, (a', b1) el L -> (a', b2) el L -> b1 = b2) -> (a, b) el L -> lookup a L def = b.
Proof.
intros H1 H2. induction L; cbn; [ destruct H2 | ].
destruct a0 as [a0 b0]. specialize (H a a0) as Heqb. apply reflect_iff in Heqb.
unfold EqBool.eqb.
destruct eqbA.
- specialize (proj2 Heqb eq_refl) as ->.
destruct H2 as [H2 | H2]; [easy | ].
apply (H1 a0); easy.
- assert (not (a = a0)). { intros ->. easy. }
destruct H2 as [H2 | H2]; [ congruence | ].
apply IHL in H2; [easy | intros; now eapply H1].
Qed.
Lemma lookup_complete (A: Type) (B: Type) eqbA `{eqbClass (X:=A) eqbA} (L : list (prod A B)) a def :
{(a,lookup a L def) el L } + {~(exists b, (a,b) el L) /\ lookup a L def = def}.
Proof.
induction L as [ |[a' b'] L].
-cbn. right. firstorder.
-cbn. destruct (eqb_spec a a').
1:{ do 2 left. congruence. }
destruct IHL as [|[? eq]];[left|right].
+eauto.
+split. 2:easy.
now intros (?&[]).
Qed.
Section finFun.
Context (X : finType) Y {reg__X:registered X} {reg__Y:registered Y}.
Context {eqbX : X -> X -> bool} `{eqbClass X eqbX} `{H0 : @eqbCompT X _ eqbX _}.
Lemma finFun_computableTime_const (f:X -> Y) (d:Y):
{c & computableTime' f (fun _ _ => (c,tt))}.
Proof using H0.
evar (c:nat). exists c.
apply computableTimeExt with (x:= (fun c => lookup c (funTable f) d )).
{ cbn. intros ?. now rewrite lookup_funTable. }
extract.
solverec. rewrite lookupTime_leq.
unfold funTable. rewrite map_length,size_finType_any_le. unfold c. reflexivity.
Qed.
End finFun.