From 733c87b4edde8eb8ece48f5ccf5b3d8bfdf7b60c Mon Sep 17 00:00:00 2001 From: Stefan Haan Date: Thu, 24 Nov 2022 13:02:10 +0100 Subject: [PATCH] use Proper and rewrite from stdlib for monotonicity --- _CoqProject | 1 + theories/Complexity/Definitions.v | 50 +- theories/Complexity/Monotonic.v | 122 +-- theories/Complexity/NP.v | 93 +-- theories/Complexity/ONotation.v | 14 +- theories/Complexity/PolyTimeComputable.v | 47 +- theories/Complexity/Subtypes.v | 19 +- theories/Complexity/UpToCPoly.v | 48 +- theories/L/ComparisonTimeBoundDerivation.v | 75 +- theories/L/Datatypes/LBinNums.v | 2 +- theories/L/Datatypes/LNat.v | 5 + theories/L/TM/TMflatComp.v | 7 +- theories/Libs/CookPrelim/FlatFinTypes.v | 23 +- theories/Libs/CookPrelim/MorePrelim.v | 7 +- theories/Libs/CookPrelim/PolyBounds.v | 110 ++- theories/NP/Clique/FlatClique.v | 116 +-- theories/NP/Clique/kSAT_to_FlatClique.v | 135 ++-- theories/NP/L/CanEnumTerm.v | 34 +- theories/NP/L/CanEnumTerm_def.v | 7 +- theories/NP/L/GenNPBool.v | 32 +- theories/NP/L/GenNP_is_hard.v | 22 +- theories/NP/SAT/CookLevin.v | 9 +- .../CookLevin/Reductions/BinaryCC_to_FSAT.v | 217 +++--- .../CookLevin/Reductions/FlatCC_to_BinaryCC.v | 149 ++-- .../Reductions/FlatSingleTMGenNP_to_FlatTCC.v | 712 ++++++++++-------- .../CookLevin/Reductions/FlatTCC_to_FlatCC.v | 35 +- ...xed_singleTapeTM_to_FlatFunSingleTMGenNP.v | 11 +- .../NP/SAT/CookLevin/Subproblems/FlatCC.v | 46 +- theories/NP/SAT/FSAT/FSAT.v | 5 +- theories/NP/SAT/FSAT/FSAT_to_SAT.v | 46 +- theories/NP/SAT/FSAT/FormulaEncoding.v | 21 +- theories/NP/SAT/SAT_inNP.v | 15 +- theories/NP/SAT/kSAT.v | 15 +- theories/NP/SAT/kSAT_to_SAT.v | 19 +- theories/NP/TM/LM_to_mTM.v | 97 +-- theories/NP/TM/L_to_LM.v | 34 +- theories/NP/TM/TMGenNP.v | 12 +- theories/NP/TM/mTM_to_singleTapeTM.v | 48 +- 38 files changed, 1298 insertions(+), 1162 deletions(-) diff --git a/_CoqProject b/_CoqProject index 87c967fa..1278505c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -52,6 +52,7 @@ theories/L/AbstractMachines/FlatPro/Computable/LPro.v theories/L/Datatypes/LBinNums.v theories/L/Datatypes/LComparison.v theories/L/Datatypes/LDepPair.v +theories/L/Datatypes/LNat.v theories/L/Functions/IterupN.v theories/L/Functions/BinNums.v theories/L/Functions/BinNumsAdd.v diff --git a/theories/Complexity/Definitions.v b/theories/Complexity/Definitions.v index 65b96d2b..9f7c3130 100644 --- a/theories/Complexity/Definitions.v +++ b/theories/Complexity/Definitions.v @@ -4,8 +4,6 @@ From Complexity.Complexity Require Export Monotonic ONotation LinTimeDecodable. (** * Basics of decision problems *) - - Record decInTime {X} `{R :encodable X} P (fT : nat -> nat) :Type := decInTime_intro { @@ -79,11 +77,15 @@ Record resSizePoly X Y `{encodable X} `{encodable Y} (f : X -> Y) : Type := resSize__rSP : nat -> nat; bounds__rSP : forall x, size (enc (f x)) <= resSize__rSP (size (enc x)); poly__rSP : inOPoly resSize__rSP; - mono__rSP : monotonic resSize__rSP; + mono__rSP : Proper (le ==> le) resSize__rSP; }. Smpl Add 10 (simple apply poly__rSP) : inO. -Smpl Add 10 (simple apply mono__rSP) : inO. + +#[global] +Instance monotonic_rSP X Y `{encodable X} `{encodable Y} (f : X -> Y) (rsp: resSizePoly f): + Proper (le ==> le) (resSize__rSP rsp). +Proof. apply mono__rSP. Qed. Record polyTimeComputable X Y `{encodable X} `{encodable Y} (f : X -> Y) := polyTimeComputable_intro @@ -91,15 +93,19 @@ Record polyTimeComputable X Y `{encodable X} `{encodable Y} (f : X -> Y) := time__polyTC : nat -> nat; comp__polyTC : computableTime' f (fun x (_ : unit) => (time__polyTC (size (enc x)),tt)); poly__polyTC : inOPoly time__polyTC ; - mono__polyTC : monotonic time__polyTC; + mono__polyTC : Proper (le ==> le) time__polyTC; resSize__polyTC :> resSizePoly f; }. +#[global] +Instance monotonic_polyTC X Y `{encodable X} `{encodable Y} (f : X -> Y) (ptc: polyTimeComputable f): + Proper (le ==> le) (time__polyTC ptc). +Proof. apply mono__polyTC. Qed. + #[export] Hint Extern 1 (computableTime _ _) => unshelve (simple apply @comp__polyTC);eassumption :typeclass_instances. Smpl Add 10 (simple apply poly__polyTC) : inO. -Smpl Add 10 (simple apply mono__polyTC) : inO. Import Nat. @@ -115,7 +121,9 @@ Proof. Qed. Lemma inOPoly_computable (f:nat -> nat): - inOPoly f -> exists f':nat -> nat , inhabited (polyTimeComputable f') /\ (forall x, f x <= f' x) /\ inOPoly f' /\ monotonic f'. + inOPoly f -> + exists f':nat -> nat, inhabited (polyTimeComputable f') /\ + (forall x, f x <= f' x) /\ inOPoly f' /\ Proper (le ==> le) f'. Proof. intros (i&Hf). eapply inO__bound in Hf as (c&Hf). @@ -128,14 +136,20 @@ Proof. rewrite (LNat.size_nat_enc_r x) at 2. set (n0:= (size (enc x))). unfold time. reflexivity. } - 3:eexists. - 3:{intros. rewrite (LNat.size_nat_enc) at 1. rewrite Nat.pow_le_mono_l. 2:now apply (LNat.size_nat_enc_r). set (size (enc x)). instantiate (1:= fun n0 => _). cbn beta;reflexivity. - } - all:unfold time;smpl_inO. - -repeat apply conj. easy. all:smpl_inO. + + unfold time. smpl_inO. + + unfold time. solve_proper. + + eexists. + * intro x. rewrite (LNat.size_nat_enc) at 1. + rewrite Nat.pow_le_mono_l by apply (LNat.size_nat_enc_r). + set (size (enc x)). instantiate (1:= fun n0 => _). cbn beta;reflexivity. + * smpl_inO. + * solve_proper. + - repeat split. + + easy. + + smpl_inO. + + solve_proper. Qed. - Lemma resSizePoly_compSize X Y `{encodable X} `{encodable Y} (f: X -> Y): resSizePoly f -> exists H : resSizePoly f, inhabited (polyTimeComputable (resSize__rSP H)). Proof. @@ -169,18 +183,18 @@ Proof. 2:easy. rewrite size_term_enc_r. generalize (size (enc x)) as n;intros. unfold time. reflexivity. - -unfold time. smpl_inO. - -unfold time. smpl_inO. + - unfold time. smpl_inO. + - unfold time. solve_proper. -{evar (resSize : nat -> nat). [resSize]:intro n. exists resSize. -intros t. specialize (decode_correct2 (X:=X) (t:=t)) as H'. destruct decode. - setoid_rewrite <- H'. 2:reflexivity. + specialize (H' x Logic.eq_refl). rewrite <- H'. *rewrite size_option,LTerm.size_term_enc_r. generalize (size (enc (enc x))). unfold resSize. reflexivity. *unfold enc at 1. cbn. unfold resSize. nia. - -unfold resSize. smpl_inO. - -unfold resSize. smpl_inO. + - unfold resSize. smpl_inO. + - unfold resSize. solve_proper. } Qed. diff --git a/theories/Complexity/Monotonic.v b/theories/Complexity/Monotonic.v index 52162e70..2ff781ec 100644 --- a/theories/Complexity/Monotonic.v +++ b/theories/Complexity/Monotonic.v @@ -1,113 +1,55 @@ -From smpl Require Import Smpl. -From Undecidability Require Import L.Prelim.MoreBase. -Definition monotonic (f:nat -> nat) : Prop := - forall x x', x <= x' -> f x <= f x'. - -Lemma monotonic_c c: monotonic (fun _ => c). -Proof. - hnf. - intros **. easy. -Qed. +Require Import Morphisms Arith. +#[global] Instance add_params: Params (@Nat.add) 0 := {}. +#[global] Instance mul_params: Params (@Nat.mul) 0 := {}. -Lemma monotonic_add f1 f2: monotonic f1 -> monotonic f2 -> monotonic (fun x => f1 x + f2 x). -Proof. - unfold monotonic. - intros H1 H2 **. - rewrite H1,H2. reflexivity. all:eassumption. -Qed. +(* TODO: can be removed if https://github.com/coq/coq/pull/16792 is merged *) -Lemma monotonic_S f : monotonic f -> monotonic (fun x => S (f x)). +#[global] Instance add_le_mono: Proper (le ==> le ==> le) Nat.add. Proof. - intros H. eapply (@monotonic_add (fun _ => 1) f); [apply monotonic_c | apply H]. -Qed. - -Lemma monotonic_mul f1 f2: monotonic f1 -> monotonic f2 -> monotonic (fun x => f1 x * f2 x). -Proof. - unfold monotonic. - intros H1 H2 **. - rewrite H1,H2. reflexivity. all:eassumption. -Qed. - -Require Import Nat. -Lemma monotonic_pow_c f1 c: monotonic f1 -> monotonic (fun x => (f1 x) ^ c). -Proof. - intros **. - unfold monotonic. - intros H1 **. eapply PeanoNat.Nat.pow_le_mono_l. apply H. easy. + intros x1 y1 H1 x2 y2 H2. + now apply Nat.add_le_mono. Qed. -Lemma monotonic_x: monotonic (fun x => x). +#[global] Instance mul_le_mono: Proper (le ==> le ==> le) Nat.mul. Proof. - unfold monotonic. easy. + intros x1 y1 H1 x2 y2 H2. + now apply Nat.mul_le_mono. Qed. -Lemma monotonic_comp f1 f2: monotonic f1 -> monotonic f2 -> monotonic (fun x => f1 (f2 x)). +#[global] Instance pow_le_mono: Proper (le ==> eq ==> le) Nat.pow. Proof. - unfold monotonic. - intros H1 H2 **. - rewrite H1. reflexivity. eauto. + intros x1 y1 H1 x2 y2 H2. subst. + now apply Nat.pow_le_mono_l. Qed. -Smpl Create monotonic. -Smpl Add 10 (first [ simple eapply monotonic_add | simple eapply monotonic_S | simple eapply monotonic_mul | simple eapply monotonic_c | simple eapply monotonic_x | simple eapply monotonic_pow_c] ) : monotonic. +(* end: can be removed ... *) -Smpl Add 20 (lazymatch goal with - |- monotonic (fun x => ?f (@?g x)) => - (lazymatch g with - | fun x => x => fail - | _ => simple eapply monotonic_comp - end) - end) : monotonic. +#[global] Instance monotonic_c c: Proper (le==>le) (fun _ => c). +Proof. constructor. Qed. -#[export] -Instance monotonic_pointwise_eq: Proper ((pointwise_relation _ eq) ==> iff) monotonic. +#[global] +Instance monotonic_pointwise_eq: Proper ((pointwise_relation _ eq) ==> iff) (Proper (le==>le)). Proof. - intros ? ? R1. unfold monotonic. setoid_rewrite R1. all:easy. + intros f g R. split; intros M x y H. + - now rewrite <-R, H. + - now rewrite R, H. Qed. -(* -Inductive TTnat: Type -> Type := - TTnatBase : TTnat nat -| TTnatArr X Y (ttx : TTnat X) (tty : TTnat Y) : TTnat (X -> Y). +Require Import Lia. -Arguments TTnatArr _ _ {_ _}. -Existing Class TTnat. #[export] -Existing Instances TTnatBase TTnatArr. - - -Fixpoint leHO {ty} {tt : TTnat ty} : ty -> ty -> Prop := - match tt with - TTnatBase => le - | TTnatArr X Y => respectful (@leHO X _) (@leHO Y _) - end. -Arguments leHO : simpl never. +Instance proper_lt_mul : Proper (lt ==> eq ==> le) Nat.mul. +Proof. intros a b c d e f. nia. Qed. -(* #[export] -Instance leHO_Pointwise_le X Y (ttx : TTnat X) (tty : TTnat Y) (f g : X -> Y): - Proper - Pointwise (@leHO _ ttx ==> leqHO _ tty).*) - -Notation "'monotonicHO'" := (Proper leHO) (at level 0). - -(*) -Lemma leHO_monotonic (f : nat -> nat) : - monotonic f <-> monotonicHO f. -Proof. - reflexivity. -Qed. - -Module test. - Variable f : nat -> nat -> nat. - Context {Hf : monotonicHO f}. +Instance proper_lt_add : Proper (lt ==> eq ==> le) Nat.add. +Proof. intros a b c d e f. nia. Qed. - Goal forall x y y', y <= y' -> f x y <= f x y'. - Proof. - pose Hf. - intros. now setoid_rewrite H. - Qed. -End test. +#[export] +Instance mult_lt_le : Proper (eq ==> lt ==> le) mult. +Proof. intros a b -> d e H. nia. Qed. -*)*) +#[export] +Instance add_lt_lt : Proper (eq ==> lt ==> lt) Nat.add. +Proof. intros a b -> c d H. lia. Qed. \ No newline at end of file diff --git a/theories/Complexity/NP.v b/theories/Complexity/NP.v index f92971a0..ae6a2d46 100644 --- a/theories/Complexity/NP.v +++ b/theories/Complexity/NP.v @@ -17,7 +17,7 @@ Section NP_certificate_fix. Context `{RegY : encodable Y}. Definition inTimePoly {X} `{encodable X} `(P: X -> Prop):= - exists f, inhabited (decInTime P f) /\ inOPoly f /\ monotonic f. + exists f, inhabited (decInTime P f) /\ inOPoly f /\ Proper (le ==> le) f. Record polyCertRel (P: X -> Prop) (R: X -> Y -> Prop) : Type := polyBoundedWitness_introSpec @@ -26,9 +26,12 @@ Section NP_certificate_fix. sound__pCR : forall x y, R x y -> P x; complete__pCR : forall x, P x -> exists (y:Y), R x y /\ size (enc y) <= p__pCR (size (enc x)); poly__pCR : inOPoly p__pCR ; - mono__pCR : monotonic p__pCR; + mono__pCR : Proper (le ==> le) p__pCR; }. + #[global] Instance monotonic__pCR P R (H: polyCertRel P R): Proper (le ==> le) (p__pCR H). + Proof. apply mono__pCR. Qed. + Lemma polyCertRel_compPoly (P:X -> Prop) R: polyCertRel P R -> exists H : polyCertRel P R , inhabited (polyTimeComputable (p__pCR H)). Proof. @@ -44,7 +47,7 @@ Section NP_certificate_fix. Lemma inTimePoly_compTime (P:X -> Prop): - inTimePoly P -> exists f, inhabited (polyTimeComputable f) /\ inhabited (decInTime P f) /\ inOPoly f /\ monotonic f. + inTimePoly P -> exists f, inhabited (polyTimeComputable f) /\ inhabited (decInTime P f) /\ inOPoly f /\ Proper (le ==> le) f. Proof. intros (time&[P__dec]&t__poly&t__mono). destruct (inOPoly_computable t__poly) as (p'&?&Hbounds&?&?). @@ -68,7 +71,6 @@ Section NP_certificate_fix. End NP_certificate_fix. Smpl Add 10 (simple apply poly__pCR) : inO. -Smpl Add 10 (simple apply mono__pCR) : inO. Local Set Warnings "-cannot-define-projection". Record inNP {X} `{encodable X} (P : X -> Prop) : Prop := @@ -87,16 +89,16 @@ Lemma inNP_intro {X Y} `{_:encodable X} `{encodable Y} `{@encInj Y _} {_:decodab -> polyCertRel P R -> inNP P. Proof. - cbn. intros decode__comp R__comp R__bound. eexists (fun x y => exists y', y = enc y' /\ R x y'). 2:{ exists (fun x => p__pCR R__bound x * c__termsize). - 3,4:solve [smpl_inO]. - -intros x y' (y&->&Hy). now eapply sound__pCR. - -intros x ?. edestruct (complete__pCR R__bound) as (y&?&?). easy. + - intros x y' (y&->&Hy). now eapply sound__pCR. + - intros x ?. edestruct (complete__pCR R__bound) as (y&?&?). easy. exists (enc y);split. easy. - rewrite size_term_enc. unfold c__termsize, c__natsizeS. lia. + rewrite size_term_enc. unfold c__termsize, c__natsizeS. easy. + - smpl_inO. + - solve_proper. } { (*TODO: simplify*) destruct R__comp as (t__f&[R__comp]&?&mono_t__f). @@ -115,10 +117,10 @@ Proof. *eapply decode_correct2 in H3 as <-. remember (size (enc a) + size (enc (enc y)) + 4) as n eqn:eqn. rewrite (mono_t__f _ n). 2:subst n;rewrite <- size_term_enc_r;lia. - rewrite (mono__polyTC _ (x':=n)). 2:lia. + setoid_replace (size (enc (enc y))) with n using relation le by easy. unfold t__f';reflexivity. - *rewrite (mono__polyTC _ (x':=(size (enc a) + size (enc b) + 4))). 2:lia. - unfold t__f'. lia. + * setoid_replace (size (enc b)) with (size (enc a) + size (enc b) + 4) using relation le at 1 by easy. + now unfold t__f'. +unfold f'. intros [x]. cbn. destruct decode as [y| ] eqn:H'. *etransitivity. 2:unshelve eapply correct__decInTime;easy. cbn. @@ -127,9 +129,9 @@ Proof. --cbn. enough (y = y') by congruence. eapply inj_enc. congruence. --eauto. *split. 2:eauto. - intros (?&->&?). rewrite decode_correct in H'. easy. - -unfold t__f'. smpl_inO. - -unfold t__f'. smpl_inO. + intros (?&->&?). rewrite decode_correct in H'. easy. + - unfold t__f'. smpl_inO. + - unfold t__f'. solve_proper. } Qed. @@ -148,17 +150,18 @@ Proof. split. { destruct H1 as [H1]. destruct H1. constructor. exists (fun (p : X * unit) => let (x , _) := p in f__decInTime x). - + extract. solverec. unfold monotonic in H3. - rewrite H3 with (x' := size (enc (a, tt))). 2: { rewrite size_prod; cbn; lia. } + + extract. solverec. + setoid_replace (size (enc a)) with (size (enc (a, tt))) using relation le. 2: { rewrite size_prod. now cbn. } [f']: intros n. subst f'. cbn. generalize (size (enc (a, tt))). intros; reflexivity. + intros [x ?]. cbn. apply correct__decInTime. } - split; subst f'; smpl_inO. + split; subst f'; [smpl_inO | solve_proper]. - exists (fun n => size (enc tt)). - 3, 4: smpl_inO. + intros x _. easy. - + intros x H2. exists tt. easy. + + intros x H2. exists tt. easy. + + smpl_inO. + + easy. Qed. (** ** Poly Time Reduction*) @@ -189,10 +192,11 @@ Qed. Lemma reducesPolyMO_reflexive X {regX : encodable X} (P : X -> Prop) : P ⪯p P. Proof. eapply reducesPolyMO_intro with (f := fun x => x). 2:easy. - exists (fun _ => 1). 4:exists (fun x => x). - 2,3,5,6:solve [ smpl_inO]. - -extract. solverec. - -reflexivity. + exists (fun _ => 1). + - extract. solverec. + - smpl_inO. + - easy. + - exists (fun x => x); [reflexivity | smpl_inO | solve_proper]. Qed. Lemma reducesPolyMO_transitive X Y Z {regX : encodable X} {regY : encodable Y} {regZ : encodable Z} @@ -206,12 +210,12 @@ Proof. exists (fun x => time__polyTC f__c x + time__polyTC g__c (resSize__rSP f__c x) + 1). -extract. solverec. erewrite (mono__polyTC g__c). 2:now apply bounds__rSP . reflexivity. - -smpl_inO. eapply inOPoly_comp. all:smpl_inO. - -smpl_inO. + - smpl_inO. eapply inOPoly_comp; [solve_proper | smpl_inO | smpl_inO]. + - solve_proper. -exists (fun x => resSize__rSP g__c (resSize__rSP f__c x)). +intros. rewrite (bounds__rSP g__c), (mono__rSP g__c). 2:apply (bounds__rSP f__c). easy. - +eapply inOPoly_comp. all:smpl_inO. - +eapply monotonic_comp. all:smpl_inO. + + eapply inOPoly_comp; [solve_proper | smpl_inO | smpl_inO]. + + solve_proper. Qed. Lemma red_inNP X Y `{regX : encodable X} `{regY : encodable Y} (P : X -> Prop) `(Q : Y -> Prop) : @@ -219,33 +223,33 @@ Lemma red_inNP X Y `{regX : encodable X} `{regY : encodable Y} (P : X -> Prop) ` Proof. intros [f f__comp f__correct] [R polyR certR]. exists (fun x z => R (f x) z). - -(* destruct (polyRes__polyTC f__comp) as (size__f&Hsize__f&?&mono__sizef). *) - destruct polyR as (time__R&[R__comp]&inO__timeR&mono__timeR). + -destruct polyR as (time__R&[R__comp]&inO__timeR&mono__timeR). evar (time : nat -> nat). [time]:intros n. exists time. split. - (*eexists (fun n => cnst n (*)polyTimeC__t n*) + time__R (time__polyTC f__comp (size__f n + n)) + 7). split.*) +split. exists (fun '(x,z)=> f__decInTime R__comp (f x,z)). *extract. solverec. all:rewrite !LProd.size_prod. all:cbn [fst snd]. set (n0:=size (enc a) + size (enc b) + 4). - rewrite (mono__polyTC _ (x':=n0)). 2:subst n0;nia. + setoid_replace (size (enc a)) with n0 using relation le by easy. erewrite (mono__timeR _ _). - 2:{ rewrite (bounds__rSP f__comp), (mono__rSP f__comp (x':=n0)). 2:unfold n0;lia. instantiate (1:=resSize__rSP f__comp n0 + n0). unfold n0;try lia. } + 2: { + rewrite (bounds__rSP f__comp). + setoid_replace (size (enc a)) with n0 using relation le by easy. + instantiate (1:=resSize__rSP f__comp n0 + n0). unfold n0;try lia. + } unfold time. reflexivity. *intros [x c]. cbn. rewrite <- correct__decInTime;cbn. easy. - +unfold time;split;smpl_inO. - { eapply inOPoly_comp. all:smpl_inO. } + +unfold time; split. + * smpl_inO. eapply inOPoly_comp; [easy | smpl_inO | smpl_inO]. + * solve_proper. -clear - certR f__correct f__comp. exists (fun x => p__pCR certR (resSize__rSP f__comp x)). +intros ? ? ?%(sound__pCR certR);cbn. now apply f__correct. +intros x Hx;cbn. apply f__correct in Hx. edestruct (complete__pCR certR) as (?&?&?). eauto. eexists;split. easy. rewrite H0. cbn. apply mono__pCR. apply bounds__rSP. - +apply inOPoly_comp;smpl_inO. - +smpl_inO. + + apply inOPoly_comp; [solve_proper | smpl_inO | smpl_inO]. + + solve_proper. Qed. - - - (** ** NP Hardness and Completeness *) Definition NPhard X `{encodable X} (P : X -> Prop) := forall Y `(encodableP Y) (Q:Y -> Prop), @@ -265,10 +269,11 @@ Corollary NPhard_sig X `{encodable X} vX `(P : X -> Prop): Proof. eapply red_NPhard. eapply reducesPolyMO_intro with (f := fun x => proj1_sig x). 2:easy. - exists (fun _ => 2). 4:exists (fun x => x). - 2,3,5,6:solve [ smpl_inO]. - -extract. solverec. - -reflexivity. + exists (fun _ => 2). + - extract. solverec. + - apply inOPoly_c. + - apply monotonic_c. + - exists (fun x => x); [easy | smpl_inO | easy]. Qed. Definition NPcomplete X `{encodable X} (P : X -> Prop) := diff --git a/theories/Complexity/ONotation.v b/theories/Complexity/ONotation.v index f8991d0f..689c7b5d 100644 --- a/theories/Complexity/ONotation.v +++ b/theories/Complexity/ONotation.v @@ -13,16 +13,16 @@ Notation " f ∈O g" := (inO f g) (at level 70). Instance inO_PreOrder : PreOrder inO. Proof. split. - -exists 1,0. intros. Lia.lia. + -exists 1,0. intros. lia. -intros f g h (c&n0&H) (c'&n0'&H'). exists (c*c'),(max n0 n0'). intros n Hn. - rewrite H,H'. all:Lia.lia. + rewrite H,H'. all: lia. Qed. #[export] -Instance inO_pointwise_leq : Proper ( Basics.flip (pointwise_relation _ le) ==> (pointwise_relation _ le) ==> Basics.impl) inO. +Instance inO_pointwise_leq : Proper ((pointwise_relation _ le) --> (pointwise_relation _ le) ==> Basics.impl) inO. Proof. intros ? ? R1 ? ? R2. unfold inO. hnf in R1,R2|-*. setoid_rewrite R1. setoid_rewrite R2. easy. @@ -94,8 +94,6 @@ Qed. Smpl Create inO. -Smpl Add 11 (smpl monotonic) : inO. - Smpl Add 10 (first [ simple eapply inO_add_l | simple eapply inO_mul_c_l | simple eapply inO_mul_c_r | progress (eapply inO_c) | reflexivity]) (* | simple eapply inO_c with (n0:=1);intro;try rewrite <- !f_geq_n;Lia.nia | inO_leq 1])*) : inO. @@ -114,7 +112,7 @@ Qed. Lemma inO_comp_l f1 f2 g1 g2: f1 ∈O g1 -> f2 ∈O g2 -> - monotonic f1 -> + Proper (le ==> le) f1 -> (forall x, x <= g2 x ) -> (forall c, (fun x => g1 (c*x)) ∈O g1) -> (fun n => f1 (f2 n)) ∈O (fun n => g1 (g2 n)). Proof. @@ -216,7 +214,7 @@ Proof. apply inOPoly_c. Qed. -Lemma inOPoly_comp f1 f2: monotonic f1 -> inOPoly f1 -> inOPoly f2 -> inOPoly (fun x => f1 (f2 x)). +Lemma inOPoly_comp f1 f2: Proper (le ==> le) f1 -> inOPoly f1 -> inOPoly f2 -> inOPoly (fun x => f1 (f2 x)). Proof. intros ? (n1&?) (n2&?). exists ((max 1 n2)*n1). @@ -258,4 +256,4 @@ Qed. Instance inOPoly_pointwise_eq: Proper ((pointwise_relation _ eq) ==> iff) inOPoly. Proof. unfold inOPoly. intros ? ? R1. hnf. setoid_rewrite R1. easy. -Qed. +Qed. \ No newline at end of file diff --git a/theories/Complexity/PolyTimeComputable.v b/theories/Complexity/PolyTimeComputable.v index a2f38507..737f7276 100644 --- a/theories/Complexity/PolyTimeComputable.v +++ b/theories/Complexity/PolyTimeComputable.v @@ -11,7 +11,9 @@ Proof. {intros x. rewrite (bounds__rSP Hg). setoid_rewrite mono__rSP. 2:now apply (bounds__rSP Hf). set (n0:=size _). unfold fsize. reflexivity. } - 1,2:now unfold fsize;smpl_inO;eapply inOPoly_comp;smpl_inO. + - unfold fsize. + apply inOPoly_comp; [apply mono__rSP | apply poly__rSP | apply poly__rSP]. + - unfold fsize. solve_proper. Qed. Lemma polyTimeComputable_composition X Y Z `{encodable X} `{encodable Y} `{encodable Z} (f:X-> Y) (g : Y -> Z): @@ -23,11 +25,13 @@ Proof. {extract. solverec. setoid_rewrite mono__polyTC at 2. 2:now apply (bounds__rSP Hf). set (size (enc x)). unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO;eapply inOPoly_comp;smpl_inO. - eapply resSizePoly_composition. all:eauto using resSize__polyTC. + - unfold time. smpl_inO. + apply inOPoly_comp; [apply mono__polyTC | apply poly__polyTC | apply poly__rSP]. + - unfold time. solve_proper. + - eapply resSizePoly_composition. + all: apply resSize__polyTC; assumption. Qed. - Lemma resSizePoly_composition2 X Y1 Y2 Z `{encodable X} `{encodable Y1} `{encodable Y2} `{encodable Z} (f1:X-> Y1) (f2:X-> Y2) (g : Y1 -> Y2 -> Z): resSizePoly f1 -> resSizePoly f2 -> resSizePoly (fun y => g (fst y) (snd y)) -> resSizePoly (fun x => g (f1 x) (f2 x)). @@ -39,7 +43,8 @@ Proof. 2:{ rewrite LProd.size_prod;cbn. rewrite (bounds__rSP Hf1). now rewrite (bounds__rSP Hf2). } set (n0:=size _). unfold fsize. reflexivity. } - 1,2:now unfold fsize;smpl_inO;eapply inOPoly_comp;smpl_inO. + - unfold fsize. apply inOPoly_comp; [apply mono__rSP | apply poly__rSP | smpl_inO]. + - unfold fsize. solve_proper. Qed. Lemma polyTimeComputable_composition2 X Y1 Y2 Z `{encodable X} `{encodable Y1} `{encodable Y2} `{encodable Z} @@ -55,11 +60,13 @@ Proof. 2:{ rewrite LProd.size_prod;cbn. rewrite (bounds__rSP Hf1). now rewrite (bounds__rSP Hf2). } set (size (enc x)). unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO;eapply inOPoly_comp;smpl_inO. - eapply resSizePoly_composition2. all:eauto using resSize__polyTC. + - unfold time. smpl_inO. + apply inOPoly_comp; [apply mono__polyTC | apply poly__polyTC | smpl_inO]. + - unfold time. solve_proper. + - eapply resSizePoly_composition2. + all: apply resSize__polyTC; assumption. Qed. - Lemma resSizePoly_prod X Y Z `{encodable X} `{encodable Y} `{encodable Z} (f:X-> Y) (g : X -> Z): resSizePoly f -> resSizePoly g -> resSizePoly (fun x => (f x, g x)). Proof. @@ -70,7 +77,8 @@ Proof. rewrite (bounds__rSP Hf),(bounds__rSP Hg). set (n0:=size _). unfold fsize. reflexivity. } - 1,2:now unfold fsize;smpl_inO;eapply inOPoly_comp;smpl_inO. + - unfold fsize. smpl_inO. + - unfold fsize. solve_proper. Qed. Lemma polyTimeComputable_prod X Y Z `{encodable X} `{encodable Y} `{encodable Z} (f:X-> Y) (g : X -> Z): @@ -81,8 +89,9 @@ Proof. exists time. {extract. solverec. set (size (enc x)). unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO;eapply inOPoly_comp;smpl_inO. - eapply resSizePoly_prod. all:eauto using resSize__polyTC. + - unfold time. smpl_inO. + - unfold time. solve_proper. + - apply resSizePoly_prod; apply resSize__polyTC; assumption. Qed. @@ -248,10 +257,11 @@ Proof. eexists time. {extract. solverec. rewrite LProd.size_prod. cbn - [mult c__mult1]. rewrite !LNat.size_nat_enc. [time]:exact (fun n => n*n). unfold time, c__mult1, mult_time, c__mult, c__natsizeO, c__natsizeS, c__add1, c__add. nia. } - 1,2:unfold time;now smpl_inO. - eexists (fun n => n*n). all:unfold time. 2,3:now smpl_inO. - intros []. rewrite LProd.size_prod,!LNat.size_nat_enc. cbn. - unfold c__natsizeS, c__natsizeO. lia. + - unfold time. smpl_inO. + - unfold time. solve_proper. + - eexists (fun n => n*n); [ | smpl_inO | solve_proper]. + intros []. rewrite LProd.size_prod,!LNat.size_nat_enc. cbn. + unfold c__natsizeS, c__natsizeO. lia. Qed. Smpl Add 5 simple apply pTC_mult : polyTimeComputable. @@ -280,9 +290,10 @@ Proof. rewrite !LNat.size_nat_enc. [time]:exact (fun n => n*n). unfold time. cbn. unfold max_time, c__max2, c__natsizeS, c__natsizeO. nia. } - 1,2:unfold time;now smpl_inO. - eexists (fun n => n*n). all:unfold time. 2,3:now smpl_inO. - intros []. rewrite LProd.size_prod,!LNat.size_nat_enc. cbn. lia. + - unfold time. smpl_inO. + - unfold time. solve_proper. + - eexists (fun n => n*n); [ | smpl_inO | solve_proper]. + intros []. rewrite LProd.size_prod,!LNat.size_nat_enc. lia. Qed. Smpl Add 5 simple apply pTC_max : polyTimeComputable. diff --git a/theories/Complexity/Subtypes.v b/theories/Complexity/Subtypes.v index 93857685..fbff487f 100644 --- a/theories/Complexity/Subtypes.v +++ b/theories/Complexity/Subtypes.v @@ -14,20 +14,26 @@ Lemma polyTimeComputable_sig_in X Y `(encodable X) `(encodable Y) P f' (f:{x:X|P -> polyTimeComputable f' -> polyTimeComputable f. Proof. - intros Hext [time Hcomp]. exists (fun x => time x +2). 2,3:solve [smpl_inO]. + intros Hext [time Hcomp]. exists (fun x => time x +2). - apply computableTimeExt with (x:=fun x => f' (proj1_sig x)) (x':=f). + intros []; cbn. apply Hext. + extract. solverec. reflexivity. - - eexists (resSize__rSP resSize__polyTC). 2,3:solve [smpl_inO]. - intros []. rewrite <- Hext. rewrite bounds__rSP, enc_sig_exist_eq. reflexivity. + - smpl_inO. + - solve_proper. + - eexists (resSize__rSP resSize__polyTC). + + intros []. rewrite <- Hext. rewrite bounds__rSP, enc_sig_exist_eq. reflexivity. + + apply poly__rSP. + + apply mono__rSP. Qed. Lemma polyTimeComputable_sig_out X Y {RX: encodable X} {RY:encodable Y} validY (f : X -> {y:Y | validY y}): polyTimeComputable (fun x => proj1_sig (f x)) -> polyTimeComputable f. Proof. - intros H. exists (time__polyTC H). 2,3:now smpl_inO. + intros H. exists (time__polyTC H). - computable_casted_result. eauto. + - apply poly__polyTC. + - apply mono__polyTC. - exists (resSize__rSP H). 2,3:now smpl_inO. intro. rewrite <- bounds__rSP, enc_sig_eq. reflexivity. Qed. @@ -38,12 +44,11 @@ Lemma reducesPolyMO_intro_restrictBy_out X Y `{RX: encodable X} `{RY:encodable Y -> (forall x , {Hfx : validY (f x) | P x <-> Q (f x)}) -> P ⪯p restrictBy validY Q. Proof. - intros H H'. unshelve eexists (fun x => exist _ (f x) (proj1_sig (H' x))). + intros H H'. exists (fun x => exist _ (f x) (proj1_sig (H' x))). - now apply polyTimeComputable_sig_out. - - intros x. all:now edestruct H'. + - intros x. all: now destruct H'. Qed. - Lemma reducesPolyMO_intro_restrictBy_in X Y `{RX: encodable X} `{RY:encodable Y} (validX P : X -> Prop) Q (f:X -> Y): polyTimeComputable f diff --git a/theories/Complexity/UpToCPoly.v b/theories/Complexity/UpToCPoly.v index fa36840d..ec9cf18f 100644 --- a/theories/Complexity/UpToCPoly.v +++ b/theories/Complexity/UpToCPoly.v @@ -47,12 +47,14 @@ Record isPoly (X : Type) `{encodable X} (f : X -> nat) : Set := isP__poly : nat -> nat; isP__bounds : forall x, f x <= isP__poly (size (enc x)); isP__inOPoly : inOPoly isP__poly; - isP__mono : monotonic isP__poly; + isP__mono : Proper (le ==> le) isP__poly; }. Arguments isP__bounds {X} {H} {_} _. Arguments isP__poly {X} {H} {_} _. -Smpl Add 15 apply isP__mono : inO. +#[global] Instance mono_isP__poly X `{encodable X} (f: X -> nat) (polyf: isPoly f): + Proper (le ==> le) (isP__poly polyf). +Proof. apply isP__mono. Qed. Smpl Add 15 apply isP__inOPoly : inO. Tactic Notation "rewpoly" constr(s) := @@ -79,48 +81,6 @@ Tactic Notation "replace_le" constr(s) "with" constr(r) := From Undecidability.L.Datatypes Require Import Lists LNat. -(** useful lemmas *) -#[export] -Instance proper_lt_mul : Proper (lt ==> eq ==> le) Nat.mul. -Proof. - intros a b c d e f. nia. -Qed. - -#[export] -Instance proper_lt_add : Proper (lt ==> eq ==> le) Nat.add. -Proof. - intros a b c d e f. nia. -Qed. - -#[export] -Instance proper_le_pow : Proper (le ==> eq ==> le) Nat.pow. -Proof. - intros a b H1 d e ->. apply Nat.pow_le_mono_l, H1. -Qed. - -#[export] -Instance mult_lt_le : Proper (eq ==> lt ==> le) mult. -Proof. - intros a b -> d e H. nia. -Qed. - -#[export] -Instance add_lt_lt : Proper (eq ==> lt ==> lt) Nat.add. -Proof. - intros a b -> c d H. lia. -Qed. - -#[export] -Instance le_lt_impl : Proper (le --> eq ==> Basics.impl) lt. -Proof. - intros a b H d e ->. unfold Basics.flip in H. unfold Basics.impl. lia. -Qed. - -#[export] -Instance lt_le_impl : Proper (lt --> eq ==> Basics.impl) le. -Proof. - intros a b H d e ->. unfold Basics.flip in H. unfold Basics.impl. lia. -Qed. Lemma list_el_size_bound {X : Type} `{encodable X} (l : list X) (a : X) : a el l -> size(enc a) <= size(enc l). diff --git a/theories/L/ComparisonTimeBoundDerivation.v b/theories/L/ComparisonTimeBoundDerivation.v index 8963ecf8..717dd1fc 100644 --- a/theories/L/ComparisonTimeBoundDerivation.v +++ b/theories/L/ComparisonTimeBoundDerivation.v @@ -94,9 +94,11 @@ Instance term_evalVar : computableTime' evalVar (fun a _ => (1, fun v _ => (eval } unfold poly__evalVar. solverec. Qed. - Lemma evalVar_poly : inOPoly poly__evalVar /\ monotonic poly__evalVar. - Proof. unfold poly__evalVar; split; smpl_inO. Qed. + Lemma evalVar_poly : inOPoly poly__evalVar. + Proof. unfold poly__evalVar; smpl_inO. Qed. Smpl Add apply evalVar_poly : inO. + #[export] Instance evalVar_mono: Proper (le ==> le) poly__evalVar. + Proof. unfold poly__evalVar. solve_proper. Qed. (** evalLiteral *) @@ -114,9 +116,11 @@ Instance term_evalLiteral : computableTime' evalLiteral (fun a _ => (1, fun l _ unfold evalLiteral_time. destruct l as [s v]. rewrite evalVar_time_bound. unfold poly__evalLiteral; solverec. Qed. - Lemma evalLiteral_poly : inOPoly poly__evalLiteral /\ monotonic poly__evalLiteral. - Proof. unfold poly__evalLiteral; split; smpl_inO. Qed. + Lemma evalLiteral_poly : inOPoly poly__evalLiteral. + Proof. unfold poly__evalLiteral; smpl_inO. Qed. Smpl Add apply evalLiteral_poly : inO. + #[export] Instance evalLiteral_mono: Proper (le ==> le) poly__evalLiteral. + Proof. unfold poly__evalLiteral. solve_proper. Qed. Section fixX. Context {X : Type} `{encodable X}. @@ -164,12 +168,15 @@ Instance term_evalClause : computableTime' evalClause (fun a _ => (1, fun C _ => unfold evalClause_time. rewrite existsb_time_explicit. rewrite sumn_map_mono. 2:{ intros. rewrite evalLiteral_time_bound at 1. instantiate (1 := fun _ => _); cbn; reflexivity. } rewrite sumn_map_const. rewrite list_size_length. - poly_mono evalLiteral_poly. 2: replace_le (size (enc a)) with (size (enc a) + size (enc C)) by lia at 1; reflexivity. + setoid_replace (size (enc a)) with (size (enc a) + size (enc C)) + using relation le at 1 by easy. unfold poly__evalClause; lia. Qed. - Lemma evalClause_poly : monotonic poly__evalClause /\ inOPoly poly__evalClause. - Proof. unfold poly__evalClause; split; smpl_inO. Qed. + Lemma evalClause_poly : inOPoly poly__evalClause. + Proof. unfold poly__evalClause; smpl_inO. Qed. Smpl Add apply evalClause_poly : inO. + #[export] Instance evalClause_mono: Proper (le ==> le) poly__evalClause. + Proof. unfold poly__evalClause. solve_proper. Qed. (* evalCnf *) Definition c__evalCnf := 3. @@ -186,14 +193,19 @@ Instance term_evalCnf : computableTime' evalCnf (fun a _ => (1, fun N _ => (eval Proof. unfold evalCnf_time. rewrite forallb_time_explicit. rewrite sumn_map_mono. 2:{ intros. rewrite evalClause_time_bound at 1. - poly_mono evalClause_poly at 1. 2: { rewrite list_el_size_bound with (a := x). 2: apply H. reflexivity. } - instantiate (1 := fun _ => _); cbn; reflexivity. } + instantiate (1 := fun _ => _). + setoid_replace (size (enc x)) with (size (enc N)) using relation le + by now apply list_el_size_bound. + reflexivity. } rewrite sumn_map_const. rewrite list_size_length. unfold poly__evalCnf; lia. Qed. - Lemma evalCnf_poly : monotonic poly__evalCnf /\ inOPoly poly__evalCnf. - Proof. unfold poly__evalCnf; split; smpl_inO. Qed. + + Lemma evalCnf_poly : inOPoly poly__evalCnf. + Proof. unfold poly__evalCnf; smpl_inO. Qed. Smpl Add apply evalCnf_poly : inO. + #[export] Instance evalCnf_mono: Proper (le ==> le) poly__evalCnf. + Proof. unfold poly__evalCnf. solve_proper. Qed. (** sat_verifierb *) Definition c__satVerifierb := 6. @@ -207,11 +219,14 @@ Instance term_sat_verifierb : computableTime' sat_verifierb (fun p _ => (sat_ver Proof. unfold sat_verifierb_time, poly__satVerifierb. destruct p as [N a]. rewrite evalCnf_time_bound. - poly_mono evalCnf_poly. 2: { instantiate (1 := size (enc (N, a))). rewrite size_prod; cbn; lia. } - lia. + setoid_replace (size (enc a) + size (enc N)) with (size (enc (N, a))) + using relation le by (rewrite size_prod; cbn; lia). + reflexivity. Qed. - Lemma sat_verifierb_poly : inOPoly poly__satVerifierb /\ monotonic poly__satVerifierb. - Proof. unfold poly__satVerifierb; split; smpl_inO. Qed. + Lemma sat_verifierb_poly : inOPoly poly__satVerifierb. + Proof. unfold poly__satVerifierb; smpl_inO. Qed. + #[export] Instance sat_verifierb_mono: Proper (le ==> le) poly__satVerifierb. + Proof. unfold poly__satVerifierb. solve_proper. Qed. (** We obtain that SAT is in NP *) @@ -227,7 +242,8 @@ Instance term_sat_verifierb : computableTime' sat_verifierb (fun p _ => (sat_ver intros cn a H. cbn. exists a; tauto. - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split. + apply compressAssignment_cnf_equiv in H. cbn. apply H. - + apply assignment_small_size. cbn. apply compressAssignment_small. + + apply assignment_small_size, compressAssignment_small. + - solve_proper. } unfold inTimePoly. exists poly__satVerifierb. repeat split. @@ -236,7 +252,8 @@ Instance term_sat_verifierb : computableTime' sat_verifierb (fun p _ => (sat_ver cbn. intros [N a] _. split; [ | easy]. apply sat_verifierb_time_bound. + intros [N a]. cbn. apply sat_verifierb_correct. } - all: apply sat_verifierb_poly. + - apply sat_verifierb_poly. + - solve_proper. Qed. End explicit_bounds. End explicit_bounds. @@ -397,12 +414,13 @@ Instance term_sat_verifierb : computableTime' sat_verifierb _ := projT2 _term_sa 1 : apply linDec_polyTimeComputable. 2 : { exists (fun n => n * (1 + c__listsizeCons + c__listsizeNil)). - 3, 4: smpl_inO. + 3: smpl_inO. - unfold SAT, sat_verifier. intros cn a H. cbn. exists a; tauto. - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split. + apply compressAssignment_cnf_equiv in H. cbn. apply H. - + apply assignment_small_size. cbn. apply compressAssignment_small. + + apply assignment_small_size, compressAssignment_small. + - solve_proper. } unfold inTimePoly. exists_poly p. repeat split. @@ -418,7 +436,8 @@ Instance term_sat_verifierb : computableTime' sat_verifierb _ := projT2 _term_sa all: rewrite size_prod; cbn; lia. + intros [N a]. cbn. apply sat_verifierb_correct. } - all: subst p; smpl_inO. + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. End uptoc_pure. End uptoc_pure. @@ -529,7 +548,8 @@ Instance term_evalClause : computableTime' evalClause _ := projT2 _term_evalClau { intros (a & C). unfold evalClause_time. rewrite !list_size_length. rewrite maxSize_enc_size. rewrite size_prod. cbn. [p] : exact (n * n * n). and_solve p. } - all: subst p; smpl_inO. + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. Arguments evalClause_time: simpl never. @@ -567,7 +587,8 @@ Instance term_evalCnf : computableTime' evalCnf _ := projT2 _term_evalCnf. rewrite sumn_map_const. rewrite list_size_length. replace_le (size (enc N)) with (size (enc (a, N))) by rewrite size_prod; cbn; lia. set (size _). and_solve p. } - all: subst p; smpl_inO. + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. (** sat_verifierb *) @@ -591,13 +612,14 @@ Instance term_sat_verifierb : computableTime' sat_verifierb _ := projT2 _term_sa 1 : apply linDec_polyTimeComputable. 2 : { exists (fun n => n * (1 + c__listsizeCons + c__listsizeNil)). - 3, 4: smpl_inO. + 3: smpl_inO. - unfold SAT, sat_verifier. intros cn a H. cbn. exists a; tauto. - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split. + apply compressAssignment_cnf_equiv in H. cbn. apply H. - + apply assignment_small_size. cbn. apply compressAssignment_small. - } + + apply assignment_small_size, compressAssignment_small. + - solve_proper. + } unfold inTimePoly. exists_poly p. repeat split. { exists (sat_verifierb). @@ -607,7 +629,8 @@ Instance term_sat_verifierb : computableTime' sat_verifierb _ := projT2 _term_sa set (L_facts.size _). [p]: intros n. and_solve p. + intros [N a]. cbn. apply sat_verifierb_correct. } - all: subst p; smpl_inO. + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. End uptoc_mixed. diff --git a/theories/L/Datatypes/LBinNums.v b/theories/L/Datatypes/LBinNums.v index 22ff5b48..22a084b0 100644 --- a/theories/L/Datatypes/LBinNums.v +++ b/theories/L/Datatypes/LBinNums.v @@ -7,7 +7,7 @@ MetaCoq Run (tmGenEncode "positive_enc" positive). #[export] Hint Resolve positive_enc_correct : Lrewrite. -Global Instance termT_Pos_xI : computableTime' xI (fun x _ => (1,tt)). +Global Instance termT_Pos_xI : computableTime xI (fun x _ => (1,tt)). extract constructor. solverec. Qed. diff --git a/theories/L/Datatypes/LNat.v b/theories/L/Datatypes/LNat.v index a53dc704..972dcc58 100644 --- a/theories/L/Datatypes/LNat.v +++ b/theories/L/Datatypes/LNat.v @@ -1,5 +1,10 @@ From Undecidability.L.Datatypes Require Export LNat. +Fact nat_size_mul a b: size (enc (a * b)) <= size (enc a) * size (enc b). +Proof. + rewrite !size_nat_enc. unfold c__natsizeS. nia. +Qed. + Definition c__sqrt_iter := 5. Definition sqrt_iter_time (k p q r: nat) := 4 + 20 * k. #[global] Instance termT_sqrt_iter: diff --git a/theories/L/TM/TMflatComp.v b/theories/L/TM/TMflatComp.v index e4ca73c1..6659c34e 100644 --- a/theories/L/TM/TMflatComp.v +++ b/theories/L/TM/TMflatComp.v @@ -491,10 +491,10 @@ Proof. +destruct v. easy. Qed. -Lemma execFlat_poly : {f : nat -> nat & (forall M t k, execFlatTM_time M t k <= f (size (enc M) +t + k)) /\ inOPoly f /\ monotonic f}. +Lemma execFlat_poly : {f : nat -> nat & (forall M t k, execFlatTM_time M t k <= f (size (enc M) +t + k)) /\ inOPoly f /\ Proper (le ==> le) f}. Proof. unfold execFlatTM_time,isValidFlatTM_time,time_isValidFlatTrans,isInjFinfuncTable_time,allSameEntry_time,loopMflat_timeNice,haltConfFlat_time,isValidFlatTapes_time,isValidFlatTape_time,stepFlat_timeNice. - eexists (fun x => _). split. + eexists (fun x => _). repeat split. { intros M t k. remember ( (size (enc M) + t + k)) as x. @@ -525,5 +525,6 @@ Proof. rewrite Hk. clear. reflexivity. } - split. all:smpl_inO. + - smpl_inO. + - solve_proper. Qed. diff --git a/theories/Libs/CookPrelim/FlatFinTypes.v b/theories/Libs/CookPrelim/FlatFinTypes.v index f87b9163..4ed97a71 100644 --- a/theories/Libs/CookPrelim/FlatFinTypes.v +++ b/theories/Libs/CookPrelim/FlatFinTypes.v @@ -361,10 +361,10 @@ Lemma ofFlatType_dec_time_bound sig e: ofFlatType_dec_time sig e <= poly__ofFlat Proof. unfold ofFlatType_dec_time. rewrite leb_time_bound_r. unfold poly__ofFlatTypeDec, c__ofFlatTypeDecBound; nia. Qed. -Lemma ofFlatType_dec_poly : monotonic poly__ofFlatTypeDec /\ inOPoly poly__ofFlatTypeDec. -Proof. - split; unfold poly__ofFlatTypeDec; smpl_inO. -Qed. +Lemma ofFlatType_dec_poly : inOPoly poly__ofFlatTypeDec. +Proof. unfold poly__ofFlatTypeDec; smpl_inO. Qed. +#[export] Instance ofFlatType_dec_mono: Proper (le ==> le) poly__ofFlatTypeDec. +Proof. unfold poly__ofFlatTypeDec. solve_proper. Qed. (*list_ofFlatType_dec *) Definition c__listOfFlatTypeDec := 3. @@ -383,16 +383,19 @@ Proof. erewrite forallb_time_bound_env. 2: { split; [ intros | ]. - - rewrite (ofFlatType_dec_time_bound y a). poly_mono ofFlatType_dec_poly. - 2: apply Nat.le_add_l with (n := size(enc y)). reflexivity. - - apply ofFlatType_dec_poly. + - rewrite (ofFlatType_dec_time_bound y a). + setoid_replace (size (enc y)) with (size (enc a) + size (enc y)) using relation le at 1 by apply Nat.le_add_l. + reflexivity. + - solve_proper. } rewrite list_size_length. replace_le (size(enc l)) with (size (enc t) + size (enc l)) by lia at 1. setoid_rewrite Nat.add_comm at 5. unfold poly__listOfFlatTypeDec, c__listOfFlatTypeDecBound. nia. Qed. -Lemma list_ofFlatType_dec_poly : monotonic poly__listOfFlatTypeDec /\ inOPoly poly__listOfFlatTypeDec. +Lemma list_ofFlatType_dec_poly : inOPoly poly__listOfFlatTypeDec. Proof. - split; unfold poly__listOfFlatTypeDec; smpl_inO; apply ofFlatType_dec_poly. -Qed. + unfold poly__listOfFlatTypeDec. smpl_inO. apply ofFlatType_dec_poly. +Qed. +#[export] Instance list_ofFlatType_dec_mono: Proper (le ==> le) poly__listOfFlatTypeDec. +Proof. unfold poly__listOfFlatTypeDec. solve_proper. Qed. diff --git a/theories/Libs/CookPrelim/MorePrelim.v b/theories/Libs/CookPrelim/MorePrelim.v index 7cd6410c..3ee3fdb3 100644 --- a/theories/Libs/CookPrelim/MorePrelim.v +++ b/theories/Libs/CookPrelim/MorePrelim.v @@ -349,7 +349,12 @@ Proof. * eauto. * right; now apply IHl. - rewrite IHl. split; intros H; [ eauto | now destruct H]. -Qed. +Qed. + +Lemma filterSome_length (X : Type) (l : list (option X)) : |filterSome l| <= |l|. +Proof. + induction l; cbn; [lia | destruct a; cbn; lia]. +Qed. (*an actually usable version of the lemma without useless bool2Prop stuff *) Lemma in_filter_iff (X : Type) (x : X) (p : X -> bool) (A : list X): x el filter p A <-> x el A /\ p x = true. diff --git a/theories/Libs/CookPrelim/PolyBounds.v b/theories/Libs/CookPrelim/PolyBounds.v index 84cd56f3..b9041acc 100644 --- a/theories/Libs/CookPrelim/PolyBounds.v +++ b/theories/Libs/CookPrelim/PolyBounds.v @@ -23,18 +23,7 @@ Proof. induction l; cbn -[Nat.add Nat.mul]. - lia. - unfold concat_time in IHl. rewrite IHl. lia. -Qed. - -Tactic Notation "poly_mono" constr(H) "at" ne_integer_list(occ) := - let He := fresh in specialize H as He; match type of He with - | _ /\ monotonic _ => unfold monotonic in He; setoid_rewrite (proj2 He) at occ - | monotonic _ /\ _ => unfold monotonic in He; setoid_rewrite (proj1 He) at occ - end; clear He. -Tactic Notation "poly_mono" constr(H) := - let He := fresh in specialize H as He; match type of He with - | _ /\ monotonic _ => unfold monotonic in He; erewrite (proj2 He) - | monotonic _ /\ _ => unfold monotonic in He; erewrite (proj1 He) - end; clear He. +Qed. Definition c__moduloBound := c__divmod + c__modulo + c__sub. Lemma modulo_time_bound x y: @@ -70,25 +59,28 @@ Section fixXEq. rewrite Nat.le_min_l. unfold poly__listInDecb. rewrite list_size_cons. unfold c__listsizeCons; leq_crossout. Qed. - Lemma list_in_decb_poly : monotonic poly__listInDecb /\ inOPoly poly__listInDecb. - Proof. - unfold poly__listInDecb; split; smpl_inO. - Qed. + + Lemma list_in_decb_poly: inOPoly poly__listInDecb. + Proof. unfold poly__listInDecb. smpl_inO. Qed. + #[export] Instance list_in_decb_mono: Proper (le ==> le) poly__listInDecb. + Proof. unfold poly__listInDecb. solve_proper. Qed. Definition poly__listInclDecb n := n * poly__listInDecb n + (n + 1) * c__list_incl_decb. Lemma list_incl_decb_time_bound (l1 l2 :list X) : list_incl_decb_time l1 l2 <= poly__listInclDecb (size (enc l1) + size (enc l2)). Proof. induction l1; cbn. - unfold poly__listInclDecb. nia. - - rewrite list_in_decb_time_bound. rewrite IHl1. - poly_mono list_in_decb_poly. 2: { instantiate (1 := size (enc (a :: l1)) + size (enc l2)). lia. } - unfold poly__listInclDecb. rewrite list_size_cons at 2 4. - poly_mono list_in_decb_poly at 2. 2 : { instantiate (1 := size (enc (a :: l1)) + size (enc l2)). rewrite list_size_cons. lia. } - unfold c__listsizeCons. nia. - Qed. - Lemma list_incl_decb_poly : monotonic poly__listInclDecb /\ inOPoly poly__listInclDecb. - Proof. - unfold poly__listInclDecb; split; smpl_inO; apply list_in_decb_poly. + - rewrite list_in_decb_time_bound. rewrite IHl1. + setoid_replace (size (enc l2)) with (size (enc (a :: l1)) + size (enc l2)) using relation le at 1 by easy. + unfold poly__listInclDecb. rewrite list_size_cons at 2 4. + setoid_replace ((size (enc l1) + size (enc l2))) with (size (enc (a :: l1)) + size (enc l2)) using relation le at 2. + + unfold c__listsizeCons. nia. + + rewrite list_size_cons. lia. + Qed. + + Lemma list_incl_decb_poly : inOPoly poly__listInclDecb. + Proof. + unfold poly__listInclDecb; smpl_inO; apply list_in_decb_poly. Qed. Definition poly__dupfreeb n := n * poly__listInDecb n + (n + 1) * c__dupfreeb. @@ -96,17 +88,19 @@ Section fixXEq. Proof. induction l; cbn. - unfold poly__dupfreeb; nia. - - rewrite list_in_decb_time_bound. rewrite IHl. - poly_mono list_in_decb_poly. 2: { instantiate (1 := size (enc (a :: l))). rewrite list_size_cons. nia. } - unfold poly__dupfreeb. - poly_mono list_in_decb_poly at 2. 2: { instantiate (1 := size (enc (a :: l))). rewrite list_size_cons. nia. } - rewrite list_size_cons at 3 5. unfold c__listsizeCons. nia. - Qed. - Lemma dupfreeb_poly : monotonic poly__dupfreeb /\ inOPoly poly__dupfreeb. + - rewrite list_in_decb_time_bound. rewrite IHl. + unfold poly__dupfreeb. + setoid_replace (size (enc l)) with (size (enc (a :: l))) using relation le at 1 3 by now rewrite list_size_cons. + rewrite list_size_cons at 3 5. unfold c__listsizeCons. nia. + Qed. + + Lemma dupfreeb_poly : inOPoly poly__dupfreeb. Proof. - unfold poly__dupfreeb; split; smpl_inO; apply list_in_decb_poly. - Qed. -End fixXEq. + unfold poly__dupfreeb; smpl_inO; apply list_in_decb_poly. + Qed. + #[export] Instance dupfreeb_mono: Proper (le ==> le) poly__dupfreeb. + Proof. unfold poly__dupfreeb. solve_proper. Qed. +End fixXEq. Section fixX. Context {X : Type}. @@ -118,15 +112,16 @@ Section fixX. Context {RY : encodable Y}. Lemma forallb_time_bound_env (predT : Y -> X -> nat) (f : nat -> nat): - (forall (a : X) (y : Y), predT y a <= f (size(enc a) + size(enc y))) /\ monotonic f + (forall (a : X) (y : Y), predT y a <= f (size(enc a) + size(enc y))) /\ Proper (le ==> le) f -> forall (l : list X) (y : Y), forallb_time (predT y) l <= (|l| +1) * (f(size (enc l) + size(enc y)) + c__forallb). Proof. intros [H1 H2]. intros. induction l. - cbn. lia. - - cbn. rewrite <- Nat.add_assoc, IHl, H1. unfold monotonic in H2. - rewrite H2 with (x' := size (enc (a :: l)) + size(enc y)). 2: rewrite list_size_cons; nia. - setoid_rewrite H2 with (x' := size(enc (a::l)) + size(enc y)) at 2. 2: rewrite list_size_cons; nia. - nia. + - cbn. rewrite <- Nat.add_assoc, IHl, H1. + setoid_replace (size (enc a) + size (enc y)) with (size (enc (a :: l)) + size(enc y)) using relation le. + setoid_replace (size (enc l) + size (enc y)) with (size(enc (a::l)) + size(enc y)) using relation le. + reflexivity. + all: rewrite list_size_cons; nia. Qed. Lemma nth_error_time_bound : @@ -136,16 +131,16 @@ Section fixX. Qed. Lemma map_time_bound_env (fT : Y -> X -> nat) (f__bound : nat -> nat): - (forall (env : Y) (ele : X), fT env ele <= f__bound (size (enc env) + size (enc ele))) /\ monotonic f__bound + (forall (env : Y) (ele : X), fT env ele <= f__bound (size (enc env) + size (enc ele))) /\ Proper (le ==> le) f__bound -> forall (env : Y) (l : list X), map_time (fT env) l <= (|l| + 1) * (f__bound (size (enc env) + size (enc l)) + 1) * (c__map + 1). Proof. intros [H1 H2] env l. induction l; cbn -[c__map]. - nia. - - rewrite IHl. rewrite H1. unfold monotonic in H2. + - rewrite IHl. rewrite H1. rewrite H2 at 1. 2: (replace_le (size (enc a)) with (size (enc (a::l))) by (rewrite list_size_cons; lia)); reflexivity. setoid_rewrite H2 at 2. 2: (replace_le (size (enc l)) with (size (enc (a::l))) by (rewrite list_size_cons; lia)); reflexivity. - nia. - Qed. + nia. + Qed. Definition poly__concat n := (n + 1) * c__concat. Lemma concat_time_bound (l : list (list X)) : concat_time l <= poly__concat (size (enc l)). @@ -153,11 +148,12 @@ Section fixX. unfold concat_time. induction l; cbn -[Nat.add Nat.mul]. - unfold poly__concat. nia. - rewrite IHl. unfold poly__concat. rewrite list_size_cons. rewrite list_size_length. unfold c__concat, c__listsizeCons; nia. - Qed. - Lemma concat_poly : monotonic poly__concat /\ inOPoly poly__concat. - Proof. - split; unfold poly__concat; smpl_inO. - Qed. + Qed. + + Lemma concat_poly : inOPoly poly__concat. + Proof. unfold poly__concat; smpl_inO. Qed. + #[export] Instance concat_mono: Proper (le ==> le) poly__concat. + Proof. unfold poly__concat. solve_proper. Qed. End fixX. Section fixXY. @@ -167,8 +163,8 @@ Section fixXY. Context {H1 : encodable Z}. Lemma fold_right_time_bound_env (step : Z -> Y -> X -> X) (stepT : Z -> Y -> X -> nat) (f__arg f__size : nat -> nat): - (forall (acc : X) (ele : Y) (env : Z), stepT env ele acc <= f__arg (size (enc acc) + size (enc ele) + size (enc env))) /\ monotonic f__arg - -> (forall (acc : X) (ele : Y) (env : Z), size (enc (step env ele acc)) <= size (enc acc) + f__size (size (enc ele) + size (enc env))) /\ monotonic f__size + (forall (acc : X) (ele : Y) (env : Z), stepT env ele acc <= f__arg (size (enc acc) + size (enc ele) + size (enc env))) /\ Proper (le ==> le) f__arg + -> (forall (acc : X) (ele : Y) (env : Z), size (enc (step env ele acc)) <= size (enc acc) + f__size (size (enc ele) + size (enc env))) /\ Proper (le ==> le) f__size -> forall (l : list Y) (acc : X) (env : Z), fold_right_time (step env) (stepT env) l acc <= (|l| + 1) * f__arg (|l| * f__size (size(enc l) + size (enc env)) + size (enc acc) + size(enc l) + size (enc env)) + (|l| + 1) * c__fold_right. Proof. intros [G1 G2] [F1 F2] l init env. @@ -178,7 +174,7 @@ Section fixXY. intros l' l''. revert l'. induction l''; intros. - cbn. lia. - cbn. rewrite F1. rewrite IHl''. 2: { now rewrite app_comm_cons' in H2. } - unfold monotonic in F2. setoid_rewrite F2 at 2. + setoid_rewrite F2 at 2. 2: (replace_le (size(enc a)) with (size (enc (a::l''))) by (apply list_el_size_bound; eauto)); reflexivity. rewrite F2 at 1. 2: (replace_le (size (enc l'')) with (size (enc (a::l''))) by (rewrite list_size_cons; lia)); reflexivity. nia. @@ -189,7 +185,7 @@ Section fixXY. - cbn -[c__fold_right]. rewrite IHl. clear IHl. 2: { intros. specialize (H3 (a::l') l''). apply H3. rewrite H2. eauto. } rewrite G1. - unfold monotonic in *. erewrite G2. + erewrite G2. 2: { rewrite H3. 2: assert (a::l = [a] ++l) as -> by eauto; easy. erewrite F2. 2: (replace_le (size (enc l)) with (size (enc (a::l))) by (rewrite list_size_cons; lia)); reflexivity. replace_le (size (enc a)) with (size (enc (a::l))) by (rewrite list_size_cons; lia). @@ -216,8 +212,8 @@ Section prodLists_bound. unfold prodLists_time. rewrite !list_size_length. unfold poly__prodLists. solverec. Qed. - Lemma prodLists_poly : monotonic poly__prodLists /\ inOPoly poly__prodLists. - Proof. - unfold poly__prodLists; split; smpl_inO. - Qed. + Lemma prodLists_poly : inOPoly poly__prodLists. + Proof. unfold poly__prodLists; smpl_inO. Qed. + #[export] Instance prodLists_mono: Proper (le ==> le) poly__prodLists. + Proof. unfold poly__prodLists. solve_proper. Qed. End prodLists_bound. diff --git a/theories/NP/Clique/FlatClique.v b/theories/NP/Clique/FlatClique.v index be3e06c5..559ccc74 100644 --- a/theories/NP/Clique/FlatClique.v +++ b/theories/NP/Clique/FlatClique.v @@ -181,11 +181,11 @@ Proof. rewrite list_in_decb_time_bound at 1. instantiate (1 := fun _ => _). cbn. reflexivity. } rewrite sumn_map_const. - rewrite list_size_length. - poly_mono (@list_in_decb_poly (nat * nat) _ _ _ _). 2: { instantiate (1 := size (enc E) + size (enc (a::l))). lia. } - unfold poly__allPairsOfEdgesDecb. - poly_mono (@list_in_decb_poly (nat * nat) _ _ _ _) at 2. 2: { instantiate (1 := size (enc E) + size (enc (a::l))). rewrite list_size_cons. lia. } - rewrite list_size_cons at 3 4 6. + rewrite list_size_length. + setoid_replace (size (enc E)) with (size (enc E) + size (enc (a::l))) using relation le at 1 by easy. + unfold poly__allPairsOfEdgesDecb. + setoid_replace (size (enc E) + size (enc l)) with (size (enc E) + size (enc (a::l))) using relation le at 3 by now rewrite list_size_cons. + rewrite list_size_cons at 3 4 6. (* nia is too dumb to solve this; leq_crossout is smart enough and fast, but produces proof terms which are too large*) replace_le (size (enc l)) with (size (enc E) + size (enc l)) by lia at 1. @@ -194,14 +194,16 @@ Proof. replace (poly__listInDecb (X := nat * nat) (size (enc E) + size (enc (a :: l))) + c__fedgesEdgeInDecb + c__allPairsOfEdgesDecbStep + c__forallb) with (poly__listInDecb (X := nat * nat) (size (enc E) + size (enc (a::l))) + c__allPairsOfEdgesDecbBound1) by (unfold c__allPairsOfEdgesDecbBound1; lia). unfold c__allPairsOfEdgesDecbBound2. - unfold c__listsizeCons. - lia. + unfold c__listsizeCons. + lia. Qed. -Lemma allPairsOfEdges_decb_poly : monotonic poly__allPairsOfEdgesDecb /\ inOPoly poly__allPairsOfEdgesDecb. +Lemma allPairsOfEdges_decb_poly : inOPoly poly__allPairsOfEdgesDecb. Proof. - unfold poly__allPairsOfEdgesDecb; split; smpl_inO; apply list_in_decb_poly. -Qed. - + unfold poly__allPairsOfEdgesDecb; smpl_inO; apply list_in_decb_poly. +Qed. +#[export] Instance allPairsOfEdges_decb_mono: Proper (le ==> le) poly__allPairsOfEdgesDecb. +Proof. unfold poly__allPairsOfEdgesDecb. solve_proper. Qed. + Definition c__isfCliqueDecb := 21. Definition isfClique_decb_time (G : fgraph) (l : list fvertex) := let (V, E) := G in list_ofFlatType_dec_time V l + dupfreeb_time l + allPairsOfEdges_decb_time l E + c__isfCliqueDecb. #[export] @@ -216,17 +218,24 @@ Proof. unfold isfClique_decb_time. destruct G as (V & E). rewrite list_ofFlatType_dec_time_bound. rewrite dupfreeb_time_bound. - rewrite allPairsOfEdges_decb_time_bound. - poly_mono list_ofFlatType_dec_poly. 2: { instantiate (1 := size (enc (V, E)) + size (enc l)). rewrite size_prod; cbn. lia. } - poly_mono (@dupfreeb_poly nat _ _ _ _). 2: { instantiate (1 := size (enc (V, E)) + size (enc l)). rewrite size_prod; cbn. lia. } - poly_mono allPairsOfEdges_decb_poly. 2: { instantiate (1 := size (enc (V, E)) + size (enc l)). rewrite size_prod; cbn. lia. } - unfold poly__isfCliqueDecb; solverec. + rewrite allPairsOfEdges_decb_time_bound. + setoid_replace (size (enc V) + size (enc l)) with (size (enc (V, E)) + size (enc l)) + using relation le by (now rewrite size_prod; cbn). + setoid_replace (size (enc l)) with (size (enc (V, E)) + size (enc l)) + using relation le at 2 by easy. + setoid_replace (size (enc E) + size (enc l)) with (size (enc (V, E)) + size (enc l)) + using relation le by (now rewrite size_prod; cbn). + unfold poly__isfCliqueDecb. solverec. Qed. -Lemma isfClique_decb_poly: monotonic poly__isfCliqueDecb /\ inOPoly poly__isfCliqueDecb. +Lemma isfClique_decb_poly: inOPoly poly__isfCliqueDecb. Proof. - unfold poly__isfCliqueDecb; split; smpl_inO. - all: first [apply list_ofFlatType_dec_poly | apply dupfreeb_poly | apply allPairsOfEdges_decb_poly]. -Qed. + unfold poly__isfCliqueDecb; smpl_inO. + - exact list_ofFlatType_dec_poly. + - apply dupfreeb_poly. + - exact allPairsOfEdges_decb_poly. +Qed. +#[export] Instance isfClique_decb_mono: Proper (le ==> le) poly__isfCliqueDecb. +Proof. unfold poly__isfCliqueDecb. solve_proper. Qed. (** isfKClique_decb *) Definition c__isfKCliqueDecb := 12 + c__length. @@ -248,10 +257,10 @@ Proof. unfold eqbTime. rewrite Nat.le_min_l, list_size_enc_length. unfold poly__isfKCliqueDecb. solverec. Qed. -Lemma isfKClique_decb_poly : monotonic poly__isfKCliqueDecb /\ inOPoly poly__isfKCliqueDecb. -Proof. - unfold poly__isfKCliqueDecb; split; smpl_inO; apply isfClique_decb_poly. -Qed. +Lemma isfKClique_decb_poly : inOPoly poly__isfKCliqueDecb. +Proof. unfold poly__isfKCliqueDecb; smpl_inO; apply isfClique_decb_poly. Qed. +#[export] Instance isfKClique_decb_mono: Proper (le ==> le) poly__isfKCliqueDecb. +Proof. unfold poly__isfKCliqueDecb. solve_proper. Qed. (** fedges_symmetric_decb *) Definition fedges_symmetric_decb_step (E : list fedge) (e : fedge) := let (v1, v2) := e in fedges_edge_in_decb E (v2, v1). @@ -286,10 +295,12 @@ Proof. rewrite sumn_map_const. rewrite list_size_length. unfold poly__fedgesSymmetricDecb. lia. Qed. -Lemma fedges_symmetric_decb_poly : monotonic poly__fedgesSymmetricDecb /\ inOPoly poly__fedgesSymmetricDecb. +Lemma fedges_symmetric_decb_poly : inOPoly poly__fedgesSymmetricDecb. Proof. - unfold poly__fedgesSymmetricDecb; split; smpl_inO; apply list_in_decb_poly. -Qed. + unfold poly__fedgesSymmetricDecb; smpl_inO; apply list_in_decb_poly. +Qed. +#[export] Instance fedges_symmetric_decb_mono: Proper (le ==> le) poly__fedgesSymmetricDecb. +Proof. unfold poly__fedgesSymmetricDecb. solve_proper. Qed. (** fedge_wf_decb *) Definition c__fedgeWfDecb := 2 * c__ltb + 12. @@ -320,10 +331,10 @@ Proof. rewrite size_nat_enc_r with (n := V) at 1. unfold poly__fedgesWfDecb. leq_crossout. Qed. -Lemma fedges_wf_decb_poly : monotonic poly__fedgesWfDecb /\ inOPoly poly__fedgesWfDecb. -Proof. - unfold poly__fedgesWfDecb; split; smpl_inO. -Qed. +Lemma fedges_wf_decb_poly : inOPoly poly__fedgesWfDecb. +Proof. unfold poly__fedgesWfDecb; smpl_inO. Qed. +#[export] Instance fedges_wf_decb_mono: Proper (le ==> le) poly__fedgesWfDecb. +Proof. unfold poly__fedgesWfDecb. solve_proper. Qed. (** fgraph_wf_decb *) Definition c__fgraphWfDecb := 11. @@ -338,15 +349,21 @@ Definition poly__fgraphWfDecb n := poly__fedgesSymmetricDecb n + poly__fedgesWfD Lemma fgraph_wf_decb_time_bound G : fgraph_wf_decb_time G <= poly__fgraphWfDecb (size (enc G)). Proof. unfold fgraph_wf_decb_time. destruct G as (V & E). - rewrite fedges_symmetric_decb_time_bound, fedges_wf_decb_time_bound. - poly_mono fedges_symmetric_decb_poly. 2: { instantiate (1 := size (enc (V, E))). rewrite size_prod; cbn; lia. } - poly_mono fedges_wf_decb_poly. 2: { instantiate (1 := size (enc (V, E))). rewrite size_prod; cbn; lia. } - unfold poly__fgraphWfDecb; lia. -Qed. -Lemma fgraph_wf_decb_poly : monotonic poly__fgraphWfDecb /\ inOPoly poly__fgraphWfDecb. -Proof. - unfold poly__fgraphWfDecb; split; smpl_inO; first [apply fedges_symmetric_decb_poly | apply fedges_wf_decb_poly]. + rewrite fedges_symmetric_decb_time_bound, fedges_wf_decb_time_bound. + setoid_replace (size (enc E)) with (size (enc (V, E))) + using relation le at 1 by (now rewrite size_prod; cbn). + setoid_replace (size (enc V) + size (enc E)) with (size (enc (V, E))) + using relation le at 1 by (rewrite size_prod; cbn; lia). + unfold poly__fgraphWfDecb. reflexivity. Qed. +Lemma fgraph_wf_decb_poly : inOPoly poly__fgraphWfDecb. +Proof. + unfold poly__fgraphWfDecb; smpl_inO. + - apply fedges_symmetric_decb_poly. + - apply fedges_wf_decb_poly. +Qed. +#[export] Instance fgraph_wf_decb_mono: Proper (le ==> le) poly__fgraphWfDecb. +Proof. unfold poly__fgraphWfDecb. solve_proper. Qed. (** ** NP containment *) @@ -361,7 +378,8 @@ Proof. destruct G as (V & E). destruct H1 as [_ ((H1 & H2 & _) & _)]. enough (size (enc l) <= size (enc (seq 0 V))) as H3. { rewrite H3. rewrite list_size_of_el. - 2: { intros a (_ & Hb)%in_seq. rewrite nat_size_le; [ | rewrite Hb; reflexivity]. + 2: { intros a (_ & Hb)%in_seq. + rewrite nat_size_le; [| apply Nat.lt_le_incl; exact Hb]. reflexivity. } rewrite seq_length. cbn -[Nat.mul]. rewrite size_nat_enc_r with (n := V) at 2 3. @@ -372,17 +390,21 @@ Proof. + intros a Hel. apply H1 in Hel. apply in_seq. split; [lia | apply Hel]. + apply H2. - smpl_inO. - - smpl_inO. + - solve_proper. } eexists. split. - constructor. exists (fun '(G, k, l) => fgraph_wf_decb G && isfKClique_decb k G l). - + extract. recRel_prettify2. rewrite isfKClique_decb_time_bound, fgraph_wf_decb_time_bound. - poly_mono isfKClique_decb_poly. 2: {instantiate (1 := size (enc (a, b1, b0, b))). rewrite !size_prod; cbn. lia. } - poly_mono fgraph_wf_decb_poly. 2: {instantiate (1 := size (enc (a, b1, b0, b))). rewrite !size_prod; cbn. lia. } + + extract. recRel_prettify2. rewrite isfKClique_decb_time_bound, fgraph_wf_decb_time_bound. + setoid_replace (size (enc (a, b1)) + size (enc b)) with (size (enc (a, b1, b0, b))) + using relation le at 1 by (rewrite !size_prod; cbn; lia). + setoid_replace (size (enc (a, b1))) with (size (enc (a, b1, b0, b))) + using relation le at 1 by (rewrite !size_prod; cbn; lia). instantiate (1 := fun n => _). cbn. generalize (size (enc (a, b1, b0, b))). reflexivity. + intros ((G & k) & l). cbn. rewrite andb_true_iff. rewrite fgraph_wf_decb_iff. split. - * intros [H1 H2]; split; [apply H1 | rewrite isfKClique_decb_iff; easy]. - * intros [H1 H2]; split; [apply H1 | rewrite <- isfKClique_decb_iff; easy ]. - - split; smpl_inO; first [apply fgraph_wf_decb_poly | apply isfKClique_decb_poly]. + * intros [H1 H2]; split; [apply H1 | now rewrite isfKClique_decb_iff]. + * intros [H1 H2]; split; [apply H1 | now rewrite <- isfKClique_decb_iff]. + - split. + + smpl_inO; [apply isfKClique_decb_poly | apply fgraph_wf_decb_poly ]. + + solve_proper. Qed. diff --git a/theories/NP/Clique/kSAT_to_FlatClique.v b/theories/NP/Clique/kSAT_to_FlatClique.v index d84f61c6..f87c4b62 100644 --- a/theories/NP/Clique/kSAT_to_FlatClique.v +++ b/theories/NP/Clique/kSAT_to_FlatClique.v @@ -1,6 +1,7 @@ From Undecidability.L Require Import L. From Undecidability.L.Tactics Require Import LTactics GenEncode. -From Undecidability.L.Datatypes Require Import Lists LNat LProd. +From Undecidability.L.Datatypes Require Import Lists LProd. +From Complexity.L.Datatypes Require Import LNat. From Complexity.NP.Clique Require Import FlatUGraph FlatClique kSAT_to_Clique. From Complexity.NP.SAT Require Import kSAT SAT_inNP. From Complexity.Libs.CookPrelim Require Import FlatFinTypes MorePrelim. @@ -249,7 +250,9 @@ Proof. unfold allPositions_time. unfold seq_time. rewrite list_size_length at 1 2. rewrite size_nat_enc_r with (n := k) at 1. rewrite prodLists_time_bound. - poly_mono prodLists_poly. + setoid_replace (size (enc (seq 0 (| N |))) + size (enc (seq 0 k))) with + ((size (enc N) + size (enc k))^2 + c__listsizeCons * (size (enc N) + size (enc k)) + 2* c__listsizeNil) + using relation le. 2: { rewrite list_size_of_el. 2: { intros a (_ & H)%in_seq. rewrite nat_size_le. 2: instantiate (1 := (|N|)); lia. reflexivity. } @@ -258,14 +261,18 @@ Proof. } rewrite !seq_length. rewrite list_size_enc_length, !list_size_length. rewrite size_nat_enc_r with (n := k) at 2 3. - instantiate (1 := ((size (enc N) + size (enc k))^2 + c__listsizeCons * (size (enc N) + size (enc k)) + 2* c__listsizeNil)). cbn -[Nat.mul c__listsizeCons]. leq_crossout. + cbn -[Nat.mul c__listsizeCons]. leq_crossout. } unfold poly__allPositions. leq_crossout. Qed. -Lemma allPositions_poly : monotonic poly__allPositions /\ inOPoly poly__allPositions. +Lemma allPositions_poly : inOPoly poly__allPositions. Proof. - unfold poly__allPositions; split; smpl_inO; try apply inOPoly_comp; smpl_inO; apply prodLists_poly. -Qed. + unfold poly__allPositions; smpl_inO. + apply inOPoly_comp. + - solve_proper. + - exact prodLists_poly. + - smpl_inO. +Qed. (** literalsConflict_decb *) Definition c__literalsConflictDecb := c__eqbBool + 24. @@ -301,10 +308,10 @@ Proof. unfold EqBool.eqbTime. rewrite Nat.le_min_l. unfold poly__optLiteralsConflictDecb. rewrite size_option, size_prod; cbn. nia. Qed. -Lemma opt_literalsConflict_decb_poly : monotonic poly__optLiteralsConflictDecb /\ inOPoly poly__optLiteralsConflictDecb. -Proof. - unfold poly__optLiteralsConflictDecb; split; smpl_inO. -Qed. +Lemma opt_literalsConflict_decb_poly : inOPoly poly__optLiteralsConflictDecb. +Proof. unfold poly__optLiteralsConflictDecb; smpl_inO. Qed. +#[export] Instance opt_literalsConflict_decb_mono: Proper (le ==> le) poly__optLiteralsConflictDecb. +Proof. unfold poly__optLiteralsConflictDecb. solve_proper. Qed. (** toVertex *) Definition c__toVertex := c__length + 8. @@ -328,10 +335,10 @@ Proof. replace_le (size (enc ci)) with g by (subst g; rewrite size_prod; cbn; lia) at 1 2 3. fold g. unfold poly__toVertex. nia. Qed. -Lemma toVertex_poly : monotonic poly__toVertex /\ inOPoly poly__toVertex. -Proof. - unfold poly__toVertex; split; smpl_inO. -Qed. +Lemma toVertex_poly : inOPoly poly__toVertex. +Proof. unfold poly__toVertex; smpl_inO. Qed. +#[export] Instance toVertex_mono: Proper (le ==> le) poly__toVertex. +Proof. unfold poly__toVertex. solve_proper. Qed. (** cnfGetLiteral *) Definition c__cnfGetLiteral := 15. @@ -359,10 +366,10 @@ Proof. - rewrite nth_error_time_bound. rewrite Nat.le_min_l. unfold poly__cnfGetLiteral; nia. Qed. -Lemma cnfGetLiteral_poly : monotonic poly__cnfGetLiteral /\ inOPoly poly__cnfGetLiteral. -Proof. - unfold poly__cnfGetLiteral; split; smpl_inO. -Qed. +Lemma cnfGetLiteral_poly : inOPoly poly__cnfGetLiteral. +Proof. unfold poly__cnfGetLiteral; smpl_inO. Qed. +#[export] Instance cnfGetLiteral_mono: Proper (le ==> le) poly__cnfGetLiteral. +Proof. unfold poly__cnfGetLiteral. solve_proper. Qed. Lemma cnfGetLiteral_size N ci li: size (enc (cnfGetLiteral N ci li)) <= size (enc N) + 5. Proof. @@ -394,20 +401,31 @@ Proof. rewrite !cnfGetLiteral_time_bound. rewrite opt_literalsConflict_decb_time_bound. rewrite !toVertex_time_bound. - pose (g := size (enc k) + size (enc N) + size (enc ((ci1, li1), (ci2, li2)))). - poly_mono cnfGetLiteral_poly. 2: { instantiate (1 := g). unfold g; nia. } - poly_mono toVertex_poly. 2: { instantiate (1 := g). unfold g. rewrite !size_prod; cbn; nia. } - poly_mono toVertex_poly at 2. 2: { instantiate (1 := g). unfold g. rewrite !size_prod; cbn; nia. } - poly_mono opt_literalsConflict_decb_poly. 2: { rewrite cnfGetLiteral_size. instantiate (1 := g + 5). unfold g. lia. } - unfold EqBool.eqbTime. rewrite Nat.le_min_l. + pose (g := size (enc k) + size (enc N) + size (enc ((ci1, li1), (ci2, li2)))). + setoid_replace (size (enc N)) with g using relation le at 1 2 by nia. + setoid_replace (size (enc N) + size (enc k) + size (enc (ci1, li1))) with g + using relation le at 1 by (unfold g;rewrite !size_prod; cbn; nia). + setoid_replace (size (enc N) + size (enc k) + size (enc (ci2, li2))) with g + using relation le at 1 by (unfold g; rewrite !size_prod; cbn; nia). + setoid_replace (size (enc (cnfGetLiteral N ci1 li1))) with (g + 5) + using relation le at 1 by (rewrite cnfGetLiteral_size; unfold g; lia). + unfold EqBool.eqbTime. rewrite Nat.le_min_l. fold g. replace_le (size (enc ci1)) with g by (unfold g; rewrite !size_prod; cbn; lia). - unfold poly__makeEdge; nia. + unfold poly__makeEdge. lia. Qed. -Lemma makeEdge_poly : monotonic poly__makeEdge /\ inOPoly poly__makeEdge. + +Lemma makeEdge_poly : inOPoly poly__makeEdge. Proof. - unfold poly__makeEdge; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply cnfGetLiteral_poly | apply opt_literalsConflict_decb_poly | apply toVertex_poly]. -Qed. + unfold poly__makeEdge. smpl_inO. + - exact cnfGetLiteral_poly. + - apply inOPoly_comp. + + solve_proper. + + exact opt_literalsConflict_decb_poly. + + smpl_inO. + - apply toVertex_poly. +Qed. +#[export] Instance makeEdge_mono: Proper (le ==> le) poly__makeEdge. +Proof. unfold poly__makeEdge. solve_proper. Qed. (** makeEdges *) Definition c__makeEdges := 11. @@ -429,31 +447,33 @@ Proof. unfold makeEdges_time. rewrite allPositions_time_bound. rewrite prodLists_time_bound. pose (g := size (enc N) + size (enc k)). - poly_mono prodLists_poly. + setoid_replace (size (enc (allPositions k N)) + size (enc (allPositions k N))) + with (((g + 4) * (g * g) + c__listsizeCons * g * g + c__listsizeNil) * 2) + using relation le. 2: { unfold allPositions. rewrite list_size_of_el. - 2: { intros (a & b) (H1 & H2)%in_prod_iff. + 2: { intros (a & b) (H1 & H2)%in_prod_iff. apply in_seq in H1 as (_ &H1). apply in_seq in H2 as (_&H2). rewrite size_prod. cbn in *. rewrite nat_size_lt; [ | unfold Ncl in H1; apply H1]. rewrite nat_size_lt with (a := b); [ | apply H2]. rewrite list_size_enc_length. reflexivity. } rewrite prod_length, !seq_length. unfold Ncl. rewrite size_nat_enc_r with (n := k) at 2 3 5 6. - rewrite list_size_length. - instantiate (1 := ((g + 4) * (g * g) + c__listsizeCons * g * g + c__listsizeNil) * 2). + rewrite list_size_length. fold g. replace_le (size (enc N)) with g by (subst g; lia). replace_le (size (enc k)) with g by (subst g; lia). nia. } rewrite map_time_mono. 2: { intros ((ci1 & li1) & (ci2 & li2)) Hel. instantiate (1 := fun _ => _). cbn -[makeEdge_time Nat.add Nat.mul]. rewrite makeEdge_time_bound. - poly_mono makeEdge_poly. + setoid_replace (size (enc k) + size (enc N) + size (enc (ci1, li1, (ci2, li2)))) + with ((g + 4) * 3) using relation le. 2: { apply in_prod_iff in Hel as (H1 & H2). apply in_allPositions_iff in H1 as (H1 & H1'). apply in_allPositions_iff in H2 as (H2 & H2'). - rewrite !size_prod. cbn. unfold Ncl in *. + rewrite !size_prod. cbn. unfold Ncl in *. rewrite nat_size_lt with (a := ci1); [ | apply H1]. rewrite nat_size_lt with (a := li1); [ | apply H1']. rewrite nat_size_lt with (a := ci2); [ | apply H2]. rewrite nat_size_lt with (a := li2); [ | apply H2']. - rewrite list_size_enc_length. instantiate (1 := (g + 4) * 3). subst g. nia. + rewrite list_size_enc_length. subst g. nia. } reflexivity. } @@ -469,11 +489,15 @@ Proof. replace_le (size (enc N)) with g by (subst g; nia). replace_le (size (enc k)) with g by (subst g; nia). unfold poly__makeEdges; cbn [Nat.pow]; nia. Qed. -Lemma makeEdges_poly : monotonic poly__makeEdges /\ inOPoly poly__makeEdges. +Lemma makeEdges_poly : inOPoly poly__makeEdges. Proof. - unfold poly__makeEdges; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply allPositions_poly | apply prodLists_poly | apply makeEdge_poly]. + unfold poly__makeEdges; smpl_inO. + - exact allPositions_poly. + - apply inOPoly_comp; [solve_proper | exact prodLists_poly | smpl_inO]. + - apply inOPoly_comp; [solve_proper | exact makeEdge_poly | smpl_inO]. Qed. +#[export] Instance makeEdges_mono: Proper (le ==> le) poly__makeEdges. +Proof. unfold poly__makeEdges, poly__allPositions. solve_proper. Qed. Lemma makeEdges_length k N : |makeEdges k N| <= k * k * (|N|) * (|N|). Proof. @@ -521,15 +545,10 @@ Proof. rewrite makeEdges_time_bound. unfold poly__Gflat. nia. Qed. -Lemma Gflat_poly : monotonic poly__Gflat /\ inOPoly poly__Gflat. -Proof. - unfold poly__Gflat; split; smpl_inO; apply makeEdges_poly. -Qed. - -Fact nat_size_mul a b: size (enc (a * b)) <= size (enc a) * size (enc b). -Proof. - rewrite !size_nat_enc. unfold c__natsizeS; nia. -Qed. +Lemma Gflat_poly : inOPoly poly__Gflat. +Proof. unfold poly__Gflat; smpl_inO; apply makeEdges_poly. Qed. +#[export] Instance Gflat_mono: Proper (le ==> le) poly__Gflat. +Proof. unfold poly__Gflat. solve_proper. Qed. Definition poly__GflatSize n := n * n + (n * n * 2 + 4) * n^4 + c__listsizeCons * n^4 + c__listsizeNil + 4. Lemma Gflat_size_bound k N: kCNF k N -> size (enc (Gflat k N)) <= poly__GflatSize (size (enc N) + size (enc k)). @@ -544,10 +563,10 @@ Proof. replace_le (size (enc k)) with g by (unfold g;nia). unfold poly__GflatSize. cbn [Nat.pow]. nia. Qed. -Lemma Gflat_size_poly : monotonic poly__GflatSize /\ inOPoly poly__GflatSize. -Proof. - unfold poly__GflatSize; split; smpl_inO. -Qed. +Lemma Gflat_size_poly : inOPoly poly__GflatSize. +Proof. unfold poly__GflatSize; smpl_inO. Qed. +#[export] Instance Gflat_size_mono: Proper (le ==> le) poly__GflatSize. +Proof. unfold poly__GflatSize. solve_proper. Qed. (** reduction *) Definition c__reduction := 14. @@ -572,15 +591,17 @@ Proof. rewrite kCNF_decb_time_bound, Gflat_time_bound. rewrite list_size_length. instantiate (f := fun n => poly__kCNFDecb (n + size (enc k)) + poly__Gflat (n + size (enc k)) + c__length * n + c__length + (c__leb * 2 + c__ltb) + c__reduction). subst f; simp_comp_arith; nia. - + subst f; smpl_inO; apply inOPoly_comp; smpl_inO; first [apply kCNF_decb_poly | apply Gflat_poly]. - + subst f; smpl_inO; first [apply kCNF_decb_poly | apply Gflat_poly]. + + unfold f; smpl_inO. + * apply inOPoly_comp; [solve_proper | exact kCNF_decb_poly | smpl_inO]. + * apply inOPoly_comp; [solve_proper | exact Gflat_poly | smpl_inO]. + + unfold f. solve_proper. + eexists (fun n => size (enc (trivialNoInstance)) + poly__GflatSize (n + size (enc k)) + n + 4). * intros N. unfold reduction. destruct kCNF_decb eqn:H1, Nat.ltb; cbn. 2-4: lia. apply kCNF_decb_iff in H1. rewrite size_prod; cbn. rewrite Gflat_size_bound by apply H1. unfold Ncl. rewrite list_size_enc_length. - nia. - * smpl_inO. apply inOPoly_comp; smpl_inO; apply Gflat_size_poly. - * smpl_inO. apply Gflat_size_poly. + nia. + * smpl_inO. apply inOPoly_comp; [solve_proper | exact Gflat_size_poly | smpl_inO]. + * solve_proper. - apply kSAT_reduces_to_FlatClique. Qed. diff --git a/theories/NP/L/CanEnumTerm.v b/theories/NP/L/CanEnumTerm.v index 8faa3b44..488691fd 100644 --- a/theories/NP/L/CanEnumTerm.v +++ b/theories/NP/L/CanEnumTerm.v @@ -17,19 +17,21 @@ Proof with try eauto;smpl_inO. now cbv;reflexivity. 1,2:unfold time... exists id... + solve_proper. Qed. Lemma pro_enum_term : canEnumTerms Pro. Proof. - evar (fsize : nat -> nat). [fsize]:intros n0. + pose (fsize := fun n => n * Compile.c__size). eexists (fun P => match decompile 0 P [] with inl [s] => s | _ => var 0 end) fsize. 2:{ intros s. exists (compile s). rewrite decompile_correct. split. easy. - rewrite compile_enc_size,LTerm.size_term_enc_r. - set (size (enc s)). unfold fsize. reflexivity. + rewrite compile_enc_size,LTerm.size_term_enc_r. reflexivity. } - 2,3:now unfold fsize;smpl_inO. - clear fsize. evar (time : nat -> nat). [time]:intros n0. + 2: unfold fsize; smpl_inO. + 2: unfold fsize; solve_proper. + clear fsize. + evar (time : nat -> nat). [time]:intros n0. exists time. {extract. solverec. all:rewrite time_decompile_nice_leq. all:unfold time_decompile_nice. @@ -39,7 +41,7 @@ Proof. } 1,2:now unfold time;smpl_inO. clear time. evar (fsize : nat -> nat). [fsize]:intros n0. - enough (mono__f:monotonic fsize). + enough (mono__f: Proper (le ==> le) fsize). exists fsize. 3:assumption. {intros x. destruct decompile as [[ |? []]| ] eqn:eq. @@ -53,7 +55,8 @@ Proof. all:unfold fsize. all:do 2 (unfold enc at 1;cbn). all:rewrite (size_list x);cbn; unfold c__listsizeNil;easy. } - all:unfold fsize;smpl_inO. + - unfold fsize. smpl_inO. + - unfold fsize. solve_proper. Qed. Module boollist_enum. @@ -137,7 +140,7 @@ Module boollist_enum. Lemma boollists_enum_term : canEnumTerms (list bool). Proof. evar (fsize : nat -> nat). [fsize]:intros n. - cut (monotonic fsize). intros mono_fsize. + cut (Proper (le ==> le) fsize). intros mono_fsize. eexists (fun bs => f__toTerm pro_enum_term (boollist_term bs [])) fsize. 2:{ intros s. specialize (complete__toTerm pro_enum_term) as (P&Hf&Hfsize). exists (pro_to_boollist P). @@ -151,11 +154,14 @@ Module boollist_enum. clear. evar (time : nat -> nat). [time]:intros n0. exists time. {extract. solverec. rewrite UpToC_le, size_list_enc_r. set (size (enc x)). unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO;eapply inOPoly_comp;smpl_inO. - clear time. evar (fsize : nat -> nat). [fsize]:intros n0. - exists fsize. - {intros x. rewrite boollist_term_size. rewrite (size_list []). cbn. - set (n0:=size _). unfold fsize. reflexivity. } - all:unfold fsize;smpl_inO. + - unfold time. smpl_inO. + - unfold time. solve_proper. + - clear time. evar (fsize : nat -> nat). [fsize]:intros n0. + exists fsize. + + intros x. rewrite boollist_term_size. rewrite (size_list []). cbn. + set (n0:=size _). unfold fsize. reflexivity. + + unfold fsize. smpl_inO. + + unfold fsize. solve_proper. + - solve_proper. Qed. End boollist_enum. diff --git a/theories/NP/L/CanEnumTerm_def.v b/theories/NP/L/CanEnumTerm_def.v index 89d0786b..3c31c21c 100644 --- a/theories/NP/L/CanEnumTerm_def.v +++ b/theories/NP/L/CanEnumTerm_def.v @@ -8,16 +8,19 @@ Record canEnumTerms (X__cert : Type) `{R__cert : encodable X__cert} : Type := inSize__toTerm : nat -> nat; complete__toTerm : (forall s:term, exists x:X__cert, f__toTerm x = s /\ size (enc x) <= inSize__toTerm (size (enc s))); polyIn__toTerm : inOPoly inSize__toTerm; - monoIn__toTerm : monotonic inSize__toTerm; + monoIn__toTerm : Proper (le ==> le) inSize__toTerm; }. +#[global] Instance mono_inSize__toTerm X (R__cert : encodable X) (H: @canEnumTerms X _): + Proper (le ==> le) (inSize__toTerm H). +Proof. apply monoIn__toTerm. Qed. + Arguments canEnumTerms : clear implicits. Arguments canEnumTerms _ {_}. #[export] Hint Extern 2 (computableTime (f__toTerm _) _) => unshelve (simple apply @comp__polyTC);simple apply @comp__toTerm :typeclass_instances. Smpl Add 10 (simple apply polyIn__toTerm) : inO. -Smpl Add 10 (simple apply monoIn__toTerm) : inO. Lemma canEnumTerms_compPoly (X__cert : Type) `{R__cert : encodable X__cert}: canEnumTerms X__cert -> exists H : canEnumTerms X__cert, inhabited (polyTimeComputable (time__polyTC H)) diff --git a/theories/NP/L/GenNPBool.v b/theories/NP/L/GenNPBool.v index a9586fb8..2a558eeb 100644 --- a/theories/NP/L/GenNPBool.v +++ b/theories/NP/L/GenNPBool.v @@ -2,7 +2,11 @@ From Undecidability.L Require Import L_facts. From Undecidability.L.Datatypes Require Import LProd LTerm LBool. From Complexity.Complexity Require Import NP Definitions Monotonic. From Undecidability.L.Functions Require Import Size. -Import Nat L_Notations. +Import Nat L_Notations. + +#[export] Instance add_time_mono: Proper (le ==> le) add_time. +Proof. unfold add_time. solve_proper. Qed. + Definition GenNPBool : term*nat*nat -> Prop:= fun '(s', maxSize, steps (*in unary*)) => (proc s'/\exists (c:term), size (enc c) <= maxSize @@ -45,15 +49,15 @@ Proof. eexists (fun x => f' x). +extract. recRel_prettify2. cbn [size]. set (size (enc x)). unfold f'. reflexivity. - +subst f'. cbn beta. unfold add_time. smpl_inO. all:eapply inOPoly_comp. all:try setoid_rewrite size_nat_enc. all:smpl_inO. - +subst f'. cbn beta. unfold add_time. smpl_inO. all:try setoid_rewrite size_nat_enc. all:smpl_inO. + +subst f'. cbn beta. unfold add_time. smpl_inO. all:eapply inOPoly_comp. all: try solve_proper. all:try setoid_rewrite size_nat_enc. all:smpl_inO. + + subst f'. cbn beta. all:try setoid_rewrite size_nat_enc. solve_proper. + eexists (fun x => _);repeat split. - *intros. - repeat (setoid_rewrite -> size_prod;cbn[fst snd]). - rewrite !size_nat_enc,!size_term_enc. cbn [size]. - generalize (size (enc x)). intros. reflexivity. - *smpl_inO. all:eapply inOPoly_comp. all:smpl_inO. - *smpl_inO. + * intros. + repeat (setoid_rewrite -> size_prod;cbn[fst snd]). + rewrite !size_nat_enc,!size_term_enc. cbn [size]. + generalize (size (enc x)). intros. reflexivity. + * smpl_inO. apply inOPoly_comp; [exact mono_t__R | exact poly_t__R | smpl_inO]. + * solve_proper. Qed. From Undecidability.L.Functions Require Import Proc. @@ -112,12 +116,12 @@ Proof. split. +cbn. intuition eauto 10. +intros (?&?&?&[= -> -> ->]&?). intuition eauto 10. Lproc. - -unfold f__t. - smpl_inO. - -unfold f__t. - smpl_inO. + -unfold f__t. smpl_inO. + -unfold f__t. solve_proper. } - eexists (fun x => x). 3,4:smpl_inO. + eexists (fun x => x). + 3: smpl_inO. + 3: solve_proper. all:intros ((?,?),?). all:cbn. -intros ? (?&?&?&[= <- <- <-]&?&?&?). eauto 10. -intros (?&?&?&?). eexists. split. eauto 10. repeat setoid_rewrite size_prod. cbn [fst snd]. diff --git a/theories/NP/L/GenNP_is_hard.v b/theories/NP/L/GenNP_is_hard.v index c184926c..6e9995a5 100644 --- a/theories/NP/L/GenNP_is_hard.v +++ b/theories/NP/L/GenNP_is_hard.v @@ -23,11 +23,14 @@ Proof. {subst f. extract. recRel_prettify. intros x _. split. nia. intros c__t _. split. 2:easy. remember (size (enc (x, c__t))) as n0 eqn:eqn0. - rewrite (mono__polyTC enumTerm (x':=n0)). 2:{ subst n0. rewrite size_prod. cbn;lia. } + setoid_replace (size (enc c__t)) with n0 using relation le. + 2:{ subst n0. rewrite size_prod. cbn;lia. } erewrite (mono_t__R _). 2:{ rewrite size_prod in eqn0|-*;cbn [fst snd] in eqn0|-*. - rewrite (bounds__rSP enumTerm c__t). rewrite (mono__rSP _ (x':=n0)). 2:{subst n0;nia. } + rewrite (bounds__rSP enumTerm c__t). + setoid_replace (size (enc c__t)) with n0 using relation le. + 2:{ subst n0; nia. } instantiate (1:=n0 + resSize__rSP enumTerm n0). nia. } unfold time;reflexivity. @@ -129,16 +132,17 @@ Proof. +unfold mSize, steps, stepsInner. extract. recRel_prettify2. generalize (size (enc x)). intro. unfold f'. reflexivity. +subst f'. cbn beta. setoid_rewrite size_nat_enc. all:smpl_inO. all:eapply inOPoly_comp. - all:unfold add_time; smpl_inO. all:eapply inOPoly_comp. all:smpl_inO. all:eapply inOPoly_comp. all:smpl_inO. - all:eapply inOPoly_comp. all:smpl_inO. - +subst f'. cbn beta. setoid_rewrite size_nat_enc. all:unfold add_time; smpl_inO. + all:unfold add_time; first [solve_proper | smpl_inO]. + all:eapply inOPoly_comp. all: first [solve_proper | smpl_inO]. + all:eapply inOPoly_comp. all: first [solve_proper | smpl_inO]. + all:eapply inOPoly_comp. all: first [solve_proper | smpl_inO]. + + subst f'. cbn beta. setoid_rewrite size_nat_enc. unfold add_time. solve_proper. +unfold mSize,steps,stepsInner. eexists (fun x => _). *intros. repeat (setoid_rewrite -> size_prod;cbn[fst snd]). rewrite !size_nat_enc,!size_term_enc. cbn [size]. generalize (size (enc x)). intros. reflexivity. - *smpl_inO. all:eapply inOPoly_comp. all:smpl_inO. all:eapply inOPoly_comp. all:smpl_inO. all:eapply inOPoly_comp. all:smpl_inO. - *smpl_inO. + *smpl_inO. all:eapply inOPoly_comp. all:first [solve_proper | smpl_inO]. all:eapply inOPoly_comp. all:first [solve_proper | smpl_inO]. + eapply inOPoly_comp; [solve_proper | smpl_inO | smpl_inO]. + *solve_proper. Qed. - - diff --git a/theories/NP/SAT/CookLevin.v b/theories/NP/SAT/CookLevin.v index d88fa302..8187b085 100644 --- a/theories/NP/SAT/CookLevin.v +++ b/theories/NP/SAT/CookLevin.v @@ -51,12 +51,9 @@ Proof. eapply reducesPolyMO_transitive with (Q := FlatFunSingleTMGenNP). apply (TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP M). eassumption. eapply reducesPolyMO_intro with (f := id). - - exists (fun _ => 1). - + extract. solverec. - + smpl_inO. - + smpl_inO. - + exists (fun n => n). 2, 3: smpl_inO. - intros x. now cbn. + - exists (fun _ => 1); [ | smpl_inO | apply monotonic_c | ]. + + extract. solverec. + + exists (fun n => n); [ easy | smpl_inO | solve_proper ]. - intros (((? & ?) & ?) & ?). apply FlatFunSingleTMGenNP_FlatSingleTMGenNP_equiv. Qed. diff --git a/theories/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v b/theories/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v index f0630de1..4ab3957c 100644 --- a/theories/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v +++ b/theories/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v @@ -1,5 +1,6 @@ From Undecidability.Shared.Libs.PSL Require Import Base. From Complexity.Libs.CookPrelim Require Import Tactics MorePrelim. +From Complexity.L.Datatypes Require Import LNat. From Undecidability.L.Datatypes Require Import Lists LNat LBool LProd LOptions. From Complexity.NP.SAT Require Import FSAT BinaryCC FormulaEncoding. Require Import Lia. @@ -512,10 +513,10 @@ Proof. unfold encodeCardAt_time. unfold encodeListAt_time. rewrite H1, H2. unfold poly__encodeCardAt; solverec. Qed. -Lemma encodeCardAt_poly : monotonic poly__encodeCardAt /\ inOPoly poly__encodeCardAt. -Proof. - unfold poly__encodeCardAt; split; smpl_inO. -Qed. +Lemma encodeCardAt_poly : inOPoly poly__encodeCardAt. +Proof. unfold poly__encodeCardAt; smpl_inO. Qed. +#[export] Instance encodeCardAt_mono: Proper (le ==> le) poly__encodeCardAt. +Proof. unfold poly__encodeCardAt. solve_proper. Qed. Lemma encodeCardAt_varsIn s1 s2 k card : CCCard_of_size card k -> formula_varsIn (fun n => (n >= s1 /\ n < s1 + k) \/ (n >= s2 /\ n < s2 + k)) (encodeCardAt s1 s2 card). Proof. @@ -543,20 +544,21 @@ Definition poly__encodeCardsAt n := n * (poly__encodeCardAt n + c__map) + c__map Lemma encodeCardsAt_time_bound bpr s1 s2: BinaryCC_wellformed bpr -> encodeCardsAt_time bpr s1 s2 <= poly__encodeCardsAt (size (enc bpr)). -Proof. +Proof. intros H. unfold encodeCardsAt_time. rewrite map_time_mono. 2: { intros card H1. apply H in H1. instantiate (1 := fun _ => _). cbn. rewrite encodeCardAt_time_bound by apply H1. reflexivity. } rewrite map_time_const. - unfold listOr_time. rewrite map_length. - poly_mono encodeCardAt_poly. 2: { rewrite size_nat_enc_r. instantiate (1 := size (enc bpr)). rewrite BinaryCC_enc_size. lia. } + unfold listOr_time. rewrite map_length. + setoid_replace (width bpr) with (size (enc bpr)) using relation le at 1. + 2: { rewrite size_nat_enc_r. rewrite BinaryCC_enc_size. lia. } rewrite list_size_length. replace_le (size (enc (cards bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - unfold poly__encodeCardsAt. solverec. + reflexivity. Qed. -Lemma encodeCardsAt_poly : monotonic poly__encodeCardsAt /\ inOPoly poly__encodeCardsAt. +Lemma encodeCardsAt_poly : inOPoly poly__encodeCardsAt. Proof. - unfold poly__encodeCardsAt; split; smpl_inO; apply encodeCardAt_poly. + unfold poly__encodeCardsAt; smpl_inO; apply encodeCardAt_poly. Qed. Lemma encodeCardsAt_varsIn s1 s2 bpr : @@ -618,10 +620,10 @@ Proof. replace_le (size (enc (width bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; cbn; lia). unfold poly__encodeCardsInLineP1. unfold add_time. nia. Qed. -Lemma encodeCardsInLineP1_poly : monotonic poly__encodeCardsInLineP1 /\ inOPoly poly__encodeCardsInLineP1. -Proof. - unfold poly__encodeCardsInLineP1; split; smpl_inO; apply encodeCardsAt_poly. -Qed. +Lemma encodeCardsInLineP1_poly : inOPoly poly__encodeCardsInLineP1. +Proof. unfold poly__encodeCardsInLineP1; smpl_inO; apply encodeCardsAt_poly. Qed. +#[export] Instance encodeCardsInLineP1_mono: Proper (le ==> le) poly__encodeCardsInLineP1. +Proof. unfold poly__encodeCardsInLineP1, poly__encodeCardsAt. solve_proper. Qed. (** in a second step, we also bound the numbers by their encoding size *) Definition poly__encodeCardsInLine' n := (n + 1) * poly__encodeCardsInLineP1 n + n * (n * n + n + 1) * c__add * 2. @@ -634,18 +636,18 @@ Proof. replace_le (size (enc (offset bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). rewrite size_nat_enc_r with (n := startA) at 1. rewrite size_nat_enc_r with (n := startB) at 1. - pose (g := size (enc bpr) + size (enc stepindex) + size (enc startA) + size (enc startB)). - poly_mono encodeCardsInLineP1_poly. 2: { instantiate (1 := g). subst g; lia. } + pose (g := size (enc bpr) + size (enc stepindex) + size (enc startA) + size (enc startB)). + setoid_replace (size (enc bpr)) with g using relation le at 1 by lia. replace_le (size (enc stepindex)) with g by (subst g; lia) at 1 2 3 4. replace_le (size (enc bpr)) with g by (subst g; lia) at 1 2. replace_le (size (enc startA)) with g by (subst g; lia) at 1. replace_le (size (enc startB)) with g by (subst g; lia) at 1. fold g. unfold poly__encodeCardsInLine'. nia. Qed. -Lemma encodeCardsInLineP_poly : monotonic poly__encodeCardsInLine' /\ inOPoly poly__encodeCardsInLine'. -Proof. - unfold poly__encodeCardsInLine'; split; smpl_inO; apply encodeCardsInLineP1_poly. -Qed. +Lemma encodeCardsInLineP_poly : inOPoly poly__encodeCardsInLine'. +Proof. unfold poly__encodeCardsInLine'; smpl_inO; apply encodeCardsInLineP1_poly. Qed. +#[export] Instance encodeCardsInLineP_mono: Proper (le ==> le) poly__encodeCardsInLine'. +Proof. unfold poly__encodeCardsInLine'. solve_proper. Qed. Lemma encodeCardsInLineP_varsIn bpr stepi l startA startB : BinaryCC_wellformed bpr @@ -686,35 +688,38 @@ Proof. unfold encodeCardsInLine_time, c__encodeCardsInLine. solverec. Qed. -Definition poly__encodeCardsInLine n := 3 * c__length * n + (n + 1) * c__add + poly__encodeCardsInLine' (n * (c__natsizeS + 2) + c__natsizeO) + c__encodeCardsInLine. +Definition poly__encodeCardsInLine n := 3 * c__length * n + (n + 1) * c__add + poly__encodeCardsInLine' (n * (c__natsizeS + 2) + c__natsizeO) + c__encodeCardsInLine. Lemma encodeCardsInLine_time_bound bpr s : BinaryCC_wellformed bpr -> encodeCardsInLine_time bpr s <= poly__encodeCardsInLine (size (enc bpr) + size (enc s)). Proof. intros H. unfold encodeCardsInLine_time. rewrite encodeCardsInLineP_time_bound by easy. - poly_mono encodeCardsInLineP_poly. + setoid_replace (size (enc bpr) + size (enc (| init bpr |)) + size (enc s) + size (enc (s + (| init bpr |)))) + with ((size (enc bpr) + size (enc s)) * ( c__natsizeS + 2) + c__natsizeO) + using relation le. 2: { setoid_rewrite size_nat_enc at 3. rewrite list_size_enc_length, list_size_length. rewrite size_nat_enc_r with (n := s) at 2. replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - instantiate (1 := (size (enc bpr) + size (enc s)) * ( c__natsizeS + 2) + c__natsizeO). lia. - } + lia. + } rewrite list_size_length. replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). unfold add_time. rewrite size_nat_enc_r with (n := s) at 1. unfold poly__encodeCardsInLine; solverec. Qed. -Lemma encodeCardsInLine_poly : monotonic poly__encodeCardsInLine /\ inOPoly poly__encodeCardsInLine. +Lemma encodeCardsInLine_poly : inOPoly poly__encodeCardsInLine. Proof. - unfold poly__encodeCardsInLine; split; smpl_inO. - - apply encodeCardsInLineP_poly. - - apply inOPoly_comp; smpl_inO; apply encodeCardsInLineP_poly. -Qed. + unfold poly__encodeCardsInLine; smpl_inO. + apply inOPoly_comp; [solve_proper | apply encodeCardsInLineP_poly | smpl_inO]. +Qed. +#[export] Instance encodeCardsInLine_mono: Proper (le ==> le) poly__encodeCardsInLine. +Proof. unfold poly__encodeCardsInLine. solve_proper. Qed. Lemma encodeCardsInLine_varsIn bpr s : BinaryCC_wellformed bpr -> formula_varsIn (fun n => (n >= s /\ n < s + 2 * (|init bpr|))) (encodeCardsInLine bpr s). Proof. - intros H. eapply formula_varsIn_monotonic. + intros H. eapply formula_varsIn_monotonic. 2: { unfold encodeCardsInLine. apply encodeCardsInLineP_varsIn, H. } cbn. intros n. lia. Qed. @@ -734,31 +739,24 @@ Proof. unfold encodeCardsInAllLines_time, c__encodeCardsInAllLines. simp_comp_arith; lia. Qed. -Fact nat_size_mul a b: size (enc (a * b)) <= size (enc a) * size (enc b). -Proof. - rewrite !size_nat_enc. unfold c__natsizeS. nia. -Qed. - Definition poly__encodeCardsInAllLines n := c__length * n + (poly__tabulateStep n + (n * (poly__encodeCardsInLine (n + n * n) + c__map) + c__map)) + c__tabulateFormula + (n + 1) * c__listAnd + c__encodeCardsInAllLines. Lemma encodeCardsInAllLines_time_bound bpr : BinaryCC_wellformed bpr -> encodeCardsInAllLines_time bpr <= poly__encodeCardsInAllLines (size (enc bpr)). Proof. intros H. unfold encodeCardsInAllLines_time. rewrite list_size_length at 1. replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - unfold tabulate_formula_time. rewrite tabulate_step_time_bound. - poly_mono tabulate_step_poly. 2: { rewrite list_size_enc_length. instantiate (1 := size (enc bpr)). rewrite BinaryCC_enc_size; lia. } - rewrite map_time_mono. + unfold tabulate_formula_time. rewrite tabulate_step_time_bound. + setoid_replace (size (enc (| init bpr |)) + size (enc (steps bpr))) with (size (enc bpr)) using relation le. + 2: { rewrite list_size_enc_length. rewrite BinaryCC_enc_size; lia. } + rewrite map_time_mono. 2: { intros start Hel. instantiate (1 := fun _ => _). cbn -[Nat.add Nat.mul]. rewrite encodeCardsInLine_time_bound by apply H. - apply in_tabulate_step_iff in Hel as (i & H1 & ->). - poly_mono encodeCardsInLine_poly. - 2: { rewrite nat_size_le with (a := 0 + (|init bpr|) * i). 2: { instantiate (1 := (|init bpr|) * steps bpr). nia. } - rewrite nat_size_mul. rewrite list_size_enc_length. - replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - reflexivity. - } - reflexivity. + apply in_tabulate_step_iff in Hel as (i & H1 & ->). + rewrite nat_size_le with (a := 0 + (|init bpr|) * i). 2: { instantiate (1 := (|init bpr|) * steps bpr). nia. } + rewrite nat_size_mul. rewrite list_size_enc_length. + replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). + replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). + reflexivity. } rewrite map_time_const. rewrite tabulate_step_length. @@ -766,10 +764,14 @@ Proof. rewrite size_nat_enc_r with (n := steps bpr) at 1 2. replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). unfold poly__encodeCardsInAllLines. nia. Qed. -Lemma encodeCardsInAllLines_poly : monotonic poly__encodeCardsInAllLines /\ inOPoly poly__encodeCardsInAllLines. +Lemma encodeCardsInAllLines_poly : inOPoly poly__encodeCardsInAllLines. Proof. - unfold poly__encodeCardsInAllLines; split; smpl_inO; try apply inOPoly_comp; smpl_inO; first [apply tabulate_step_poly | apply encodeCardsInLine_poly]. + unfold poly__encodeCardsInAllLines; smpl_inO. + - exact tabulate_step_poly. + - apply inOPoly_comp; [solve_proper | apply encodeCardsInLine_poly | smpl_inO]. Qed. +#[export] Instance encodeCardsInAllLines_mono: Proper (le ==> le) poly__encodeCardsInAllLines. +Proof. unfold poly__encodeCardsInAllLines. solve_proper. Qed. Lemma encodeCardsInAllLines_varsIn bpr : BinaryCC_wellformed bpr @@ -777,14 +779,14 @@ Lemma encodeCardsInAllLines_varsIn bpr : Proof. intros H. unfold encodeCardsInAllLines. apply listAnd_varsIn. intros f H1. destruct steps; [now cbn in H1 | ]. - eapply tabulate_formula_varsIn in H1. + eapply tabulate_formula_varsIn in H1. 2: { intros s. eapply formula_varsIn_monotonic. 2: apply encodeCardsInLine_varsIn, H. intros n'. cbn. intros [_ H2]. apply H2. } - 2: smpl_inO. - cbn in H1. eapply formula_varsIn_monotonic. 2 : apply H1. intros n'. cbn. - nia. -Qed. + 2: solve_proper. + cbn in H1. eapply formula_varsIn_monotonic. 2 : apply H1. intros n'. cbn. + nia. +Qed. Lemma encodeCardsInAllLines_size bpr : BinaryCC_wellformed bpr @@ -828,14 +830,15 @@ Proof. unfold ltb_time, leb_time. rewrite Nat.le_min_r. rewrite list_size_length. rewrite size_nat_enc_r with (n := offset bpr) at 1. - replace_le (size (enc (offset bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; cbn; lia). - poly_mono encodeListAt_poly. 2: { instantiate (1 := size (enc bpr) + size (enc s)). lia. } - unfold poly__encodeSubstringInLineP1. unfold add_time. nia. -Qed. -Lemma encodeSubstringInLineP_poly1 : monotonic poly__encodeSubstringInLineP1 /\ inOPoly poly__encodeSubstringInLineP1. -Proof. - unfold poly__encodeSubstringInLineP1; split; smpl_inO; apply encodeListAt_poly. + replace_le (size (enc (offset bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; cbn; lia). + setoid_replace (size (enc s)) with (size (enc bpr) + size (enc s)) + using relation le at 1 by lia. + unfold poly__encodeSubstringInLineP1, add_time. nia. Qed. +Lemma encodeSubstringInLineP_poly1 : inOPoly poly__encodeSubstringInLineP1. +Proof. unfold poly__encodeSubstringInLineP1; smpl_inO; apply encodeListAt_poly. Qed. +#[export] Instance encodeSubstringInLineP1_mono: Proper (le ==> le) poly__encodeSubstringInLineP1. +Proof. unfold poly__encodeSubstringInLineP1. solve_proper. Qed. Definition poly__encodeSubstringInLine' n := (n + 1) * poly__encodeSubstringInLineP1 n + n * (n * n + n + 1) * c__add. Lemma encodeSubstringInLineP_time_bound bpr s stepindex l start : @@ -843,7 +846,8 @@ Lemma encodeSubstringInLineP_time_bound bpr s stepindex l start : Proof. intros H. rewrite encodeSubstringInLineP_time_bound1 by apply H. pose (g := size (enc bpr) + size (enc s) + size (enc stepindex) + size (enc start)). - poly_mono encodeSubstringInLineP_poly1. 2 : { instantiate (1 := g). subst g; lia. } + setoid_replace (size (enc bpr) + size (enc s)) with g + using relation le at 1 by lia. rewrite size_nat_enc_r with (n := stepindex) at 1 2 3. rewrite size_nat_enc_r with (n := offset bpr). replace_le (size (enc (offset bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). rewrite size_nat_enc_r with (n := start) at 1. @@ -852,10 +856,10 @@ Proof. replace_le (size (enc start)) with g by (unfold g; lia) at 1. fold g. unfold poly__encodeSubstringInLine'. nia. Qed. -Lemma encodeSubstringInLineP_poly : monotonic poly__encodeSubstringInLine' /\ inOPoly poly__encodeSubstringInLine'. -Proof. - unfold poly__encodeSubstringInLine'; split; smpl_inO; apply encodeSubstringInLineP_poly1. -Qed. +Lemma encodeSubstringInLineP_poly : inOPoly poly__encodeSubstringInLine'. +Proof. unfold poly__encodeSubstringInLine'; smpl_inO; apply encodeSubstringInLineP_poly1. Qed. +#[export] Instance encodeSubstringInLineP_mono: Proper (le ==> le) poly__encodeSubstringInLine'. +Proof. unfold poly__encodeSubstringInLine'. solve_proper. Qed. Lemma encodeSubstringInLineP_varsIn bpr s stepindex l start: formula_varsIn (fun n => n >= start /\ n < start + l) (encodeSubstringInLine' bpr s stepindex l start). Proof. @@ -939,10 +943,11 @@ Proof. 2: { intros l Hel. unfold encodeFinalConstraint_step_time, encodeSubstringInLine_time. instantiate (1 := fun _ => _). cbn -[Nat.mul Nat.add]. rewrite encodeSubstringInLineP_time_bound by apply H. - rewrite list_size_length at 1. replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - poly_mono encodeSubstringInLineP_poly. - 2: { instantiate (1 := 2 * (size (enc bpr) + size (enc start))). - rewrite (list_el_size_bound Hel), list_size_enc_length. + rewrite list_size_length at 1. replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). + setoid_replace (size (enc bpr) + size (enc l) + size (enc (| init bpr |)) + size (enc start)) + with (2 * (size (enc bpr) + size (enc start))) + using relation le. + 2: { rewrite (list_el_size_bound Hel), list_size_enc_length. cbn. rewrite BinaryCC_enc_size at 2. lia. } reflexivity. @@ -951,12 +956,15 @@ Proof. replace_le (size (enc (final bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). unfold poly__encodeFinalConstraint; nia. Qed. -Lemma encodeFinalConstraint_poly : monotonic poly__encodeFinalConstraint /\ inOPoly poly__encodeFinalConstraint. +Lemma encodeFinalConstraint_poly : inOPoly poly__encodeFinalConstraint. Proof. - unfold poly__encodeFinalConstraint; split; smpl_inO. - - apply encodeSubstringInLineP_poly. - - apply inOPoly_comp; smpl_inO; apply encodeSubstringInLineP_poly. -Qed. + unfold poly__encodeFinalConstraint; smpl_inO. apply inOPoly_comp. + - solve_proper. + - apply encodeSubstringInLineP_poly. + - smpl_inO. +Qed. +#[export] Instance encodeFinalConstraint_mono: Proper (le ==> le) poly__encodeFinalConstraint. +Proof. unfold poly__encodeFinalConstraint. solve_proper. Qed. Lemma encodeFinalConstraint_varsIn bpr start : formula_varsIn (fun n => n >= start /\ n < start + (|init bpr|)) (encodeFinalConstraint bpr start). Proof. @@ -987,24 +995,28 @@ Definition poly__encodeTableau n := poly__encodeListAt n + poly__encodeCardsInAl Lemma encodeTableau_time_bound bpr : BinaryCC_wellformed bpr -> encodeTableau_time bpr <= poly__encodeTableau (size (enc bpr)). Proof. intros H. unfold encodeTableau_time. - rewrite encodeListAt_time_bound. poly_mono encodeListAt_poly. 2: { instantiate (1:= size (enc bpr)). rewrite BinaryCC_enc_size; lia. } - rewrite encodeCardsInAllLines_time_bound by apply H. - rewrite encodeFinalConstraint_time_bound by apply H. - poly_mono encodeFinalConstraint_poly. - 2: { rewrite nat_size_mul. rewrite list_size_enc_length. - replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). - reflexivity. - } + rewrite encodeListAt_time_bound. + setoid_replace (size (enc (init bpr))) with (size (enc bpr)) using relation le. + 2: { rewrite BinaryCC_enc_size; lia. } + rewrite encodeCardsInAllLines_time_bound by apply H. + rewrite encodeFinalConstraint_time_bound by apply H. + rewrite nat_size_mul. rewrite list_size_enc_length. + replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). + replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). unfold mult_time. rewrite list_size_length at 1 2. rewrite size_nat_enc_r with (n := steps bpr). replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia) at 1 2. replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia) at 1 2. unfold poly__encodeTableau; nia. Qed. -Lemma encodeTableau_poly : monotonic poly__encodeTableau /\ inOPoly poly__encodeTableau. +Lemma encodeTableau_poly : inOPoly poly__encodeTableau. Proof. - unfold poly__encodeTableau; split; smpl_inO; try apply inOPoly_comp; smpl_inO; first [apply encodeListAt_poly | apply encodeCardsInAllLines_poly | apply encodeFinalConstraint_poly]. -Qed. + unfold poly__encodeTableau; smpl_inO. + - apply encodeListAt_poly. + - apply encodeCardsInAllLines_poly. + - apply inOPoly_comp; [solve_proper | apply encodeFinalConstraint_poly | smpl_inO]. +Qed. +#[export] Instance encodeTableau_mono: Proper (le ==> le) poly__encodeTableau. +Proof. unfold poly__encodeTableau. solve_proper. Qed. Lemma encodeTableau_varsIn bpr: BinaryCC_wellformed bpr -> formula_varsIn (fun n => n < (1 + steps bpr) * (|init bpr|)) (encodeTableau bpr). Proof. @@ -1016,7 +1028,7 @@ Proof. - unfold encodeFinalConstraint' in H2. apply encodeFinalConstraint_varsIn in H2. nia. Qed. -Lemma encodeTableau_size : {f : nat -> nat & (forall bpr, BinaryCC_wellformed bpr -> formula_size (encodeTableau bpr) <= f (size (enc bpr))) /\ monotonic f /\ inOPoly f}. +Lemma encodeTableau_size : {f : nat -> nat & (forall bpr, BinaryCC_wellformed bpr -> formula_size (encodeTableau bpr) <= f (size (enc bpr))) /\ Proper (le ==> le) f /\ inOPoly f}. Proof. eexists. split; [ | split]. - intros bpr H. unfold encodeTableau. cbn. @@ -1039,11 +1051,11 @@ Proof. rewrite size_nat_enc_r with (n := steps bpr). replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). instantiate (1 := fun n => _). cbn -[Nat.add Nat.mul]. generalize (size (enc bpr)). reflexivity. - - smpl_inO. + - solve_proper. - smpl_inO. Qed. -Lemma encodeTableau_enc_size : {f : nat -> nat & (forall bpr, BinaryCC_wellformed bpr -> size (enc (encodeTableau bpr)) <= f (size (enc bpr))) /\ inOPoly f /\ monotonic f}. +Lemma encodeTableau_enc_size : {f : nat -> nat & (forall bpr, BinaryCC_wellformed bpr -> size (enc (encodeTableau bpr)) <= f (size (enc bpr))) /\ inOPoly f /\ Proper (le ==> le) f}. Proof. destruct encodeTableau_size as (f' & H1 & H2 & H3). eexists. split; [ | split]. @@ -1054,8 +1066,8 @@ Proof. rewrite list_size_length. replace_le (size (enc (init bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). rewrite size_nat_enc_r with (n := steps bpr). replace_le (size (enc (steps bpr))) with (size (enc bpr)) by (rewrite BinaryCC_enc_size; lia). generalize (size (enc bpr)). reflexivity. - - smpl_inO. - - smpl_inO. + - smpl_inO. + - solve_proper. Qed. (** BinaryCC_wf_dec *) @@ -1067,7 +1079,7 @@ Instance term_BinaryCC_wf_dec : computableTime' BinaryCC_wf_dec (fun bpr _ => (B Proof. extract. solverec. unfold BinaryCC_wf_dec_time, c__BinaryCCWfDec, leb_time. rewrite !eqbTime_le_r. - rewrite !Nat.le_min_l with (n:=1). simp_comp_arith. ring_simplify;reflexivity. + rewrite !Nat.le_min_l with (n:=1). simp_comp_arith. ring_simplify;reflexivity. Qed. Definition c__BinaryCCWfDecBound := 2*(2 * c__length + c__leb + FlatCC.c__prcardOfSizeDecBound + c__forallb + 2 * c__moduloBound + c__BinaryCCWfDec). @@ -1083,7 +1095,7 @@ Proof. split; [intros | ]. - specialize (FlatCC.CCCard_of_size_dec_time_bound (X := bool) y a) as H1. instantiate (2:= fun n => (n + 1) * FlatCC.c__prcardOfSizeDecBound). simp_comp_arith; nia. - - smpl_inO. + - solve_proper. } rewrite list_size_length. replace_le (size(enc (cards fpr))) with (size (enc fpr)) by (rewrite BinaryCC_enc_size; lia). @@ -1092,10 +1104,10 @@ Proof. replace_le (size(enc(offset fpr))) with (size (enc fpr)) by (rewrite BinaryCC_enc_size; lia). unfold poly__BinaryCCWfDec, c__BinaryCCWfDecBound. nia. Qed. -Lemma BinaryCC_wf_dec_poly : monotonic poly__BinaryCCWfDec /\ inOPoly poly__BinaryCCWfDec. -Proof. - unfold poly__BinaryCCWfDec; split; smpl_inO. -Qed. +Lemma BinaryCC_wf_dec_poly : inOPoly poly__BinaryCCWfDec. +Proof. unfold poly__BinaryCCWfDec; smpl_inO. Qed. +#[export] Instance BinaryCC_wf_dec_mono: Proper (le ==> le) poly__BinaryCCWfDec. +Proof. unfold poly__BinaryCCWfDec. solve_proper. Qed. (** reduction *) Definition c__reduction := 4. @@ -1119,13 +1131,12 @@ Proof. generalize (size (enc bpr)). reflexivity. * rewrite BinaryCC_wf_dec_time_bound. lia. + smpl_inO; first [apply encodeTableau_poly | apply BinaryCC_wf_dec_poly]. - + smpl_inO; first [apply encodeTableau_poly | apply BinaryCC_wf_dec_poly]. + + solve_proper. + destruct encodeTableau_enc_size as (f & H1 & H2 & H3). exists (fun n => f n + size (enc trivialNoInstance)). - * intros bpr. unfold reduction. destruct BinaryCC_wf_dec eqn:H4. - -- apply BinaryCC_wf_dec_correct in H4. rewrite H1 by apply H4. lia. - -- lia. - * smpl_inO. + * intros bpr. unfold reduction. destruct BinaryCC_wf_dec eqn:H4; [|lia]. + apply BinaryCC_wf_dec_correct in H4. rewrite H1 by apply H4. lia. * smpl_inO. + * solve_proper. - apply BinaryCC_to_FSAT. Qed. diff --git a/theories/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v b/theories/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v index 7770b328..12e1b566 100644 --- a/theories/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v +++ b/theories/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v @@ -4,19 +4,6 @@ From Complexity.Libs Require Import CookPrelim.MorePrelim UniformHomomorphisms F From Complexity.NP.SAT.CookLevin Require Import BinaryCC FlatCC CC_to_BinaryCC. Require Import Lia. -#[export] Instance equi_equivalence X: Equivalence (@equi X). -Proof. - eexists. - - intro l. split; apply incl_refl. - - intros l l' H. split; apply H. - - intros l l' l'' [] []. split; eapply incl_tran; eassumption. -Qed. - -#[export] Instance in_equi_proper X x: Proper (@equi X ==> Basics.impl) (In x). -Proof. - intros ??[H]?. now apply H. -Qed. - (** * Reduction of FlatCC to BinaryCC *) (** logically, we reduce FlatCC to CC and use the reduction of CC to BinaryCC *) (** but in order to make the reduction extractable, we give a shortcut reduction which produces instances which are the same up to syntax (like reordering)*) @@ -180,21 +167,18 @@ Section fixX. Global Instance term_repEl : computableTime' (@repeat X) (fun e _ => (c__repeat2, fun n _ => (repeat_time n, tt))). Proof. extract. solverec. all: unfold repeat_time, c__repeat, c__repeat2; solverec. - Qed. - - Lemma repeat_time_mono : monotonic repeat_time. - Proof. - unfold repeat_time; smpl_inO. - Qed. + Qed. + #[export] Instance repat_time_mono: Proper (le ==> le) repeat_time. + Proof. unfold repeat_time. solve_proper. Qed. Definition poly__repeat n := (n+1) * c__repeat. Lemma repeat_time_bound n : repeat_time n <= poly__repeat (size (enc n)). Proof. unfold repeat_time, poly__repeat. replace_le n with (size (enc n)) by (apply size_nat_enc_r) at 1. lia. Qed. - Lemma repEl_poly : monotonic poly__repeat /\ inOPoly poly__repeat. + Lemma repEl_poly : inOPoly poly__repeat. Proof. - unfold poly__repeat; split; smpl_inO. + unfold poly__repeat; smpl_inO. Qed. End fixX. @@ -212,11 +196,12 @@ Definition c__hNat := 2 * (c__leb2 + 2 * c__repeat2 + 18 + 2* c__app + 2 * c__su Definition hNat_time sig n := (leb_time (S n) sig + repeat_time sig + sig + 1) * c__hNat. #[export] Instance term_hNat : computableTime' hNat (fun sig _ => (1, fun n _ => (hNat_time sig n, tt))). -Proof. - specialize repeat_time_mono as H1. unfold monotonic in H1. +Proof. extract. solverec. - setoid_rewrite sub_time_bound_r at 2. rewrite repeat_length. - apply leb_iff in H. rewrite H1 with (x' := x) by lia. setoid_rewrite H1 with (x' := x) at 2. 2: lia. + apply leb_iff in H. + setoid_replace (x - x0 - 1) with x using relation le by lia. + setoid_replace x0 with x using relation le at 3 by lia. replace_le x0 with x by lia at 3. rewrite sub_time_bound_l. unfold hNat_time, c__hNat. cbn[Nat.add]. unfold c__sub1, c__sub. nia. @@ -232,10 +217,10 @@ Proof. unfold poly__hNat, c__hNatBound. rewrite repeat_time_bound. rewrite size_nat_enc_r with (n := sig) at 3. lia. Qed. -Lemma hNat_poly : monotonic poly__hNat /\ inOPoly poly__hNat. -Proof. - unfold poly__hNat; split; smpl_inO; apply repEl_poly. -Qed. +Lemma hNat_poly : inOPoly poly__hNat. +Proof. unfold poly__hNat; smpl_inO; apply repEl_poly. Qed. +#[export] Instance hNat_mono: Proper (le ==> le) poly__hNat. +Proof. unfold poly__hNat. solve_proper. Qed. (** hflat *) Definition c__hflat := c__Sigma + 3. @@ -268,30 +253,27 @@ Proof. unfold hflat_time. rewrite map_time_bound_env. 2: { split; [ intros | ]. - - rewrite hNat_time_bound. poly_mono hNat_poly. 2: apply Nat.le_add_r with (m := size (enc ele)). reflexivity. - - apply hNat_poly. + - rewrite hNat_time_bound. + setoid_replace (size (enc env)) with (size (enc env) + size (enc ele)) + using relation le at 1 by apply Nat.le_add_r. + reflexivity. + - solve_proper. } - poly_mono hNat_poly. - 2: (replace_le (size (enc (Sigma fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia)); reflexivity. - - rewrite concat_time_bound. poly_mono concat_poly. - 2: { - rewrite map_hNat_size_bound. rewrite list_size_length. - replace_le (Sigma fpr) with (size (enc fpr)) by (rewrite size_nat_enc_r with (n := Sigma fpr); rewrite FlatCC_enc_size; lia). - reflexivity. - } + replace_le (size (enc (Sigma fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia); reflexivity. + rewrite concat_time_bound. + rewrite map_hNat_size_bound. rewrite list_size_length. + replace_le (Sigma fpr) with (size (enc fpr)) by (rewrite size_nat_enc_r with (n := Sigma fpr); rewrite FlatCC_enc_size; lia). unfold poly__concat. - rewrite list_size_length. replace_le (size (enc l)) with (size (enc fpr) + size (enc l)) by lia at 1 3. replace_le (size (enc fpr)) with (size (enc fpr) + size (enc l)) by lia at 4. replace_le (size (enc l)) with (size (enc fpr) + size (enc l)) by lia at 5. set (size (enc fpr) + size (enc l)). unfold poly__hflat. nia. Qed. -Lemma hflat_poly : monotonic poly__hflat /\ inOPoly poly__hflat. -Proof. - split; unfold poly__hflat; smpl_inO; apply hNat_poly. -Qed. +Lemma hflat_poly : inOPoly poly__hflat. +Proof. unfold poly__hflat; smpl_inO; apply hNat_poly. Qed. +#[export] Instance hflat_mono: Proper (le ==> le) poly__hflat. +Proof. unfold poly__hflat. solve_proper. Qed. Lemma hflat_length fpr l : |hflat fpr l| = (Sigma fpr) * |l|. Proof. @@ -320,15 +302,15 @@ Definition poly__hcard n := poly__hflat n + poly__hflat n + c__hcard. Lemma hcard_time_bound fpr card : hcard_time fpr card <= poly__hcard (size (enc fpr) + size (enc card)). Proof. unfold hcard_time. rewrite !hflat_time_bound. - unfold poly__hcard. - poly_mono hflat_poly. 2: { replace_le (size (enc (prem card))) with (size (enc card)) by (rewrite CCCard_enc_size; lia). reflexivity. } - poly_mono hflat_poly at 2. 2: { replace_le (size (enc (conc card))) with (size (enc card)) by (rewrite CCCard_enc_size; lia). reflexivity. } - lia. -Qed. -Lemma hcard_poly : monotonic poly__hcard /\ inOPoly poly__hcard. -Proof. - unfold poly__hcard; split; smpl_inO; apply hflat_poly. + unfold poly__hcard. + replace_le (size (enc (prem card))) with (size (enc card)) by (rewrite CCCard_enc_size; lia). + replace_le (size (enc (conc card))) with (size (enc card)) by (rewrite CCCard_enc_size; lia). + reflexivity. Qed. +Lemma hcard_poly : inOPoly poly__hcard. +Proof. unfold poly__hcard; smpl_inO; apply hflat_poly. Qed. +#[export] Instance hcard_mono: Proper (le ==> le) poly__hcard. +Proof. unfold poly__hcard. solve_proper. Qed. Definition c__hcardSize1 := c__listsizeNil + c__listsizeNil + c__sizeCCCard. Definition c__hcardSize2 := 2 * c__hflatSize. @@ -356,18 +338,15 @@ Definition poly__hcards n := ((n + 1) * (poly__hcard (n+ n) + 1) + 1) * c__hcar Lemma hcards_time_bound fpr : hcards_time fpr <= poly__hcards (size (enc fpr)). Proof. unfold hcards_time. - rewrite map_time_bound_env. 2: split; [ intros; apply hcard_time_bound | apply hcard_poly]. + rewrite map_time_bound_env. 2: split; [ intros; apply hcard_time_bound | solve_proper]. rewrite list_size_length. - replace_le (size (enc (cards fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. - poly_mono hcard_poly. - 2: { replace_le (size (enc (cards fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. reflexivity. } + replace_le (size (enc (cards fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1 2. unfold poly__hcards, c__hcardsBound. lia. Qed. -Lemma hcards_poly : monotonic poly__hcards /\ inOPoly poly__hcards. +Lemma hcards_poly : inOPoly poly__hcards. Proof. - unfold poly__hcards; split; smpl_inO. - - apply hcard_poly. - - eapply inOPoly_comp; [apply hcard_poly | apply hcard_poly | smpl_inO]. + unfold poly__hcards; smpl_inO. + apply inOPoly_comp; [solve_proper | apply hcard_poly | smpl_inO]. Qed. Definition c__hcardsSize1 := c__hcardSize1 + c__listsizeNil. @@ -397,18 +376,16 @@ Definition poly__hfinal n := ((n + 1) * (poly__hflat (n+ n) + 1) + 1) * c__hfin Lemma hfinal_time_bound fpr : hfinal_time fpr <= poly__hfinal (size (enc fpr)). Proof. unfold hfinal_time. - rewrite map_time_bound_env. 2: split; [ intros; apply hflat_time_bound | apply hflat_poly]. + rewrite map_time_bound_env. 2: split; [ intros; apply hflat_time_bound | solve_proper]. rewrite list_size_length. replace_le (size (enc (final fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. - poly_mono hflat_poly. - 2: { replace_le (size (enc (final fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. reflexivity. } + replace_le (size (enc (final fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. unfold poly__hfinal, c__hfinalBound. lia. Qed. -Lemma hfinal_poly : monotonic poly__hfinal /\ inOPoly poly__hfinal. +Lemma hfinal_poly : inOPoly poly__hfinal. Proof. - unfold poly__hfinal; split; smpl_inO. - - apply hflat_poly. - - eapply inOPoly_comp; [apply hflat_poly | apply hflat_poly | smpl_inO]. + unfold poly__hfinal; smpl_inO. + apply inOPoly_comp; [solve_proper | apply hflat_poly | smpl_inO]. Qed. (** one could obtain a linear time bound, but a quadratic bound is easier to prove *) @@ -442,16 +419,17 @@ Proof. replace_le (offset fpr) with (size (enc fpr)) by (rewrite size_nat_enc_r, FlatCC_enc_size; lia). replace_le (width fpr) with (size (enc fpr)) by (rewrite size_nat_enc_r, FlatCC_enc_size; lia). rewrite hflat_time_bound. - poly_mono hflat_poly. - 2: { (replace_le (size (enc (init fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia)); reflexivity. } + replace_le (size (enc (init fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia). rewrite hfinal_time_bound. rewrite hcards_time_bound. unfold poly__hBinaryCC. lia. Qed. -Lemma hBinaryCC_poly : monotonic poly__hBinaryCC /\ inOPoly poly__hBinaryCC. +Lemma hBinaryCC_poly : inOPoly poly__hBinaryCC. Proof. - split; unfold poly__hBinaryCC; smpl_inO. all: try solve [apply hflat_poly | apply hcards_poly | apply hfinal_poly ]. - eapply inOPoly_comp; [apply hflat_poly | apply hflat_poly | smpl_inO]. -Qed. + unfold poly__hBinaryCC; smpl_inO. + - apply inOPoly_comp; [solve_proper | exact hflat_poly | smpl_inO]. + - exact hcards_poly. + - exact hfinal_poly. +Qed. Proposition nat_mul_size_bound n m : size (enc (n * m)) <= size (enc n) * size (enc m). Proof. @@ -498,14 +476,25 @@ Proof. unfold reduction_time, poly__reduction. rewrite FlatCC_wf_dec_time_bound, isValidFlattening_dec_time_bound, hBinaryCC_time_bound. lia. Qed. -Lemma reduction_poly : monotonic poly__reduction /\ inOPoly poly__reduction. +Lemma reduction_poly : inOPoly poly__reduction. Proof. - split; unfold poly__reduction; smpl_inO. - all: try solve [ apply FlatCC_wf_dec_poly | apply isValidFlatteningDec_poly | apply hBinaryCC_poly]. -Qed. + unfold poly__reduction; smpl_inO. + - exact FlatCC_wf_dec_poly. + - exact isValidFlatteningDec_poly. + - exact hBinaryCC_poly. +Qed. + +#[export] Instance hBinaryCC_mono: Proper (le ==> le) poly__hBinaryCC. +Proof. unfold poly__hBinaryCC, poly__hflat, poly__hcards, poly__hfinal. solve_proper. Qed. +#[export] Instance isValidFlatteningDec_mono: Proper (le ==> le) poly__isValidFlatteningDec. +Proof. unfold poly__isValidFlatteningDec. solve_proper. Qed. +#[export] Instance FlatCCWfDec_mono: Proper (le ==> le) poly__FlatCCWfDec. +Proof. unfold poly__FlatCCWfDec. solve_proper. Qed. +#[export] Instance reduction_mono: Proper (le ==> le) poly__reduction. +Proof. unfold poly__reduction. solve_proper. Qed. (** size bound *) -Lemma reduction_size_bound : {f | (forall fpr, size (enc (reduction fpr)) <= f (size (enc fpr))) /\ inOPoly f /\ monotonic f}. +Lemma reduction_size_bound : {f | (forall fpr, size (enc (reduction fpr)) <= f (size (enc fpr))) /\ inOPoly f /\ Proper (le ==> le) f}. Proof. exists (fun n => c__hBinaryCCSize * (n + 1)^3 + c__hBinaryCCSize2 + 32). split; [ | split]. @@ -515,7 +504,7 @@ Proof. + unfold trivialNoInstance. rewrite BinaryCC_enc_size. cbn -[Nat.mul Nat.add]. rewrite !size_nat_enc. rewrite !size_list. cbn. lia. - unfold Nat.pow. smpl_inO. - - smpl_inO. + - solve_proper. Qed. (** This is the polynomial-time result of the reduction. @@ -528,7 +517,7 @@ Proof. + extract. solverec. all: specialize (reduction_time_bound x) as H1; unfold reduction_time, c__reduction in H1; lia. + apply reduction_poly. - + apply reduction_poly. + + solve_proper. + destruct (reduction_size_bound) as (f & H1 & H2 & H3). exists f; auto. - apply FlatCC_to_BinaryCC. Qed. diff --git a/theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v b/theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v index 658d5159..98b36936 100644 --- a/theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v +++ b/theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v @@ -173,9 +173,9 @@ Proof. unfold flatPolSigma_time. rewrite flatStateSigma_bound. unfold poly__flatPolSigma. rewrite sig_TM_le. nia. Qed. -Lemma flatPolSigma_poly : monotonic poly__flatPolSigma /\ inOPoly poly__flatPolSigma. +Lemma flatPolSigma_poly : inOPoly poly__flatPolSigma. Proof. - unfold poly__flatPolSigma; split; smpl_inO. + unfold poly__flatPolSigma; smpl_inO. Qed. Definition c__flatTapeSigma := c__add1 + 1 + (flatDelim + 1) * c__add. @@ -201,10 +201,10 @@ Proof. unfold flatStates_time. unfold mult_time. rewrite flatStateSigma_bound. rewrite states_TM_le, sig_TM_le. unfold poly__flatStates. nia. Qed. -Lemma flatStates_poly : monotonic poly__flatStates /\ inOPoly poly__flatStates. -Proof. - unfold poly__flatStates; split; smpl_inO. -Qed. +Lemma flatStates_poly : inOPoly poly__flatStates. +Proof. unfold poly__flatStates; smpl_inO. Qed. +#[export] Instance flatStates_mono: Proper (le ==> le) poly__flatStates. +Proof. unfold poly__flatStates. solve_proper. Qed. Definition c__flatGamma := c__add1 + 1. Definition flatGamma_time (tm : flatTM) := flatStates_time tm + flatTapeSigma_time tm + add_time (flatStates tm) + c__flatGamma. @@ -224,10 +224,12 @@ Proof. rewrite states_TM_le, sig_TM_le. unfold poly__flatGamma. nia. Qed. -Lemma flatGamma_poly : monotonic poly__flatGamma /\ inOPoly poly__flatGamma. +Lemma flatGamma_poly : inOPoly poly__flatGamma. Proof. - unfold poly__flatGamma; split; smpl_inO; first [apply flatStates_poly | apply flatPolSigma_poly]. -Qed. + unfold poly__flatGamma; smpl_inO; first [apply flatStates_poly | apply flatPolSigma_poly]. +Qed. +#[export] Instance flatGamma_mono: Proper (le ==> le) poly__flatGamma. +Proof. unfold poly__flatGamma, poly__flatStates, poly__flatPolSigma. solve_proper. Qed. Definition c__flatPreludeSig' :=c__add1 + 5 * c__add + 22. #[export] @@ -253,10 +255,10 @@ Proof. rewrite sig_TM_le, states_TM_le. unfold poly__flatAlphabet. nia. Qed. -Lemma flatAlphabet_poly : monotonic poly__flatAlphabet /\ inOPoly poly__flatAlphabet. -Proof. - unfold poly__flatAlphabet; split; smpl_inO; apply flatGamma_poly. -Qed. +Lemma flatAlphabet_poly : inOPoly poly__flatAlphabet. +Proof. unfold poly__flatAlphabet; smpl_inO; apply flatGamma_poly. Qed. +#[export] Instance flatAlphabet_mono: Proper (le ==> le) poly__flatAlphabet. +Proof. unfold poly__flatAlphabet. solve_proper. Qed. (** flattenPolarity *) @@ -307,10 +309,10 @@ Proof. - lia. - unfold nth_error_time. rewrite H1. rewrite Nat.le_min_l. nia. Qed. -Lemma generatePolarityFlat_poly : monotonic poly__generatePolarityFlat /\ inOPoly poly__generatePolarityFlat. -Proof. - unfold poly__generatePolarityFlat; split; smpl_inO. -Qed. +Lemma generatePolarityFlat_poly : inOPoly poly__generatePolarityFlat. +Proof. unfold poly__generatePolarityFlat; smpl_inO. Qed. +#[export] Instance generatePolarityFlat_mono: Proper (le ==> le) poly__generatePolarityFlat. +Proof. unfold poly__generatePolarityFlat. solve_proper. Qed. Lemma generatePolarityFlat_ofFlatType tm env c n: envOfFlatTypes tm env -> generatePolarityFlat env c = Some n -> n < flatPolarity. Proof. @@ -365,10 +367,10 @@ Proof. - unfold nth_error_time. rewrite H1, Nat.le_min_l. nia. - unfold nth_error_time. rewrite H2, Nat.le_min_l. nia. Qed. -Lemma generateStateSigmaFlat_poly : monotonic poly__generateStateSigmaFlat /\ inOPoly poly__generateStateSigmaFlat. -Proof. - unfold poly__generateStateSigmaFlat; split; smpl_inO. -Qed. +Lemma generateStateSigmaFlat_poly : inOPoly poly__generateStateSigmaFlat. +Proof. unfold poly__generateStateSigmaFlat; smpl_inO. Qed. +#[export] Instance generateStateSigmaFlat_mono: Proper (le ==> le) poly__generateStateSigmaFlat. +Proof. unfold poly__generateStateSigmaFlat. solve_proper. Qed. Lemma generateStateSigmaFlat_ofFlatType tm n env c : envOfFlatTypes tm env -> generateStateSigmaFlat env c = Some n -> n < flatStateSigma tm. @@ -417,13 +419,8 @@ Proof. intros H H0. unfold generatePolSigmaFlat_time. destruct c as (p & s). rewrite generatePolarityFlat_time_bound by apply H. - rewrite generateStateSigmaFlat_time_bound by apply H. - poly_mono generatePolarityFlat_poly. 2: { - replace_le n with (size (enc tm) + n) by lia at 1. reflexivity. - } - poly_mono generateStateSigmaFlat_poly. 2: { - replace_le n with (size (enc tm) + n) by lia at 1. reflexivity. - } + rewrite generateStateSigmaFlat_time_bound by apply H. + replace_le n with (size (enc tm) + n) by lia at 1 2. destruct generatePolarityFlat eqn:H1. - destruct generateStateSigmaFlat eqn:H2. + unfold flatPair_time, mult_time, add_time, flatOption. @@ -433,9 +430,9 @@ Proof. + unfold poly__generatePolSigmaFlat. lia. - unfold poly__generatePolSigmaFlat. lia. Qed. -Lemma generatePolSigmaFlat_poly : monotonic poly__generatePolSigmaFlat /\ inOPoly poly__generatePolSigmaFlat. +Lemma generatePolSigmaFlat_poly : inOPoly poly__generatePolSigmaFlat. Proof. - unfold poly__generatePolSigmaFlat; split; smpl_inO; first [apply generatePolarityFlat_poly | apply generateStateSigmaFlat_poly]. + unfold poly__generatePolSigmaFlat; smpl_inO; first [apply generatePolarityFlat_poly | apply generateStateSigmaFlat_poly]. Qed. Lemma generatePolSigmaFlat_ofFlatType tm env c n: envOfFlatTypes tm env -> generatePolSigmaFlat tm env c = Some n -> n < flatPolSigma tm. @@ -477,10 +474,12 @@ Proof. - lia. - rewrite (generatePolSigmaFlat_time_bound _ H H0). lia. Qed. -Lemma generateTapeSigmaFlat_poly : monotonic poly__generateTapeSigmaFlat /\ inOPoly poly__generateTapeSigmaFlat. +Lemma generateTapeSigmaFlat_poly : inOPoly poly__generateTapeSigmaFlat. Proof. - unfold poly__generateTapeSigmaFlat; split; smpl_inO; apply generatePolSigmaFlat_poly. -Qed. + unfold poly__generateTapeSigmaFlat; smpl_inO; apply generatePolSigmaFlat_poly. +Qed. +#[export] Instance generateTapeSigmaFlat_mono: Proper (le ==> le) poly__generateTapeSigmaFlat. +Proof. unfold poly__generateTapeSigmaFlat, poly__generatePolSigmaFlat. solve_proper. Qed. Lemma generateTapeSigmaFlat_ofFlatType tm env c n : envOfFlatTypes tm env -> generateTapeSigmaFlat tm env c = Some n -> n < flatTapeSigma tm. Proof. @@ -517,8 +516,7 @@ Proof. rewrite (generateStateSigmaFlat_time_bound _ H). destruct H as (_ & _ & _ & H). unfold nth_error_time. rewrite H. rewrite Nat.le_min_l. - poly_mono generateStateSigmaFlat_poly. - 2: { replace_le n with (size (enc tm) + n) by lia at 1. reflexivity. } + replace_le n with (size (enc tm) + n) by lia at 2. destruct nth_error eqn:H1. - unfold flatPair_time, flatOption, add_time, mult_time. apply nth_error_In in H1. apply H0 in H1. unfold ofFlatType in H1. rewrite H1. @@ -533,11 +531,11 @@ Proof. unfold poly__generateStatesFlat. generalize (size (enc tm) + n). intros n'. nia. - unfold poly__generateStatesFlat. lia. Qed. -Lemma generateStatesFlat_poly : monotonic poly__generateStatesFlat /\ inOPoly poly__generateStatesFlat. +Lemma generateStatesFlat_poly : inOPoly poly__generateStatesFlat. Proof. - unfold poly__generateStatesFlat; split; smpl_inO; apply generateStateSigmaFlat_poly. + unfold poly__generateStatesFlat; smpl_inO; apply generateStateSigmaFlat_poly. Qed. - + Lemma generateStatesFlat_ofFlatType env tm n c : envOfFlatTypes tm env -> generateStatesFlat tm env c = Some n -> n < flatStates tm. Proof. intros H. unfold generateStatesFlat. @@ -580,14 +578,13 @@ Proof. - rewrite flatStates_time_bound, generateTapeSigmaFlat_time_bound by easy. unfold add_time. rewrite flatStates_bound. rewrite sig_TM_le, states_TM_le. - poly_mono flatStates_poly. - 2: { replace_le (size (enc tm)) with (size (enc tm) + n) by lia at 1. reflexivity. } + replace_le (size (enc tm)) with (size (enc tm) + n) by lia at 1. unfold poly__generateGammaFlat. lia. Qed. -Lemma generateGammaFlat_poly : monotonic poly__generateGammaFlat /\ inOPoly poly__generateGammaFlat. +Lemma generateGammaFlat_poly : inOPoly poly__generateGammaFlat. Proof. - unfold poly__generateGammaFlat; split; smpl_inO; first [apply flatStates_poly | apply generateTapeSigmaFlat_poly | apply generateStatesFlat_poly ]. -Qed. + unfold poly__generateGammaFlat; smpl_inO; first [apply flatStates_poly | apply generateTapeSigmaFlat_poly | apply generateStatesFlat_poly ]. +Qed. Lemma generateGammaFlat_ofFlatType tm env f n: envOfFlatTypes tm env -> generateGammaFlat tm env f = Some n -> ofFlatType (flatGamma tm) n. Proof. @@ -626,10 +623,10 @@ Proof. 5: { unfold nth_error_time. destruct H as (_ & H1 & _). rewrite H1, Nat.le_min_l. lia. } all: lia. Qed. -Lemma generatePreludeSigPFlat_poly : monotonic poly__generatePreludeSigPFlat /\ inOPoly poly__generatePreludeSigPFlat. -Proof. - unfold poly__generatePreludeSigPFlat; split; smpl_inO. -Qed. +Lemma generatePreludeSigPFlat_poly : inOPoly poly__generatePreludeSigPFlat. +Proof. unfold poly__generatePreludeSigPFlat; smpl_inO. Qed. +#[export] Instance generatePreludeSigPFlat_mono: Proper (le ==> le) poly__generatePreludeSigPFlat. +Proof. unfold poly__generatePreludeSigPFlat. solve_proper. Qed. Lemma generatePreludeSigP_ofFlatType tm env f n : envOfFlatTypes tm env -> generatePreludeSigPFlat env f = Some n -> ofFlatType (flatPreludeSig' tm) n. Proof. @@ -669,16 +666,16 @@ Proof. intros H H0. unfold generateAlphabetFlat_time. unfold poly__generateAlphabetFlat. destruct c. - rewrite generateGammaFlat_time_bound by easy. lia. - rewrite generatePreludeSigPFlat_time_bound by easy. - poly_mono generatePreludeSigPFlat_poly. 2: { replace_le n with (size (enc tm) + n) by lia at 1. reflexivity. } + replace_le n with (size (enc tm) + n) by lia at 1. rewrite flatGamma_time_bound. - poly_mono flatGamma_poly. 2: { replace_le (size (enc tm)) with (size (enc tm) + n) by lia at 1. reflexivity. } + replace_le (size (enc tm)) with (size (enc tm) + n) by lia at 1. unfold add_time. rewrite flatGamma_bound. rewrite sig_TM_le, states_TM_le. leq_crossout. Qed. -Lemma generateAlphabetFlat_poly : monotonic poly__generateAlphabetFlat /\ inOPoly poly__generateAlphabetFlat. +Lemma generateAlphabetFlat_poly : inOPoly poly__generateAlphabetFlat. Proof. - unfold poly__generateAlphabetFlat; split; smpl_inO; first [apply generateGammaFlat_poly | apply flatGamma_poly | apply generatePreludeSigPFlat_poly]. + unfold poly__generateAlphabetFlat; smpl_inO; first [apply generateGammaFlat_poly | apply flatGamma_poly | apply generatePreludeSigPFlat_poly]. Qed. Lemma generateAlphabetFlat_ofFlatType tm env f n: envOfFlatTypes tm env -> generateAlphabetFlat tm env f = Some n -> ofFlatType (flatAlphabet tm) n. @@ -717,9 +714,14 @@ Proof. rewrite !generateAlphabetFlat_time_bound by eauto. unfold poly__generateCard; lia. Qed. -Lemma generateCard_poly : monotonic poly__generateCard /\ inOPoly poly__generateCard. -Proof. - split; unfold poly__generateCard; smpl_inO; apply generateAlphabetFlat_poly. +Lemma generateCard_poly : inOPoly poly__generateCard. +Proof. unfold poly__generateCard; smpl_inO; apply generateAlphabetFlat_poly. Qed. +#[export] Instance generateCard_mono: Proper (le ==> le) poly__generateCard. +Proof. + unfold poly__generateCard, poly__generateAlphabetFlat, poly__generateGammaFlat, + poly__flatStates, poly__generateTapeSigmaFlat, poly__generatePolSigmaFlat, + poly__generatePolarityFlat, poly__generateStateSigmaFlat, poly__generateStatesFlat. + solve_proper. Qed. Lemma generateCardFlat_ofFlatType tm env rule card: envOfFlatTypes tm env -> generateCardFlat tm env rule = Some card -> TCCCard_ofFlatType card (flatAlphabet tm). @@ -757,9 +759,9 @@ Section fixListDistr. Proof. unfold list_distr_time, poly__listDistr. rewrite !list_size_length. leq_crossout. Qed. - Lemma list_prod_poly : monotonic poly__listDistr /\ inOPoly poly__listDistr. + Lemma list_prod_poly : inOPoly poly__listDistr. Proof. - unfold poly__listDistr; split; smpl_inO. + unfold poly__listDistr; smpl_inO. Qed. Lemma list_distr_length (l1 : list X) l2 : |list_distr l1 l2| = |l1| * |l2|. @@ -839,10 +841,10 @@ Proof. replace_le ((|l| + 1) ^ num) with ((|l| + 1)^(S num)) by cbn; nia. unfold c__mkVarEnvB1, c__mkVarEnvB2. leq_crossout. Qed. -Lemma mkVarEnv_poly n : monotonic (poly__mkVarEnv n) /\ inOPoly (poly__mkVarEnv n). -Proof. - unfold poly__mkVarEnv. split; smpl_inO. -Qed. +Lemma mkVarEnv_poly n : inOPoly (poly__mkVarEnv n). +Proof. unfold poly__mkVarEnv. smpl_inO. Qed. +#[export] Instance mkVarEnv_mono: Proper (eq ==> le ==> le) poly__mkVarEnv. +Proof. intros _ n ->. unfold poly__mkVarEnv. solve_proper. Qed. (** tupToEvalEnv *) Definition c__tupToEvalEnv := 17. @@ -879,9 +881,9 @@ Section fixprodLists. unfold prodLists_time. rewrite !list_size_length. unfold poly__prodLists. solverec. Qed. - Lemma prodLists_poly : monotonic poly__prodLists /\ inOPoly poly__prodLists. + Lemma prodLists_poly : inOPoly poly__prodLists. Proof. - unfold poly__prodLists; split; smpl_inO. + unfold poly__prodLists; smpl_inO. Qed. End fixprodLists. @@ -938,19 +940,25 @@ Proof. match goal with [ |- context [?a + mkVarEnv_time (seq 0 flatPolarity) ?b] ] => replace_le a with ((flatPolarity + 3 * size (enc tm) + 5) * c__seq) by nia end. rewrite !mkVarEnv_time_bound. rewrite !seq_length. unfold prodLists_time. rewrite !prod_length, !mkVarEnv_length, !seq_length. - poly_mono (mkVarEnv_poly n2). 2: { rewrite sig_TM_le. reflexivity. } - poly_mono (mkVarEnv_poly n3). 2: { rewrite flatStateSigma_bound, sig_TM_le. reflexivity. } - poly_mono (mkVarEnv_poly n4). 2: { rewrite states_TM_le. reflexivity. } + rewrite sig_TM_le at 1. + rewrite flatStateSigma_bound, sig_TM_le at 1. + rewrite states_TM_le at 1. rewrite flatStateSigma_bound. - rewrite !sig_TM_le, !states_TM_le. + rewrite !sig_TM_le, !states_TM_le. repeat match goal with [ |- context[?a + 1 + 1]] => replace (a + 1 + 1) with (a + 2) by lia end. unfold poly__makeAllEvalEnvFlat. leq_crossout. Qed. -Lemma makeAllEvalEnvFlat_poly n1 n2 n3 n4 : monotonic (poly__makeAllEvalEnvFlat n1 n2 n3 n4) /\ inOPoly (poly__makeAllEvalEnvFlat n1 n2 n3 n4). +Lemma makeAllEvalEnvFlat_poly n1 n2 n3 n4 : inOPoly (poly__makeAllEvalEnvFlat n1 n2 n3 n4). Proof. - unfold poly__makeAllEvalEnvFlat; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: apply mkVarEnv_poly. -Qed. + unfold poly__makeAllEvalEnvFlat; smpl_inO; apply inOPoly_comp. + all: first [apply mkVarEnv_poly | solve_proper | smpl_inO ]. +Qed. +#[export] Instance makeAllEvalEnvFlat_mono n1 n2 n3 n4: + Proper (le ==> le) (poly__makeAllEvalEnvFlat n1 n2 n3 n4). +Proof. unfold poly__makeAllEvalEnvFlat. solve_proper. Qed. + +(* see https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Rewrite.20gets.20stuck/near/318011578 *) +#[global] Typeclasses Opaque poly__makeAllEvalEnvFlat. Lemma makeAllEvalEnvFlat_envOfFlatTypes tm n1 n2 n3 n4 : forall e, e el makeAllEvalEnvFlat tm n1 n2 n3 n4 -> envOfFlatTypes tm e. Proof. @@ -984,10 +992,13 @@ Proof. unfold poly__makeAllEvalEnvFlatLength. replace (size (enc tm) + 1 + 1) with (size (enc tm) + 2) by lia. nia. Qed. -Lemma makeAllEvalEnvFlat_length_poly n1 n2 n3 n4 : monotonic (poly__makeAllEvalEnvFlatLength n1 n2 n3 n4) /\ inOPoly (poly__makeAllEvalEnvFlatLength n1 n2 n3 n4). +Lemma makeAllEvalEnvFlat_length_poly n1 n2 n3 n4 : inOPoly (poly__makeAllEvalEnvFlatLength n1 n2 n3 n4). Proof. - unfold poly__makeAllEvalEnvFlatLength; split; smpl_inO. + unfold poly__makeAllEvalEnvFlatLength; smpl_inO. Qed. +#[global] Instance makeAllEvalEnvFlatLength_mono n1 n2 n3 n4: + Proper (le ==> le) (poly__makeAllEvalEnvFlatLength n1 n2 n3 n4). +Proof. unfold poly__makeAllEvalEnvFlatLength. solve_proper. Qed. (** filterSome *) Section fixfilterSome. @@ -1013,9 +1024,9 @@ Section fixfilterSome. Proof. unfold filterSome_time, poly__filterSome. rewrite list_size_length. lia. Qed. - Lemma filterSome_poly : monotonic poly__filterSome /\ inOPoly poly__filterSome. + Lemma filterSome_poly : inOPoly poly__filterSome. Proof. - unfold poly__filterSome; split; smpl_inO. + unfold poly__filterSome; smpl_inO. Qed. End fixfilterSome. @@ -1053,19 +1064,15 @@ Proof. intros H. unfold makeCardsP_flat_time. unfold makeCardsP_flat_step_time. rewrite map_time_mono with (f2 := fun _ => poly__generateCard(size (enc tm) + n) + c__makeCardsPFlatStep). 2: { intros e [H1 H2]%H. rewrite (generateCard_time_bound _ H2 H1). lia. } - rewrite map_time_const. - poly_mono generateCard_poly. 2: { instantiate (1 := size (enc tm) + n + (|envs|)). lia. } + rewrite map_time_const. + setoid_replace (size (enc tm) + n) with (size (enc tm) + n + (|envs|)) + using relation le at 1 by lia. unfold poly__makeCards'. nia. Qed. -Lemma makeCardsP_poly : monotonic poly__makeCards' /\ inOPoly poly__makeCards'. -Proof. - unfold poly__makeCards'; split; smpl_inO; apply generateCard_poly. -Qed. - -Lemma filterSome_length (X : Type) (l : list (option X)) : |filterSome l| <= |l|. -Proof. - induction l; cbn; [lia | destruct a; cbn; lia]. -Qed. +Lemma makeCardsP_poly : inOPoly poly__makeCards'. +Proof. unfold poly__makeCards'; smpl_inO; apply generateCard_poly. Qed. +#[export] Instance makeCardsP_mono: Proper (le ==> le) poly__makeCards'. +Proof. unfold poly__makeCards'. solve_proper. Qed. Lemma makeCardsP_length tm envs card: |makeCardsP_flat tm envs card| <= |envs|. Proof. @@ -1094,14 +1101,15 @@ Proof. rewrite map_time_const. rewrite concat_time_exp. rewrite map_map, map_length. rewrite sumn_map_mono with (f2 := fun _ => c__concat * |envs|). 2: { intros card _. rewrite makeCardsP_length. unfold evalEnvFlat. lia. } - rewrite sumn_map_const. - poly_mono makeCardsP_poly. 2: { instantiate (1 := size (enc tm) + n + (|envs|) + (|cards|)). lia. } + rewrite sumn_map_const. + setoid_replace (size (enc tm) + n + (| envs |)) with (size (enc tm) + n + (|envs|) + (|cards|)) + using relation le at 1 by lia. unfold poly__makeCardsFlat. lia. Qed. -Lemma makeCardsFlat_poly : monotonic poly__makeCardsFlat /\ inOPoly poly__makeCardsFlat. -Proof. - unfold poly__makeCardsFlat; split; smpl_inO; apply makeCardsP_poly. -Qed. +Lemma makeCardsFlat_poly : inOPoly poly__makeCardsFlat. +Proof. unfold poly__makeCardsFlat; smpl_inO; apply makeCardsP_poly. Qed. +#[export] Instance makeCardsFlat_mono: Proper (le ==> le) poly__makeCardsFlat. +Proof. unfold poly__makeCardsFlat. solve_proper. Qed. Lemma makeCardsFlat_length_bound tm envs cards : |makeCardsFlat tm envs cards| <= |envs| * |cards|. Proof. @@ -1203,20 +1211,27 @@ Qed. Definition poly__flatMTRCards n := poly__makeAllEvalEnvFlat 1 4 0 0 n + poly__makeCardsFlat (n + 4 + poly__makeAllEvalEnvFlatLength 1 4 0 0 n + |mtrRules|) + c__flatMTRCards. Lemma flatMTRCards_time_bound tm : flatMTRCards_time tm <= poly__flatMTRCards (size (enc tm)). -Proof. - unfold flatMTRCards_time. - rewrite makeAllEvalEnvFlat_time_bound. - rewrite makeCardsFlat_time_bound. 2: apply makeAllEvalEnvFlat_envBounded. +Proof. + unfold flatMTRCards_time. + rewrite makeAllEvalEnvFlat_time_bound. + rewrite makeCardsFlat_time_bound. + 2: apply makeAllEvalEnvFlat_envBounded. cbn [max]. - poly_mono makeCardsFlat_poly. - 2: { rewrite makeAllEvalEnvFlat_length_bound. reflexivity. } - unfold poly__flatMTRCards. nia. + rewrite makeAllEvalEnvFlat_length_bound. + unfold poly__flatMTRCards. reflexivity. Qed. -Lemma flatMTRCards_poly : monotonic poly__flatMTRCards /\ inOPoly poly__flatMTRCards. + +Lemma flatMTRCards_poly : inOPoly poly__flatMTRCards. Proof. - unfold poly__flatMTRCards; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply makeAllEvalEnvFlat_poly | apply makeCardsFlat_poly | apply makeAllEvalEnvFlat_length_poly]. + unfold poly__flatMTRCards; smpl_inO. + - apply makeAllEvalEnvFlat_poly. + - apply inOPoly_comp. + + solve_proper. + + exact makeCardsFlat_poly. + + smpl_inO. apply makeAllEvalEnvFlat_length_poly. Qed. +#[export] Instance flatMTRCards_mono: Proper (le ==> le) poly__flatMTRCards. +Proof. unfold poly__flatMTRCards. solve_proper. Qed. Definition c__flatMTICards := 25. Definition flatMTICards_time (tm : flatTM) := makeAllEvalEnvFlat_time tm 2 0 4 0 + makeCardsFlat_time tm (makeAllEvalEnvFlat tm 2 0 4 0) mtiRules + c__flatMTICards. @@ -1234,15 +1249,18 @@ Proof. rewrite makeAllEvalEnvFlat_time_bound. rewrite makeCardsFlat_time_bound. 2: apply makeAllEvalEnvFlat_envBounded. cbn [max]. - poly_mono makeCardsFlat_poly. - 2: { rewrite makeAllEvalEnvFlat_length_bound. reflexivity. } - unfold poly__flatMTICards. nia. + rewrite makeAllEvalEnvFlat_length_bound. + unfold poly__flatMTICards. reflexivity. Qed. -Lemma flatMTICards_poly : monotonic poly__flatMTICards /\ inOPoly poly__flatMTICards. +Lemma flatMTICards_poly : inOPoly poly__flatMTICards. Proof. - unfold poly__flatMTICards; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply makeAllEvalEnvFlat_poly | apply makeCardsFlat_poly | apply makeAllEvalEnvFlat_length_poly]. + unfold poly__flatMTICards; smpl_inO. + - apply makeAllEvalEnvFlat_poly. + - apply inOPoly_comp; [ solve_proper | exact makeCardsFlat_poly | ]. + smpl_inO. apply makeAllEvalEnvFlat_length_poly. Qed. +#[export] Instance flatMTICards_mono: Proper (le ==> le) poly__flatMTICards. +Proof. unfold poly__flatMTICards. solve_proper. Qed. Definition c__flatMTLCards := 22. Definition flatMTLCards_time (tm : flatTM) := makeAllEvalEnvFlat_time tm 1 4 0 0 + makeCardsFlat_time tm (makeAllEvalEnvFlat tm 1 4 0 0) mtlRules + c__flatMTLCards. @@ -1255,20 +1273,25 @@ Qed. Definition poly__flatMTLCards n := poly__makeAllEvalEnvFlat 1 4 0 0 n + poly__makeCardsFlat (n + 4 + poly__makeAllEvalEnvFlatLength 1 4 0 0 n + |mtlRules|) + c__flatMTLCards. Lemma flatMTLCards_time_bound tm : flatMTLCards_time tm <= poly__flatMTLCards (size (enc tm)). -Proof. - unfold flatMTLCards_time. +Proof. + unfold flatMTLCards_time. rewrite makeAllEvalEnvFlat_time_bound. rewrite makeCardsFlat_time_bound. 2: apply makeAllEvalEnvFlat_envBounded. cbn [max]. - poly_mono makeCardsFlat_poly. - 2: { rewrite makeAllEvalEnvFlat_length_bound. reflexivity. } - unfold poly__flatMTLCards. nia. + rewrite makeAllEvalEnvFlat_length_bound. + unfold poly__flatMTLCards. reflexivity. Qed. -Lemma flatMTLCards_poly : monotonic poly__flatMTLCards /\ inOPoly poly__flatMTLCards. +Lemma flatMTLCards_poly : inOPoly poly__flatMTLCards. Proof. - unfold poly__flatMTLCards; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply makeAllEvalEnvFlat_poly | apply makeCardsFlat_poly | apply makeAllEvalEnvFlat_length_poly]. + unfold poly__flatMTLCards; smpl_inO. + - apply makeAllEvalEnvFlat_poly. + - apply inOPoly_comp. + + solve_proper. + + exact makeCardsFlat_poly. + + smpl_inO. apply makeAllEvalEnvFlat_length_poly. Qed. +#[export] Instance flatMTLCards_mono: Proper (le ==> le) poly__flatMTLCards. +Proof. unfold poly__flatMTLCards. solve_proper. Qed. Definition c__flatTapeCards := 2 * c__app + 11. Definition flatTapeCards_time (tm : flatTM) := flatMTRCards_time tm + flatMTICards_time tm + flatMTLCards_time tm + (|flatMTICards tm| + |flatMTRCards tm| + 1) * c__flatTapeCards. @@ -1289,11 +1312,13 @@ Proof. rewrite !makeAllEvalEnvFlat_length_bound. unfold poly__flatTapeCards; nia. Qed. -Lemma flatTapeCards_poly : monotonic poly__flatTapeCards /\ inOPoly poly__flatTapeCards. +Lemma flatTapeCards_poly : inOPoly poly__flatTapeCards. Proof. - unfold poly__flatTapeCards; split; smpl_inO. - all: first [apply flatMTRCards_poly | apply flatMTLCards_poly | apply flatMTICards_poly | apply makeAllEvalEnvFlat_length_poly]. + unfold poly__flatTapeCards; smpl_inO. + all: first [apply flatMTRCards_poly | apply flatMTLCards_poly | apply flatMTICards_poly | apply makeAllEvalEnvFlat_length_poly]. Qed. +#[export] Instance flatTapeCards_mono: Proper (le ==> le) poly__flatTapeCards. +Proof. unfold poly__flatTapeCards. solve_proper. Qed. Definition poly__flatTapeCardsLength n := poly__makeAllEvalEnvFlatLength 1 4 0 0 n * (| mtrRules |) + @@ -1307,9 +1332,9 @@ Proof. rewrite !makeAllEvalEnvFlat_length_bound. unfold poly__flatTapeCardsLength. nia. Qed. -Lemma flatTapeCards_length_poly : monotonic poly__flatTapeCardsLength /\ inOPoly poly__flatTapeCardsLength. +Lemma flatTapeCards_length_poly : inOPoly poly__flatTapeCardsLength. Proof. - unfold poly__flatTapeCardsLength; split; smpl_inO. + unfold poly__flatTapeCardsLength; smpl_inO. all: apply makeAllEvalEnvFlat_length_poly. Qed. @@ -1367,12 +1392,13 @@ Proof. replace (size (enc tm) + S (S n) + (|envs|) + (|cards|)) with (size (enc tm) + (|cards|) + (|envs|) + n + 2) by lia. unfold poly__makeSomeBaseFlat. nia. Qed. -Lemma makeSome_base_flat_poly : monotonic poly__makeSomeBaseFlat /\ inOPoly poly__makeSomeBaseFlat. +Lemma makeSome_base_flat_poly : inOPoly poly__makeSomeBaseFlat. Proof. - unfold poly__makeSomeBaseFlat; split; smpl_inO. - - apply makeCardsFlat_poly. - - apply inOPoly_comp; smpl_inO; apply makeCardsFlat_poly. + unfold poly__makeSomeBaseFlat; smpl_inO. + apply inOPoly_comp; [solve_proper | apply makeCardsFlat_poly | smpl_inO]. Qed. +#[export] Instance makeSome_base_flat_mono: Proper (le ==> le) poly__makeSomeBaseFlat. +Proof. unfold poly__makeSomeBaseFlat. solve_proper. Qed. (** makeSomeRight *) Definition makeSomeRightFlat tm q q' m m' := makeSomeRight q q' m m' (makeCardsFlat tm). @@ -1454,12 +1480,13 @@ Proof. replace (size (enc tm) + S (S n) + (|envs|) + (|rules|)) with (size (enc tm) + (|rules|) + (|envs|) + n + 2) by lia. unfold poly__makeNoneBaseFlat. nia. Qed. -Lemma makeNone_base_flat_poly : monotonic poly__makeNoneBaseFlat /\ inOPoly poly__makeNoneBaseFlat. +Lemma makeNone_base_flat_poly : inOPoly poly__makeNoneBaseFlat. Proof. - unfold poly__makeNoneBaseFlat; split; smpl_inO. - - apply makeCardsFlat_poly. - - apply inOPoly_comp; smpl_inO; apply makeCardsFlat_poly. -Qed. + unfold poly__makeNoneBaseFlat; smpl_inO. + apply inOPoly_comp; [solve_proper | apply makeCardsFlat_poly | smpl_inO]. +Qed. +#[export] Instance makeNone_base_flat_mono: Proper (le ==> le) poly__makeNoneBaseFlat. +Proof. unfold poly__makeNoneBaseFlat. solve_proper. Qed. (** makeNoneRight *) Definition makeNoneRightFlat tm q q' := makeNoneRight q q' (makeCardsFlat tm). @@ -1558,7 +1585,7 @@ Proof. | None, (q', (None, TM.Nmove)) => makeNoneStayFlat tm q q' (flat_baseEnvNone tm) end). 1: { unfold makeSomeLeftFlat, makeSomeStayFlat, makeSomeRightFlat, makeNoneLeftFlat, makeNoneStayFlat, makeNoneRightFlat. easy. } - extract. + extract. (* timing 384.33 secs *) recRel_prettify2. all: unfold opt_generateCardsForFlatNonHalt_time, c__optGenerateCardsForFlatNonHalt. all: unfold optReturn; lia. @@ -1588,27 +1615,32 @@ Lemma opt_generateCardsForFlatNonHalt_time_bound tm q m act: -> opt_generateCardsForFlatNonHalt_time tm q m act <= poly__optGenerateCardsForFlatNonHalt (size (enc tm)). Proof. intros H1 H2 H3. unfold isValidFlatStateSig, isValidFlatAct in *. - unfold opt_generateCardsForFlatNonHalt_time. - destruct m as [m | ], act as (q' & [m' | ] & []). + unfold opt_generateCardsForFlatNonHalt_time. + destruct m as [m | ], act as (q' & [m' | ] & []). 10-12: rewrite makeNone_base_flat_time_bound; [ | unfold flat_baseEnvNone; apply makeAllEvalEnvFlat_envBounded | easy | easy]; - cbn [max]; unfold flat_baseEnvNone; - poly_mono makeNone_base_flat_poly; + cbn [max]; unfold flat_baseEnvNone; + erewrite makeNone_base_flat_mono; [ | rewrite makeAllEvalEnvFlat_length_bound; instantiate (1 := size (enc tm) + c__genNone + poly__makeAllEvalEnvFlatLength 2 2 2 0 (size (enc tm)) + 2); unfold c__genNone; lia]; rewrite !makeAllEvalEnvFlat_time_bound; unfold poly__optGenerateCardsForFlatNonHalt; lia. 1-9: rewrite makeSome_base_flat_time_bound; [ | unfold flat_baseEnv; apply makeAllEvalEnvFlat_envBounded | easy | easy | now finRepr_simpl| now finRepr_simpl ]; cbn [max]; unfold flat_baseEnv; - poly_mono makeSome_base_flat_poly; + erewrite makeSome_base_flat_mono; [ | rewrite makeAllEvalEnvFlat_length_bound; instantiate (1 := (size (enc tm) + c__genSome + poly__makeAllEvalEnvFlatLength 1 0 3 0 (size (enc tm)) + 3)); unfold c__genSome; lia]; rewrite !makeAllEvalEnvFlat_time_bound; unfold poly__optGenerateCardsForFlatNonHalt; lia. Qed. -Lemma opt_generateCardsForFlatNonHalt_poly : monotonic poly__optGenerateCardsForFlatNonHalt /\ inOPoly poly__optGenerateCardsForFlatNonHalt. +Lemma opt_generateCardsForFlatNonHalt_poly : inOPoly poly__optGenerateCardsForFlatNonHalt. Proof. - unfold poly__optGenerateCardsForFlatNonHalt; split; smpl_inO; try apply inOPoly_comp; smpl_inO; - first [apply makeSome_base_flat_poly | apply makeNone_base_flat_poly | apply makeAllEvalEnvFlat_length_poly | apply makeAllEvalEnvFlat_poly]. + unfold poly__optGenerateCardsForFlatNonHalt; smpl_inO. + - apply inOPoly_comp; [solve_proper | apply makeSome_base_flat_poly | ]. + smpl_inO. apply makeAllEvalEnvFlat_length_poly. + - apply inOPoly_comp; [solve_proper | apply makeNone_base_flat_poly | ]. + smpl_inO. apply makeAllEvalEnvFlat_length_poly. + - apply makeAllEvalEnvFlat_poly. + - apply makeAllEvalEnvFlat_poly. Qed. Lemma opt_generateCardsForFlatNonHalt_ofFlatType tm q m act: @@ -1628,9 +1660,7 @@ Qed. Import LProd List.List_eqb LOptions LNat. From Complexity Require Import CompCode. Lemma eqbComp_inp : EqBool.eqbCompT (nat * list (option nat)). -Proof. - easy. -Qed. +Proof. easy. Qed. (** generateCardsForFlatNonHalt *) @@ -1671,7 +1701,7 @@ Proof. all: unfold generateCardsForFlatNonHalt_time, c__generateCardsForFlatNonHalt; rewrite H; solverec. Qed. -Definition poly__generateCardsForFlatNonHalt n := +Definition poly__generateCardsForFlatNonHalt n := poly__optGenerateCardsForFlatNonHalt n + n * ((2 * n + 5 + c__listsizeCons + c__listsizeNil + 4) * c__eqbComp (nat * list (option nat)) + 24) + 4 + c__generateCardsForFlatNonHalt. Lemma generateCardsForFlatNonHalt_time_bound tm q m : validFlatTM tm -> ofFlatType (states tm) q -> isValidFlatStateSig tm m @@ -1705,10 +1735,12 @@ Proof. } all: unfold poly__generateCardsForFlatNonHalt; nia. Qed. -Lemma generateCardsForFlatNonHalt_poly : monotonic poly__generateCardsForFlatNonHalt /\ inOPoly poly__generateCardsForFlatNonHalt. +Lemma generateCardsForFlatNonHalt_poly : inOPoly poly__generateCardsForFlatNonHalt. Proof. - unfold poly__generateCardsForFlatNonHalt; split; smpl_inO; apply opt_generateCardsForFlatNonHalt_poly. + unfold poly__generateCardsForFlatNonHalt; smpl_inO; apply opt_generateCardsForFlatNonHalt_poly. Qed. +#[export] Instance generateCardsForFlatNonHalt_mono: Proper (le ==> le) poly__generateCardsForFlatNonHalt. +Proof. unfold poly__generateCardsForFlatNonHalt, poly__optGenerateCardsForFlatNonHalt. solve_proper. Qed. Lemma flat_baseEnv_length tm : |flat_baseEnv tm| <= poly__makeAllEvalEnvFlatLength 1 0 3 0 (size (enc tm)). Proof. @@ -1734,11 +1766,13 @@ Proof. 1-3: unfold makeNoneRight, makeNoneStay, makeNoneLeft, makeNone_base; rewrite makeCardsFlat_length_bound, map_length, flat_baseEnvNone_length; unfold poly__generateCardsForFlatNonHaltLength, c__genNone; nia. Qed. -Lemma generateCardsForFlatNonHalt_length_poly : monotonic poly__generateCardsForFlatNonHaltLength /\ inOPoly poly__generateCardsForFlatNonHaltLength. +Lemma generateCardsForFlatNonHalt_length_poly : inOPoly poly__generateCardsForFlatNonHaltLength. Proof. - unfold poly__generateCardsForFlatNonHaltLength; split; smpl_inO. + unfold poly__generateCardsForFlatNonHaltLength; smpl_inO. all: apply makeAllEvalEnvFlat_length_poly. Qed. +#[export] Instance generateCardsForFlatNonHalt_length_mono: Proper (le ==> le) poly__generateCardsForFlatNonHaltLength. +Proof. unfold poly__generateCardsForFlatNonHaltLength. solve_proper. Qed. Lemma generateCardsForFlatNonHalt_ofFlatType tm q m: validFlatTM tm -> ofFlatType (states tm) q -> isValidFlatStateSig tm m @@ -1783,17 +1817,17 @@ Proof. intros H H1. unfold makeHaltFlat_time. rewrite makeCardsFlat_time_bound. 2: { intros e (e' & <- & H2)%in_map_iff. apply envAddState_envBounded; eauto. } - rewrite map_length. - poly_mono makeCardsFlat_poly. - 2: { replace_le (size (enc tm) + S n + (|envs|) + (|makeHalt_rules|)) with (size (enc tm) + n + (|envs|) + ((|makeHalt_rules|) + 1)) by lia. reflexivity. } + rewrite map_length. + replace_le (size (enc tm) + S n + (|envs|) + (|makeHalt_rules|)) with (size (enc tm) + n + (|envs|) + ((|makeHalt_rules|) + 1)) by lia. unfold poly__makeHaltFlat. leq_crossout. Qed. -Lemma makeHaltFlat_poly : monotonic poly__makeHaltFlat /\ inOPoly poly__makeHaltFlat. +Lemma makeHaltFlat_poly : inOPoly poly__makeHaltFlat. Proof. - unfold poly__makeHaltFlat; split; smpl_inO. - - apply makeCardsFlat_poly. - - apply inOPoly_comp; smpl_inO; apply makeCardsFlat_poly. + unfold poly__makeHaltFlat; smpl_inO. + apply inOPoly_comp; [solve_proper | exact makeCardsFlat_poly | smpl_inO]. Qed. +#[export] Instance makeHaltFlat_mono: Proper (le ==> le) poly__makeHaltFlat. +Proof. unfold poly__makeHaltFlat. solve_proper. Qed. (** generateCardsForFlatHalt *) Definition generateCardsForFlatHalt_time tm q := makeAllEvalEnvFlat_time tm 1 0 3 0 + c__flatBaseEnv + makeHaltFlat_time tm q (flat_baseEnv tm) + 3. @@ -1816,15 +1850,18 @@ Proof. 3: apply H. 2: { unfold flat_baseEnv. apply makeAllEvalEnvFlat_envBounded. } cbn [max]. - poly_mono makeHaltFlat_poly. - 2: { unfold flat_baseEnv. rewrite makeAllEvalEnvFlat_length_bound. reflexivity. } + unfold flat_baseEnv. rewrite makeAllEvalEnvFlat_length_bound. unfold poly__generateCardsForFlatHalt. nia. Qed. -Lemma generateCardsForFlatHalt_poly : monotonic poly__generateCardsForFlatHalt /\ inOPoly poly__generateCardsForFlatHalt. +Lemma generateCardsForFlatHalt_poly : inOPoly poly__generateCardsForFlatHalt. Proof. - unfold poly__generateCardsForFlatHalt; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply makeAllEvalEnvFlat_poly | apply makeHaltFlat_poly | apply makeAllEvalEnvFlat_length_poly]. + unfold poly__generateCardsForFlatHalt; smpl_inO. + - apply makeAllEvalEnvFlat_poly. + - apply inOPoly_comp; [solve_proper | exact makeHaltFlat_poly | smpl_inO]. + apply makeAllEvalEnvFlat_length_poly. Qed. +#[export] Instance generateCardsForFlatHalt_mono: Proper (le ==> le) poly__generateCardsForFlatHalt. +Proof. unfold poly__generateCardsForFlatHalt. solve_proper. Qed. Lemma generateCardsForFlatHalt_length tm q: |generateCardsForFlatHalt tm q| <= poly__makeAllEvalEnvFlatLength 1 0 3 0 (size (enc tm)) * (| makeHalt_rules |). Proof. @@ -1909,11 +1946,13 @@ Proof. unfold ofFlatType in H. rewrite H, states_TM_le. unfold poly__generateCardsForFlat. nia. Qed. -Lemma generateCardsForFlat_poly : inOPoly poly__generateCardsForFlat /\ monotonic poly__generateCardsForFlat. +Lemma generateCardsForFlat_poly : inOPoly poly__generateCardsForFlat. Proof. - unfold poly__generateCardsForFlat; split; smpl_inO. + unfold poly__generateCardsForFlat; smpl_inO. all: first [apply generateCardsForFlatHalt_poly | apply generateCardsForFlatNonHalt_poly | apply generateCardsForFlatNonHalt_length_poly ]. -Qed. +Qed. +#[export] Instance generateCardsForFlat_mono: Proper (le ==> le) poly__generateCardsForFlat. +Proof. unfold poly__generateCardsForFlat. solve_proper. Qed. Definition poly__generateCardsForFlatLength n := poly__makeAllEvalEnvFlatLength 1 0 3 0 n * (|makeHalt_rules|) + poly__generateCardsForFlatNonHaltLength n * (n + 1). @@ -1928,15 +1967,17 @@ Proof. rewrite sig_TM_le. unfold poly__generateCardsForFlatLength; nia. Qed. -Lemma generateCardsForFlat_length_poly : monotonic poly__generateCardsForFlatLength /\ inOPoly poly__generateCardsForFlatLength. +Lemma generateCardsForFlat_length_poly : inOPoly poly__generateCardsForFlatLength. Proof. - unfold poly__generateCardsForFlatLength; split; smpl_inO. + unfold poly__generateCardsForFlatLength; smpl_inO. all: first [apply makeAllEvalEnvFlat_length_poly | apply generateCardsForFlatNonHalt_length_poly ]. -Qed. +Qed. +#[export] Instance generateCardsForFlat_length_mono: Proper (le ==> le) poly__generateCardsForFlatLength. +Proof. unfold poly__generateCardsForFlatLength. solve_proper. Qed. (**flatStateCards *) Definition c__flatStateCards := 17. -Definition flatStateCards_time (tm : flatTM) := seq_time (states tm) + map_time (fun q => generateCardsForFlat_time tm q) (seq 0 (states tm)) + concat_time (map (generateCardsForFlat tm) (seq 0 (states tm))) + c__flatStateCards. +Definition flatStateCards_time (tm : flatTM) := seq_time (states tm) + map_time (fun q => generateCardsForFlat_time tm q) (seq 0 (states tm)) + concat_time (map (generateCardsForFlat tm) (seq 0 (states tm))) + c__flatStateCards. #[export] Instance term_flatStateCards : computableTime' flatStateCards (fun tm _ => (flatStateCards_time tm, tt)). Proof. @@ -1958,11 +1999,13 @@ Proof. rewrite map_length, seq_length, states_TM_le. unfold poly__flatStateCards. nia. Qed. -Lemma flatStateCards_poly : inOPoly poly__flatStateCards /\ monotonic poly__flatStateCards. +Lemma flatStateCards_poly : inOPoly poly__flatStateCards. Proof. - unfold poly__flatStateCards; split; smpl_inO. + unfold poly__flatStateCards; smpl_inO. all: first [apply generateCardsForFlat_poly | apply generateCardsForFlat_length_poly]. Qed. +#[export] Instance flatStateCards_mono: Proper (le ==> le) poly__flatStateCards. +Proof. unfold poly__flatStateCards. solve_proper. Qed. Lemma flatStateCards_length tm : |flatStateCards tm| <= states tm * poly__generateCardsForFlatLength (size (enc tm)). Proof. @@ -2006,14 +2049,16 @@ Proof. rewrite makeCardsFlat_time_bound. 2: { intros e (e' & <- & H1)%in_map_iff. eapply envAddState_envBounded; easy. } rewrite map_length. - poly_mono makeCardsFlat_poly. - 2: { replace_le (size (enc tm) + S n + (|envs|) + (|listPreludeRules|)) with (size (enc tm) + n + (|envs|) + (|listPreludeRules|) + 1) by lia. reflexivity. } + replace_le (size (enc tm) + S n + (|envs|) + (|listPreludeRules|)) with (size (enc tm) + n + (|envs|) + (|listPreludeRules|) + 1) by lia. unfold poly__makePreludeCardsFlat. nia. Qed. -Lemma makePreludeCards_flat_poly : monotonic poly__makePreludeCardsFlat /\ inOPoly poly__makePreludeCardsFlat. +Lemma makePreludeCards_flat_poly : inOPoly poly__makePreludeCardsFlat. Proof. - unfold poly__makePreludeCardsFlat; split; smpl_inO; try apply inOPoly_comp; smpl_inO; apply makeCardsFlat_poly. + unfold poly__makePreludeCardsFlat; smpl_inO. + apply inOPoly_comp; [solve_proper | exact makeCardsFlat_poly | smpl_inO]. Qed. +#[export] Instance makePreludeCards_flat_mono: Proper (le ==> le) poly__makePreludeCardsFlat. +Proof. unfold poly__makePreludeCardsFlat. solve_proper. Qed. (** flat_baseEnvPrelude *) Definition c__flatBaseEnvPrelude := 17. @@ -2048,14 +2093,15 @@ Proof. 3: { intros e. unfold flat_baseEnvPrelude. apply makeAllEvalEnvFlat_envBounded. } 2: { destruct H. easy. } rewrite makeAllEvalEnvFlat_time_bound. cbn[max]. - poly_mono makePreludeCards_flat_poly. - 2: { rewrite flat_baseEnvPrelude_length. reflexivity. } + rewrite flat_baseEnvPrelude_length. unfold poly__flatPreludeCards. nia. Qed. -Lemma flatPreludeCards_poly : monotonic poly__flatPreludeCards /\ inOPoly poly__flatPreludeCards. +Lemma flatPreludeCards_poly : inOPoly poly__flatPreludeCards. Proof. - unfold poly__flatPreludeCards; split; smpl_inO; try apply inOPoly_comp; smpl_inO. - all: first [apply makeAllEvalEnvFlat_poly | apply makePreludeCards_flat_poly | apply makeAllEvalEnvFlat_length_poly]. + unfold poly__flatPreludeCards; smpl_inO. + - apply makeAllEvalEnvFlat_poly. + - apply inOPoly_comp; [solve_proper | exact makePreludeCards_flat_poly | smpl_inO]. + apply makeAllEvalEnvFlat_length_poly. Qed. Lemma flatPreludeCards_length tm : |flatPreludeCards tm| <= poly__makeAllEvalEnvFlatLength 0 3 1 0 (size (enc tm)) * (|listPreludeRules|). @@ -2098,11 +2144,13 @@ Proof. rewrite flatPreludeCards_length. unfold poly__allFlatCards. lia. Qed. -Lemma allFlatCards_poly : monotonic poly__allFlatCards /\ inOPoly poly__allFlatCards. +Lemma allFlatCards_poly : inOPoly poly__allFlatCards. Proof. - unfold poly__allFlatCards; split; smpl_inO. - all: first [apply flatPreludeCards_poly | apply flatTapeCards_poly | apply flatStateCards_poly | apply flatTapeCards_length_poly | apply makeAllEvalEnvFlat_length_poly ]. + unfold poly__allFlatCards. + smpl_inO; [apply flatPreludeCards_poly | apply flatTapeCards_poly | apply flatStateCards_poly | apply flatTapeCards_length_poly | apply makeAllEvalEnvFlat_length_poly ]. Qed. +#[export] Instance allFlatCards_mono: Proper (le ==> le) poly__allFlatCards. +Proof. unfold poly__allFlatCards, poly__flatPreludeCards, poly__flatTapeCardsLength. solve_proper. Qed. Definition poly__allFlatCardsLength n := poly__makeAllEvalEnvFlatLength 0 3 1 0 n * (|listPreludeRules|) + poly__flatTapeCardsLength n + n * poly__generateCardsForFlatLength n. Lemma allFlatCards_length tm : |allFlatCards tm| <= poly__allFlatCardsLength (size (enc tm)). @@ -2112,13 +2160,15 @@ Proof. unfold allFlatSimCards. rewrite app_length. rewrite flatTapeCards_length, flatStateCards_length. rewrite states_TM_le. - unfold poly__allFlatCardsLength. nia. + unfold poly__allFlatCardsLength. nia. Qed. -Lemma allFlatCards_length_poly : monotonic poly__allFlatCardsLength /\ inOPoly poly__allFlatCardsLength. +Lemma allFlatCards_length_poly : inOPoly poly__allFlatCardsLength. Proof. - unfold poly__allFlatCardsLength; split; smpl_inO. + unfold poly__allFlatCardsLength; smpl_inO. all: first [apply makeAllEvalEnvFlat_length_poly | apply flatTapeCards_length_poly | apply generateCardsForFlat_length_poly]. Qed. +#[export] Instance allFlatCards_length_mono: Proper (le ==> le) poly__allFlatCardsLength. +Proof. unfold poly__allFlatCardsLength, poly__flatTapeCardsLength. solve_proper. Qed. Lemma allFlatCards_ofFlatType tm : validFlatTM tm -> isValidFlatCards (allFlatCards tm) (flatAlphabet tm). Proof. @@ -2146,9 +2196,9 @@ Proof. rewrite size_nat_enc with (n := flatAlphabet tm). rewrite flatAlphabet_bound, sig_TM_le, states_TM_le. unfold poly__allFlatCardsSize; reflexivity. Qed. -Lemma allFlatCards_size_poly : monotonic poly__allFlatCardsSize /\ inOPoly poly__allFlatCardsSize. +Lemma allFlatCards_size_poly : inOPoly poly__allFlatCardsSize. Proof. - unfold poly__allFlatCardsSize; split; smpl_inO; apply allFlatCards_length_poly. + unfold poly__allFlatCardsSize; smpl_inO; apply allFlatCards_length_poly. Qed. (** repeat *) @@ -2180,10 +2230,10 @@ Proof. unfold add_time. rewrite size_nat_enc_r with (n := k') at 1. unfold poly__kflat. leq_crossout. Qed. -Lemma kflat_poly : monotonic poly__kflat /\ inOPoly poly__kflat. -Proof. - unfold poly__kflat; split; smpl_inO. -Qed. +Lemma kflat_poly : inOPoly poly__kflat. +Proof. unfold poly__kflat; smpl_inO. Qed. +#[export] Instance kflat_mono: Proper (le ==> le) poly__kflat. +Proof. unfold poly__kflat. solve_proper. Qed. (** zflat *) Definition c__zflat := c__add1 + 2. @@ -2199,13 +2249,13 @@ Definition poly__zflat n := poly__kflat n + (n + 1) * c__add + c__zflat. Lemma zflat_time_bound t k' fixed : zflat_time t k' fixed <= poly__zflat (size (enc t) + size (enc k') + size (enc fixed)). Proof. unfold zflat_time. rewrite kflat_time_bound. - poly_mono kflat_poly. 2: { replace_le (size (enc k') + size (enc fixed)) with (size (enc t) + size (enc k') + size (enc fixed)) by lia. reflexivity. } + replace_le (size (enc k') + size (enc fixed)) with (size (enc t) + size (enc k') + size (enc fixed)) by lia. unfold add_time. rewrite size_nat_enc_r with (n := t) at 2. unfold poly__zflat. leq_crossout. Qed. -Lemma zflat_poly : monotonic poly__zflat /\ inOPoly poly__zflat. +Lemma zflat_poly : inOPoly poly__zflat. Proof. - unfold poly__zflat; split; smpl_inO; apply kflat_poly. + unfold poly__zflat; smpl_inO; apply kflat_poly. Qed. (** zPflat *) @@ -2224,10 +2274,10 @@ Proof. unfold zPflat_time. rewrite zflat_time_bound. unfold poly__zPflat; lia. Qed. -Lemma zPflat_poly : monotonic poly__zPflat /\ inOPoly poly__zPflat. -Proof. - unfold poly__zPflat; split; smpl_inO; apply zflat_poly. -Qed. +Lemma zPflat_poly : inOPoly poly__zPflat. +Proof. unfold poly__zPflat; smpl_inO; apply zflat_poly. Qed. +#[export] Instance zPflat_mono: Proper (le ==> le) poly__zPflat. +Proof. unfold poly__zPflat, poly__zflat. solve_proper. Qed. (** flatInitialString *) (* step function for map *) @@ -2274,41 +2324,33 @@ Definition poly__flatInitialString n := c__app * n + c__app * n + (c__app + c__rev + c__repeat) * (wo + (n + (n + n))) + c__flatInitialString. Lemma flat_initial_string_time_bound t k' tm fixed : flat_initial_string_time t k' tm fixed <= poly__flatInitialString (size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). -Proof. +Proof. unfold flat_initial_string_time. - rewrite flatGamma_time_bound. rewrite zPflat_time_bound. + rewrite flatGamma_time_bound, zPflat_time_bound. unfold flatInr_flatNsig_time. rewrite map_time_const. rewrite flatGamma_time_bound. unfold zPflat, zflat, kflat. rewrite list_size_length with (l := fixed). unfold add_time. rewrite flatGamma_bound. rewrite states_TM_le, sig_TM_le. - rewrite size_nat_enc_r with (n := k') at 2 3 4. - rewrite size_nat_enc_r with (n := t) at 2 3 4. - - pose (m := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). - poly_mono flatGamma_poly. 2: { instantiate (1 := m). subst m. lia. } - replace_le (size (enc tm)) with m by (subst m; lia) at 1. - replace_le (size (enc tm)) with m by (subst m; lia) at 1. - replace_le (size (enc tm)) with m by (subst m; lia) at 1. - replace_le (size (enc tm)) with m by (subst m; lia) at 1. - poly_mono zPflat_poly. 2: {instantiate (1 := m). subst m; lia. } - replace_le (size (enc k')) with m by (subst m; lia) at 1. - replace_le (size (enc k')) with m by (subst m; lia) at 1. - replace_le (size (enc k')) with m by (subst m; lia) at 1. - replace_le (size (enc t)) with m by (subst m; lia) at 1. - replace_le (size (enc t)) with m by (subst m; lia) at 1. - replace_le (size (enc t)) with m by (subst m; lia) at 1. - replace_le (size (enc fixed)) with m by (subst m; lia) at 1. - replace_le (size (enc fixed)) with m by (subst m; lia) at 1. - replace_le (size (enc fixed)) with m by (subst m; lia) at 1. - fold m. generalize m. intros m'. - unfold poly__flatInitialString. reflexivity. -Qed. -Lemma flat_initial_string_poly : monotonic poly__flatInitialString /\ inOPoly poly__flatInitialString. -Proof. - unfold poly__flatInitialString; split; smpl_inO; first [apply flatGamma_poly | apply zPflat_poly]. -Qed. + rewrite size_nat_enc_r with (n := k') at 2 3 4. + rewrite size_nat_enc_r with (n := t) at 2 3 4. + + pose (m := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). + setoid_replace (size (enc tm)) with m using relation le at 1 2 3 4 5 6 by lia. + setoid_replace (size (enc t) + size (enc k') + size (enc fixed)) with m + using relation le at 1 by lia. + setoid_replace (size (enc k')) with m using relation le at 1 2 3 by lia. + setoid_replace (size (enc t)) with m using relation le at 1 2 3 by lia. + setoid_replace (size (enc fixed)) with m using relation le at 1 2 3 by lia. + reflexivity. +Qed. +Lemma flat_initial_string_poly : inOPoly poly__flatInitialString. +Proof. + unfold poly__flatInitialString; smpl_inO; first [apply flatGamma_poly | apply zPflat_poly]. +Qed. +#[export] Instance flat_initial_string_mono: Proper (le ==> le) poly__flatInitialString. +Proof. unfold poly__flatInitialString. solve_proper. Qed. Lemma flat_initial_string_length t k' tm fixed: |flat_initial_string t k' tm fixed| = 2 * (zPflat t k' fixed + 1) + 1. Proof. @@ -2347,7 +2389,8 @@ Definition poly__flatInitialStringSize n := (c__flatAlphabetS * c__natsizeS * Lemma flat_initial_string_size_bound t k' tm fixed: list_ofFlatType (sig tm) fixed -> size (enc (flat_initial_string t k' tm fixed)) <= poly__flatInitialStringSize (size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). Proof. intros H. rewrite list_size_of_el. - 2: { intros a H1%flat_initial_string_ofFlatType. 2: apply H. rewrite nat_size_lt by apply H1. + 2: { intros a H1%flat_initial_string_ofFlatType%Nat.lt_le_incl; [|apply H]. + rewrite nat_size_le. 2: exact H1. rewrite nat_size_le. 2: { rewrite flatAlphabet_bound. reflexivity. } reflexivity. @@ -2359,15 +2402,12 @@ Proof. pose (g := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). replace_le (size (enc tm)) with g by (subst g; lia) at 1. replace_le (size (enc tm)) with g by (subst g; lia) at 1. - replace_le (size (enc t) + (size (enc k') + size (enc fixed))) with g by (subst g; lia) at 1. - replace_le (size (enc t) + (size (enc k') + size (enc fixed))) with g by (subst g; lia) at 1. + replace_le (size (enc t) + (size (enc k') + size (enc fixed))) with g by (subst g; lia) at 1 2. fold g. unfold poly__flatInitialStringSize. nia. Qed. -Lemma flat_initial_string_size_poly : monotonic poly__flatInitialStringSize /\ inOPoly poly__flatInitialStringSize. -Proof. - unfold poly__flatInitialStringSize; split; smpl_inO. -Qed. +Lemma flat_initial_string_size_poly : inOPoly poly__flatInitialStringSize. +Proof. unfold poly__flatInitialStringSize; smpl_inO. Qed. Section fixX. Variable (X : Type). @@ -2411,7 +2451,7 @@ Instance term_flat_haltingStates : computableTime' flat_haltingStates (fun tm _ Proof. unfold flat_haltingStates. apply computableTimeExt with (x :=fun tm => filter (isHalting tm) (seq 0 (states tm))). - { easy. } + { reflexivity. } extract. solverec. unfold flat_haltingStates_time, c__flatHaltingStates. solverec. Qed. @@ -2426,11 +2466,12 @@ Proof. rewrite states_TM_le at 1 2. unfold poly__flatHaltingStates. nia. Qed. -Lemma flat_haltingStates_poly : monotonic poly__flatHaltingStates /\ inOPoly poly__flatHaltingStates. -Proof. - unfold poly__flatHaltingStates; split; smpl_inO. -Qed. +Lemma flat_haltingStates_poly : inOPoly poly__flatHaltingStates. +Proof. unfold poly__flatHaltingStates; smpl_inO. Qed. +#[export] Instance flat_haltingStates_mono: Proper (le ==> le) poly__flatHaltingStates. +Proof. unfold poly__flatHaltingStates. solve_proper. Qed. +(* TODO: use stdlib when https://github.com/coq/coq/pull/17027 gets merged *) Lemma filter_length (X : Type) (p : X -> bool) (l : list X) : |filter p l| <= |l|. Proof. induction l; cbn; [lia | destruct p; cbn; lia]. @@ -2465,10 +2506,10 @@ Proof. unfold flatPair_time, mult_time, add_time. rewrite flatStateSigma_bound, H. rewrite states_TM_le, sig_TM_le. unfold poly__flatFinalSubstringsStep; solverec. Qed. -Lemma flat_finalSubstrings_step_poly : monotonic poly__flatFinalSubstringsStep /\ inOPoly poly__flatFinalSubstringsStep. -Proof. - unfold poly__flatFinalSubstringsStep; split; smpl_inO. -Qed. +Lemma flat_finalSubstrings_step_poly : inOPoly poly__flatFinalSubstringsStep. +Proof. unfold poly__flatFinalSubstringsStep; smpl_inO. Qed. +#[export] Instance flat_finalSubstrings_steps_mono: Proper (le ==> le) poly__flatFinalSubstringsStep. +Proof. unfold poly__flatFinalSubstringsStep. solve_proper. Qed. Definition c__finalSubstrings := c__flatStateSigma + 13. Definition flat_finalSubstrings_time (tm : flatTM) := flat_haltingStates_time tm + seq_time (flatStateSigma tm) + prodLists_time (flat_haltingStates tm) (seq 0 (flatStateSigma tm)) + map_time (flat_finalSubstrings_step_time tm) (list_prod (flat_haltingStates tm) (seq 0 (flatStateSigma tm))) + c__finalSubstrings. @@ -2477,7 +2518,7 @@ Instance term_flat_finalSubstrings : computableTime' flat_finalSubstrings (fun t Proof. apply computableTimeExt with (x := fun tm => map (flat_finalSubstrings_step tm) (list_prod (flat_haltingStates tm) (seq 0 (flatStateSigma tm)))). - { easy. } + { reflexivity. } extract. recRel_prettify2. unfold flat_finalSubstrings_time, c__finalSubstrings; simp_comp_arith; solverec. Qed. @@ -2498,10 +2539,13 @@ Proof. rewrite flatStateSigma_bound, sig_TM_le, states_TM_le. unfold poly__finalSubstrings; lia. Qed. -Lemma flat_finalSubstrings_poly : monotonic poly__finalSubstrings /\ inOPoly poly__finalSubstrings. +Lemma flat_finalSubstrings_poly : inOPoly poly__finalSubstrings. Proof. - unfold poly__finalSubstrings; split; smpl_inO; first [apply flat_haltingStates_poly | apply flat_finalSubstrings_step_poly]. + unfold poly__finalSubstrings. + smpl_inO; [apply flat_haltingStates_poly | apply flat_finalSubstrings_step_poly]. Qed. +#[export] Instance flat_finalSubstrings_mono: Proper (le ==> le) poly__finalSubstrings. +Proof. unfold poly__finalSubstrings. solve_proper. Qed. Proposition flat_finalSubstrings_length (tm : flatTM) : |flat_finalSubstrings tm| <= states tm * (S (sig tm)). Proof. @@ -2538,9 +2582,9 @@ Proof. unfold enc at 1. cbn -[Nat.add Nat.mul]. rewrite size_nat_enc, sig_TM_le, states_TM_le. unfold poly__flatFinalSubstringsSize. nia. Qed. -Lemma flat_finalSubstrings_size_poly : monotonic poly__flatFinalSubstringsSize /\ inOPoly poly__flatFinalSubstringsSize. +Lemma flat_finalSubstrings_size_poly : inOPoly poly__flatFinalSubstringsSize. Proof. - unfold poly__flatFinalSubstringsSize; split; smpl_inO. + unfold poly__flatFinalSubstringsSize; smpl_inO. Qed. (** reduction_wf *) @@ -2555,23 +2599,27 @@ Qed. Definition poly__reductionWf n := poly__flatAlphabet n + poly__flatInitialString n + poly__allFlatCards n + poly__finalSubstrings n + c__reductionWf. Lemma reduction_wf_time_bound t k' tm fixed: validFlatTM tm -> reduction_wf_time t k' tm fixed <= poly__reductionWf (size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). -Proof. +Proof. intros H. unfold reduction_wf_time. rewrite flatAlphabet_time_bound, flat_initial_string_time_bound. rewrite allFlatCards_time_bound by easy. rewrite flat_finalSubstrings_time_bound. - pose (m := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). - poly_mono flatAlphabet_poly. 2: { instantiate (1 := m). subst m;lia. } - poly_mono flat_initial_string_poly. 2: { instantiate (1 := m); subst m; lia. } - poly_mono allFlatCards_poly. 2 : { instantiate (1 := m); subst m; lia. } - poly_mono flat_finalSubstrings_poly. 2 : { instantiate (1 := m); subst m; lia. } - subst m; unfold poly__reductionWf. lia. -Qed. -Lemma reduction_wf_poly : monotonic poly__reductionWf /\ inOPoly poly__reductionWf. + set (m := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). + setoid_replace (size (enc tm)) with m using relation le at 1 2 3 by lia. + reflexivity. +Qed. +Lemma reduction_wf_poly : inOPoly poly__reductionWf. Proof. - unfold poly__reductionWf; split; smpl_inO. - all: first [apply flatAlphabet_poly | apply flat_initial_string_poly | apply allFlatCards_poly | apply flat_finalSubstrings_poly]. + unfold poly__reductionWf. + smpl_inO; [apply flatAlphabet_poly | apply flat_initial_string_poly | apply allFlatCards_poly | apply flat_finalSubstrings_poly]. Qed. +#[export] Instance reduction_wf_mono: Proper (le ==> le) poly__reductionWf. +Proof. unfold poly__reductionWf, poly__flatAlphabet. solve_proper. Qed. + +#[export] Instance allFlatCardsSize_mono: Proper (le ==> le) poly__allFlatCardsSize. +Proof. unfold poly__allFlatCardsSize. solve_proper. Qed. +#[export] Instance flatFinalSubstringsSize_mono: Proper (le ==> le) poly__flatFinalSubstringsSize. +Proof. unfold poly__flatFinalSubstringsSize. solve_proper. Qed. Definition poly__reductionWfSize n := c__flatAlphabetS * (n + 1) * (n + 1) * c__natsizeS + c__natsizeO @@ -2580,27 +2628,31 @@ Definition poly__reductionWfSize n := Lemma reduction_wf_size_bound t k' tm fixed : validFlatTM tm -> list_ofFlatType (sig tm) fixed -> size (enc (reduction_wf t k' tm fixed)) <= poly__reductionWfSize (size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). -Proof. +Proof. intros H H0. unfold reduction_wf. rewrite FlatTCC_enc_size. cbn -[allFlatCards flat_initial_string poly__reductionWfSize]. rewrite flat_initial_string_size_bound by easy. rewrite allFlatCards_size_bound by easy. rewrite flat_finalSubstrings_size_bound by easy. - pose (g := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). - poly_mono allFlatCards_size_poly. 2: { instantiate (1 := g); subst g; lia. } - poly_mono flat_finalSubstrings_size_poly. 2: { instantiate (1 := g); subst g; lia. } + set (g := size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)). + setoid_replace (size (enc tm)) with g using relation le at 1 2 by lia. rewrite size_nat_enc at 1; rewrite flatAlphabet_bound, states_TM_le, sig_TM_le at 1. replace (size (enc (S t))) with (c__natsizeS + size (enc t)). 2: { rewrite !size_nat_enc. nia. } - replace_le (size (enc tm)) with g by (subst g; lia) at 1. - replace_le (size (enc tm)) with g by (subst g; lia) at 1. - replace_le (size (enc t)) with g by (subst g; lia) at 2. + replace_le (size (enc tm)) with g by (subst g; lia) at 1 2. + replace_le (size (enc t)) with g by (subst g; lia) at 1. fold g. unfold poly__reductionWfSize; leq_crossout. Qed. -Lemma reduction_wf_size_poly : monotonic poly__reductionWfSize /\ inOPoly poly__reductionWfSize. +Lemma reduction_wf_size_poly : inOPoly poly__reductionWfSize. Proof. - unfold poly__reductionWfSize; split; smpl_inO. - all: first [apply flat_initial_string_size_poly | apply allFlatCards_size_poly | apply flat_finalSubstrings_size_poly]. + unfold poly__reductionWfSize. + smpl_inO; [apply flat_initial_string_size_poly | apply allFlatCards_size_poly | apply flat_finalSubstrings_size_poly]. +Qed. +#[export] Instance reduction_wf_size_mono: Proper (le ==> le) poly__reductionWfSize. +Proof. + unfold poly__reductionWfSize, poly__flatInitialStringSize, + poly__allFlatCardsSize, poly__flatFinalSubstringsSize. + solve_proper. Qed. (** implb *) @@ -2668,10 +2720,10 @@ Section fixIsInjFinfuncTable. unfold poly__allSameEntry. rewrite list_size_cons, size_prod; cbn -[Nat.add Nat.mul]. nia. Qed. - Lemma allSameEntry_poly : monotonic poly__allSameEntry /\ inOPoly poly__allSameEntry. - Proof. - unfold poly__allSameEntry; split; smpl_inO. - Qed. + Lemma allSameEntry_poly : inOPoly poly__allSameEntry. + Proof. unfold poly__allSameEntry; smpl_inO. Qed. + #[export] Instance allSameEntry_mono: Proper (le ==> le) poly__allSameEntry. + Proof. unfold poly__allSameEntry. solve_proper. Qed. (** isInjFinfuncTable *) Definition c__isInjFinfuncTable := 21. @@ -2692,14 +2744,15 @@ Section fixIsInjFinfuncTable. - unfold poly__isInjFinfuncTable. rewrite size_list; cbn -[Nat.add]. unfold c__listsizeNil; nia. - destruct a. rewrite IHl. rewrite allSameEntry_time_bound. - unfold poly__isInjFinfuncTable. - poly_mono allSameEntry_poly. 2: { instantiate (1 := size (enc ((x, y) :: l))). rewrite list_size_cons. nia. } + unfold poly__isInjFinfuncTable. + setoid_replace (size (enc l)) with (size (enc ((x, y) :: l))) + using relation le at 1 3 by (rewrite list_size_cons; nia). rewrite list_size_cons. unfold c__listsizeCons. leq_crossout. Qed. - Lemma isInjFinfuncTable_poly : monotonic poly__isInjFinfuncTable /\ inOPoly poly__isInjFinfuncTable. - Proof. - unfold poly__isInjFinfuncTable; split; smpl_inO; apply allSameEntry_poly. - Qed. + Lemma isInjFinfuncTable_poly : inOPoly poly__isInjFinfuncTable. + Proof. unfold poly__isInjFinfuncTable; smpl_inO; apply allSameEntry_poly. Qed. + #[export] Instance isInjFinfuncTable_mono: Proper (le ==> le) poly__isInjFinfuncTable. + Proof. unfold poly__isInjFinfuncTable. solve_proper. Qed. End fixIsInjFinfuncTable. (** isBoundTransTable *) @@ -2726,7 +2779,7 @@ Definition ltb_time (a b : nat) := leb_time (S a) b + c__ltb. Instance term_ltb : computableTime' Nat.ltb (fun a _ => (1, fun b _ => (ltb_time a b, tt))). Proof. extract. recRel_prettify2. - - lia. + - reflexivity. - unfold ltb_time, c__ltb, flatSome. solverec. Qed. @@ -2751,9 +2804,9 @@ Proof. rewrite size_nat_enc_r with (n := k) at 1. unfold poly__optBound. nia. - unfold poly__optBound. nia. Qed. -Lemma optBound_poly : monotonic poly__optBound /\ inOPoly poly__optBound. +Lemma optBound_poly : inOPoly poly__optBound. Proof. - unfold poly__optBound; split; smpl_inO. + unfold poly__optBound; smpl_inO. Qed. Definition c__fstOptBound := 7. @@ -2782,6 +2835,9 @@ Proof. rewrite size_nat_enc. unfold c__natsizeO, c__leb, c__natsizeS. nia. Qed. +#[export] Instance optBound_mono: Proper (le ==> le) poly__optBound. +Proof. unfold poly__optBound. solve_proper. Qed. + Definition poly__isBoundTrans n := n * (2 * c__leb + 2 * c__length + 2 * c__eqbComp nat + 2 * c__forallb + c__fstOptBound) + 2 * c__forallb + 2 * c__ltb + 2 * c__eqbComp nat + 2 * n * poly__optBound n + c__isBoundTrans. Lemma isBoundTrans_time_bound sig n states t : isBoundTrans_time sig n states t <= poly__isBoundTrans (size (enc t) + size (enc sig)). @@ -2796,9 +2852,9 @@ Proof. unfold forallb_time. rewrite sumn_map_mono. 2: {instantiate (1 := fun _ => _). intros x _. cbn. unfold fst_optBound_time. rewrite optBound_time_bound. reflexivity. } rewrite sumn_map_const. - rewrite !list_size_length. - poly_mono optBound_poly. - 2: { instantiate (1 := size (enc (s, v, (s', v'))) + size (enc sig)). lia. } + rewrite !list_size_length. + setoid_replace (size (enc sig)) with (size (enc (s, v, (s', v'))) + size (enc sig)) + using relation le at 1 2 by lia. replace_le (size (enc s)) with (size (enc (s, v, (s', v')))) by (rewrite !size_prod; cbn; lia ). replace_le (size (enc v)) with (size (enc (s, v, (s', v')))) by (rewrite !size_prod; cbn; lia ). @@ -2807,10 +2863,12 @@ Proof. generalize (size (enc (s, v, (s', v')))). intros n'. unfold poly__isBoundTrans. nia. Qed. -Lemma isBoundTrans_poly : monotonic poly__isBoundTrans /\ inOPoly poly__isBoundTrans. +Lemma isBoundTrans_poly : inOPoly poly__isBoundTrans. Proof. - unfold poly__isBoundTrans; split; smpl_inO; apply optBound_poly. + unfold poly__isBoundTrans; smpl_inO; apply optBound_poly. Qed. +#[export] Instance isBoundTrans_mono: Proper (le ==> le) poly__isBoundTrans. +Proof. unfold poly__isBoundTrans, poly__optBound. solve_proper. Qed. Definition c__isBoundTransTable := 5. Definition isBoundTransTable_time (sig n states : nat) (l : list (nat * list (option nat) * (nat * list (option nat * TM.move)))) := @@ -2818,8 +2876,7 @@ Definition isBoundTransTable_time (sig n states : nat) (l : list (nat * list (op #[export] Instance term_isBoundTransTable : computableTime' isBoundTransTable (fun sig _ => (1, fun n _ => (1, fun states _ => (1, fun l _ => (isBoundTransTable_time sig n states l, tt))))). Proof. - eapply computableTimeExt with (x := isBoundTransTable'). - { easy. } + eapply computableTimeExt with (x := isBoundTransTable'); [reflexivity |]. extract. solverec. unfold isBoundTransTable_time, c__isBoundTransTable; simp_comp_arith; solverec. Qed. @@ -2832,17 +2889,17 @@ Proof. - cbn -[Nat.add Nat.mul]. match goal with [ |- ?a + ?b + ?c + ?d + ?e <= _] => replace (a + b + c + d + e) with (a + b + (c + d + e)) by lia end. rewrite IHl. rewrite isBoundTrans_time_bound. - unfold poly__isBoundTransTable. - poly_mono isBoundTrans_poly. 2: { instantiate (1 := size (enc (a :: l)) + size (enc sig)). rewrite list_size_cons. lia. } - poly_mono isBoundTrans_poly at 2. 2: { instantiate (1 := size (enc (a :: l)) + size (enc sig)). rewrite list_size_cons. lia. } + unfold poly__isBoundTransTable. + setoid_replace (size (enc a) + size (enc sig)) with (size (enc (a :: l)) + size (enc sig)) + using relation le at 1 by (rewrite list_size_cons; lia). + setoid_replace (size (enc l) + size (enc sig)) with (size (enc (a :: l)) + size (enc sig)) + using relation le at 2 by (rewrite list_size_cons; lia). rewrite list_size_cons at 3 5. unfold c__listsizeCons. leq_crossout. Qed. -Lemma isBoundTransTable_poly : monotonic poly__isBoundTransTable /\ inOPoly poly__isBoundTransTable. -Proof. - unfold poly__isBoundTransTable; split; smpl_inO; apply isBoundTrans_poly. -Qed. +Lemma isBoundTransTable_poly : inOPoly poly__isBoundTransTable. +Proof. unfold poly__isBoundTransTable; smpl_inO; apply isBoundTrans_poly. Qed. (** isValidFlatTrans *) Definition c__isValidFlatTrans := 9. @@ -2862,16 +2919,15 @@ Definition poly__isValidFlatTrans n := poly__isInjFinfuncTable (X := nat * list Lemma isValidFlatTrans_time_bound sig n states l : isValidFlatTrans_time sig n states l <= poly__isValidFlatTrans (size (enc l) + size (enc sig)). Proof. unfold isValidFlatTrans_time. - rewrite isInjFinfuncTable_time_bound. - rewrite isBoundTransTable_time_bound. - poly_mono (isInjFinfuncTable_poly (X := nat * list (option nat)) (Y := nat * list (option nat * TM.move))). - 2: { instantiate (1 := size (enc l) + size (enc sig)). lia. } - unfold poly__isValidFlatTrans. lia. + rewrite isInjFinfuncTable_time_bound, isBoundTransTable_time_bound. + setoid_replace (size (enc l)) with (size (enc l) + size (enc sig)) + using relation le at 1 by lia. + unfold poly__isValidFlatTrans. reflexivity. Qed. -Lemma isValidFlatTrans_poly : monotonic poly__isValidFlatTrans /\ inOPoly poly__isValidFlatTrans. +Lemma isValidFlatTrans_poly : inOPoly poly__isValidFlatTrans. Proof. - unfold poly__isValidFlatTrans; split; smpl_inO. - all: first [apply isInjFinfuncTable_poly | apply isBoundTransTable_poly ]. + unfold poly__isValidFlatTrans. + smpl_inO; [apply isInjFinfuncTable_poly | apply isBoundTransTable_poly ]. Qed. (** isValidFlatTM *) @@ -2884,19 +2940,27 @@ Proof. unfold isValidFlatTM_time, c__isValidFlatTM. solverec. Qed. +#[export] Instance isValidFlatTrans_mono: Proper (le ==> le) poly__isValidFlatTrans. +Proof. unfold poly__isValidFlatTrans, poly__isBoundTransTable. solve_proper. Qed. + Definition poly__isValidFlatTM n := poly__isValidFlatTrans n + n * c__leb + c__ltb + c__isValidFlatTM. Lemma isValidFlatTM_time_bound tm : isValidFlatTM_time tm <= poly__isValidFlatTM (size (enc tm)). Proof. unfold isValidFlatTM_time. rewrite isValidFlatTrans_time_bound. - rewrite ltb_time_bound_l. - poly_mono isValidFlatTrans_poly. - 2: { instantiate (1 := size (enc tm)). rewrite size_TM. destruct tm. cbn. lia. } + rewrite ltb_time_bound_l. + setoid_replace (size (enc (trans tm)) + size (enc (sig tm))) with (size (enc tm)) + using relation le at 1. + 2: { rewrite size_TM. destruct tm. cbn. lia. } replace_le (size (enc (start tm))) with (size (enc tm)) by (rewrite size_TM; destruct tm; cbn ;lia). unfold poly__isValidFlatTM. lia. Qed. -Lemma isValidFlatTM_poly : monotonic poly__isValidFlatTM /\ inOPoly poly__isValidFlatTM. -Proof. - unfold poly__isValidFlatTM; split; smpl_inO; apply isValidFlatTrans_poly. +Lemma isValidFlatTM_poly : inOPoly poly__isValidFlatTM. +Proof. unfold poly__isValidFlatTM; smpl_inO; apply isValidFlatTrans_poly. Qed. +#[export] Instance isValidFlatTM_mono: Proper (le ==> le) poly__isValidFlatTM. +Proof. + unfold poly__isValidFlatTM, poly__isValidFlatTrans, poly__isInjFinfuncTable, + poly__isBoundTransTable. + solve_proper. Qed. (** reduction *) @@ -2919,19 +2983,23 @@ Lemma reduction_time_bound t k' tm fixed : reduction_time t k' tm fixed <= poly_ Proof. unfold reduction_time. rewrite isValidFlatTM_time_bound. rewrite list_ofFlatType_dec_time_bound. - pose (m := size (enc k') + size (enc t) + size (enc tm) + size (enc fixed)). - poly_mono isValidFlatTM_poly. 2: { instantiate (1 := m). subst m; lia. } - poly_mono list_ofFlatType_dec_poly. 2 : { instantiate (1 := m). subst m. rewrite size_TM; destruct tm; cbn. lia. } + pose (m := size (enc k') + size (enc t) + size (enc tm) + size (enc fixed)). + setoid_replace (size (enc tm)) with m using relation le at 1 by lia. + setoid_replace (size (enc (sig tm)) + size (enc fixed)) with m + using relation le at 1. + 2 : { unfold m. rewrite size_TM; destruct tm; cbn. lia. } destruct isValidFlatTM eqn:H1. - rewrite reduction_wf_time_bound. 2: { rewrite reflect_iff; [apply H1 | apply isValidFlatTM_spec]. } subst m. unfold poly__reduction. nia. - subst m. unfold poly__reduction. nia. Qed. -Lemma reduction_poly : monotonic poly__reduction /\ inOPoly poly__reduction. +Lemma reduction_poly : inOPoly poly__reduction. Proof. - unfold poly__reduction; split; smpl_inO. - all: first [apply isValidFlatTM_poly | apply list_ofFlatType_dec_poly | apply reduction_wf_poly]. + unfold poly__reduction. + smpl_inO; [apply isValidFlatTM_poly | apply list_ofFlatType_dec_poly | apply reduction_wf_poly]. Qed. +#[export] Instance reduction_mono: Proper (le ==> le) poly__reduction. +Proof. unfold poly__reduction. solve_proper. Qed. Definition poly__reductionSize n := poly__reductionWfSize n + size (enc trivial_no_instance). Lemma reduction_size_bound p : size (enc (reduction p)) <= poly__reductionSize (size (enc p)). @@ -2942,8 +3010,9 @@ Proof. destruct list_ofFlatType_dec eqn:H3; cbn -[poly__reductionSize]; [ | unfold poly__reductionSize; lia]. rewrite <- reflect_iff in H1; [ | apply isValidFlatTM_spec ]. apply list_ofFlatType_dec_correct in H3. rewrite reduction_wf_size_bound by easy. - poly_mono reduction_wf_size_poly. - 2: { instantiate (1 := size (enc (tm, fixed, k', t))). rewrite !size_prod. cbn. lia. } + setoid_replace (size (enc t) + size (enc k') + size (enc tm) + size (enc fixed)) + with (size (enc (tm, fixed, k', t))) using relation le + by (rewrite !size_prod; cbn; lia). unfold poly__reductionSize. lia. Qed. @@ -2955,14 +3024,15 @@ From Complexity.NP.SAT.CookLevin.Subproblems Require Import SingleTMGenNP. Theorem FlatSingleTMGenNP_to_FlatTCCLang_poly : FlatSingleTMGenNP ⪯p FlatTCCLang. Proof. apply reducesPolyMO_intro with (f := reduction). - - exists poly__reduction. + - exists poly__reduction; [|apply reduction_poly|exact reduction_mono|]. + exists (extT reduction). eapply computesTime_timeLeq. 2: apply term_reduction. cbn. intros p _. split; [ | easy]. destruct p as (((tm & fixed) & t) & k'). - rewrite reduction_time_bound. poly_mono reduction_poly; [reflexivity | rewrite !size_prod; cbn;lia]. - + apply reduction_poly. - + apply reduction_poly. - + evar (f :nat -> nat). exists f. - 1: { intros p. rewrite reduction_size_bound. [f]: intros n. subst f; reflexivity. } - all: subst f; smpl_inO; unfold poly__reductionSize; smpl_inO; apply reduction_wf_size_poly. + rewrite reduction_time_bound. + rewrite !size_prod. cbn. + apply reduction_mono. lia. + + evar (f :nat -> nat). exists f. + * intros p. rewrite reduction_size_bound. [f]: intros n. subst f; reflexivity. + * unfold f, poly__reductionSize. smpl_inO. apply reduction_wf_size_poly. + * unfold f, poly__reductionSize. solve_proper. - apply FlatSingleTMGenNP_to_FlatTCC. Qed. diff --git a/theories/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v b/theories/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v index 7dd508be..05d220c2 100644 --- a/theories/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v +++ b/theories/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v @@ -106,19 +106,15 @@ Section fixX. Proof. unfold CC_cards_time. unfold poly__CCCards, c__CCCardsBound. rewrite (map_time_bound_env (Y := unit) (X := (TCCCard X)) (fT := fun _ _ => c__TCCCardToCCCard) (f__bound := fun n => c__TCCCardToCCCard)). - 3: easy. - 2: { - split. - - intros _ _. reflexivity. - - smpl_inO. - } - rewrite list_size_length. nia. - Qed. + - rewrite list_size_length. nia. + - split; [reflexivity | apply monotonic_c]. + - constructor. + Qed. - Lemma CCCards_poly : monotonic poly__CCCards /\ inOPoly poly__CCCards. - Proof. - split; unfold poly__CCCards; smpl_inO. - Qed. + Lemma CCCards_poly : inOPoly poly__CCCards. + Proof. unfold poly__CCCards; smpl_inO. Qed. + #[export] Instance CCCards_mono: Proper (le ==> le) poly__CCCards. + Proof. unfold poly__CCCards. solve_proper. Qed. Definition CC_cards_size (w : list (TCCCard X)): size (enc (CC_cards w)) <= size (enc (w)) + (|w|) * c__TCCCardToCCCardSize. Proof. @@ -144,18 +140,19 @@ Lemma FlatTCC_to_FlatCC_poly : FlatTCCLang ⪯p FlatCCLang. Proof. apply reducesPolyMO_intro with (f := FCC_instance). - exists (fun n => c__FCC_instance + poly__CCCards n). - + extract. solverec. rewrite CC_cards_time_bound. - poly_mono CCCards_poly. - 2: (replace_le (size (enc (FlatTCC.cards x))) with (size (enc x)) by (rewrite FlatTCC_enc_size; lia)); reflexivity. unfold c__FCC_instance; lia. - + smpl_inO. apply CCCards_poly. + + extract. solverec. rewrite CC_cards_time_bound. + replace_le (size (enc (FlatTCC.cards x))) with (size (enc x)) + by (rewrite FlatTCC_enc_size; lia). + unfold c__FCC_instance; lia. + smpl_inO. apply CCCards_poly. - + evar (f : nat -> nat). exists f. repeat split. + + solve_proper. + + evar (f : nat -> nat). exists f. * intros fpr. unfold FCC_instance. rewrite FlatCC_enc_size; cbn. rewrite CC_cards_size. rewrite list_size_length. rewrite (size_nat_enc 1). rewrite (size_nat_enc 3). instantiate (f := fun n => (1 + c__TCCCardToCCCardSize) * n + 4 * c__natsizeS + 2 * c__natsizeO + 9). subst f. rewrite FlatTCC_enc_size. cbn -[Nat.add Nat.mul]. nia. - * subst f. smpl_inO. - * subst f. smpl_inO. + * unfold f. smpl_inO. + * unfold f. solve_proper. - apply FlatTCC_to_FlatCC. Qed. diff --git a/theories/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v b/theories/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v index 348f880e..1a854d54 100644 --- a/theories/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v +++ b/theories/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v @@ -91,7 +91,7 @@ Instance term_reduction : computableTime' reduction (fun p _ => (let '(ts, maxSi Qed. Lemma TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP : - TMGenNP_fixed M ⪯p FlatFunSingleTMGenNP. + TMGenNP_fixed M ⪯p FlatFunSingleTMGenNP. Proof using index__comp. apply reducesPolyMO_intro with (f := reduction). - evar (f : nat -> nat). exists f. @@ -101,16 +101,15 @@ Instance term_reduction : computableTime' reduction (fun p _ => (let '(ts, maxSi replace_le (size (enc ts)) with (size (enc (ts, n, n0))) by (rewrite !size_prod; cbn; nia). generalize (size (enc (ts, n, n0))). intros n'. [f]: intros n. subst f. cbn. reflexivity. - + subst f. smpl_inO. - + subst f. smpl_inO. + + unfold f. smpl_inO. + + unfold f. solve_proper. + evar (g : nat -> nat). exists g. * intros ((ts & maxSize) & steps). cbn. rewrite !size_prod. cbn. rewrite size_input_index. instantiate (g := fun n => size (enc flatM) + c__listsizeNil + 8 + (c__sizeInputIndex + 1) * n). subst g. cbn. nia. - * subst g. smpl_inO. - * subst g. smpl_inO. + * unfold g. smpl_inO. + * unfold g. solve_proper. - apply reduction_correct. Qed. End fixTM. - diff --git a/theories/NP/SAT/CookLevin/Subproblems/FlatCC.v b/theories/NP/SAT/CookLevin/Subproblems/FlatCC.v index a4220b4f..3b89b31e 100644 --- a/theories/NP/SAT/CookLevin/Subproblems/FlatCC.v +++ b/theories/NP/SAT/CookLevin/Subproblems/FlatCC.v @@ -639,7 +639,7 @@ Proof. split; [intros | ]. - specialize (CCCard_of_size_dec_time_bound (X := nat) y a) as H1. instantiate (2:= fun n => (n + 1) * c__prcardOfSizeDecBound). simp_comp_arith. nia. - - smpl_inO. + - solve_proper. } rewrite list_size_length. replace_le (size(enc (cards fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia). @@ -648,9 +648,9 @@ Proof. replace_le (size(enc(offset fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia). unfold poly__FlatCCWfDec, c__FlatCCWfDecBound. nia. Qed. -Lemma FlatCC_wf_dec_poly : monotonic poly__FlatCCWfDec /\ inOPoly poly__FlatCCWfDec. +Lemma FlatCC_wf_dec_poly : inOPoly poly__FlatCCWfDec. Proof. - unfold poly__FlatCCWfDec; split; smpl_inO. + unfold poly__FlatCCWfDec; smpl_inO. Qed. @@ -669,16 +669,18 @@ Lemma CCCard_ofFlatType_dec_time_bound sig w : CCCard_ofFlatType_dec_time sig w Proof. unfold CCCard_ofFlatType_dec_time. rewrite !list_ofFlatType_dec_time_bound. unfold poly__CCCardOfFlatTypeDec. - poly_mono list_ofFlatType_dec_poly at 2. - 2: (replace_le (size (enc (conc w))) with (size (enc w)) by (rewrite CCCard_enc_size; lia)); reflexivity. - poly_mono list_ofFlatType_dec_poly at 1. - 2: (replace_le (size (enc (prem w))) with (size (enc w)) by (rewrite CCCard_enc_size; lia)); reflexivity. + setoid_replace (size (enc (conc w))) with (size (enc w)) + using relation le by (rewrite CCCard_enc_size; lia). + setoid_replace (size (enc (prem w))) with (size (enc w)) + using relation le by (rewrite CCCard_enc_size; lia). unfold c__CCCardOfFlatTypeDecBound. nia. Qed. -Lemma CCCard_ofFlatType_dec_poly : monotonic poly__CCCardOfFlatTypeDec /\ inOPoly poly__CCCardOfFlatTypeDec. +Lemma CCCard_ofFlatType_dec_poly : inOPoly poly__CCCardOfFlatTypeDec. Proof. - split; unfold poly__CCCardOfFlatTypeDec; smpl_inO; apply list_ofFlatType_dec_poly. -Qed. + unfold poly__CCCardOfFlatTypeDec; smpl_inO; apply list_ofFlatType_dec_poly. +Qed. +#[export] Instance CCCard_ofFlatType_dec_mono: Proper (le ==> le) poly__CCCardOfFlatTypeDec. +Proof. unfold poly__CCCardOfFlatTypeDec. solve_proper. Qed. (** isValidFlattening_dec *) Definition c__isValidFlatteningDec := 3 * c__Sigma + c__init + c__final + c__cards + 16. @@ -700,27 +702,29 @@ Proof. 2: { split; [intros | ]. - rewrite list_ofFlatType_dec_time_bound, Nat.add_comm; reflexivity. - - apply list_ofFlatType_dec_poly. + - solve_proper. } erewrite forallb_time_bound_env. 2 : { split; [intros | ]. - rewrite CCCard_ofFlatType_dec_time_bound, Nat.add_comm; reflexivity. - - apply CCCard_ofFlatType_dec_poly. + - solve_proper. } rewrite !list_size_length. - poly_mono list_ofFlatType_dec_poly at 1. - 2: (replace_le (size (enc (Sigma fpr)) + size (enc (init fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia)); reflexivity. - poly_mono list_ofFlatType_dec_poly at 2. - 2: (replace_le (size (enc (final fpr)) + size (enc (Sigma fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia)); reflexivity. + setoid_replace (size (enc (Sigma fpr)) + size (enc (init fpr))) with (size (enc fpr)) + using relation le by (rewrite FlatCC_enc_size; lia). + setoid_replace (size (enc (final fpr)) + size (enc (Sigma fpr))) with (size (enc fpr)) + using relation le by (rewrite FlatCC_enc_size; lia). replace_le (size (enc (final fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. replace_le (size (enc (cards fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia) at 1. - poly_mono CCCard_ofFlatType_dec_poly at 1. - 2: (replace_le (size (enc (cards fpr)) + size (enc (Sigma fpr))) with (size (enc fpr)) by (rewrite FlatCC_enc_size; lia)); reflexivity. + setoid_replace (size (enc (cards fpr)) + size (enc (Sigma fpr))) with (size (enc fpr)) + using relation le by (rewrite FlatCC_enc_size; lia). unfold poly__isValidFlatteningDec, c__isValidFlatteningDecBound. nia. Qed. -Lemma isValidFlatteningDec_poly : monotonic poly__isValidFlatteningDec /\ inOPoly poly__isValidFlatteningDec. +Lemma isValidFlatteningDec_poly : inOPoly poly__isValidFlatteningDec. Proof. - split; (unfold poly__isValidFlatteningDec; smpl_inO; [apply list_ofFlatType_dec_poly |apply CCCard_ofFlatType_dec_poly ]). -Qed. + unfold poly__isValidFlatteningDec; smpl_inO. + - exact list_ofFlatType_dec_poly. + - exact CCCard_ofFlatType_dec_poly. +Qed. diff --git a/theories/NP/SAT/FSAT/FSAT.v b/theories/NP/SAT/FSAT/FSAT.v index 3625ad85..6e27f0ce 100644 --- a/theories/NP/SAT/FSAT/FSAT.v +++ b/theories/NP/SAT/FSAT/FSAT.v @@ -233,8 +233,7 @@ Proof. unfold poly__formulaMaxVar, c__formulaMaxVarBound1. leq_crossout. - rewrite IHf. setoid_rewrite formula_enc_size at 2. unfold poly__formulaMaxVar, c__formulaMaxVarBound1. leq_crossout. Qed. -Lemma formula_maxVar_poly : monotonic poly__formulaMaxVar /\ inOPoly poly__formulaMaxVar. +Lemma formula_maxVar_poly : inOPoly poly__formulaMaxVar. Proof. - split; unfold poly__formulaMaxVar; smpl_inO. + unfold poly__formulaMaxVar; smpl_inO. Qed. - diff --git a/theories/NP/SAT/FSAT/FSAT_to_SAT.v b/theories/NP/SAT/FSAT/FSAT_to_SAT.v index 0c07a44f..b7363175 100644 --- a/theories/NP/SAT/FSAT/FSAT_to_SAT.v +++ b/theories/NP/SAT/FSAT/FSAT_to_SAT.v @@ -730,9 +730,9 @@ From Complexity.Complexity Require Import UpToCPoly. Require Import Complexity.Libs.CookPrelim.PolyBounds. Lemma reduction_poly_size: - { p: nat -> nat & (forall f, size (enc (reduction f)) <= p (size (enc f))) /\ monotonic p /\ inOPoly p }. + { p: nat -> nat & (forall f, size (enc (reduction f)) <= p (size (enc f))) /\ Proper (le ==> le) p /\ inOPoly p }. Proof. - evar (p : nat -> nat). exists p. split. + evar (p : nat -> nat). exists p. repeat split. - intros f. rewrite cnf_enc_size_bound with (N := reduction f). rewrite cnf_varsIn_bound. @@ -742,7 +742,8 @@ Proof. rewrite formula_size_enc_bound. rewrite formula_maxVar_enc_bound. [p] : intros n. generalize (size (enc f)). subst p. cbn -[Nat.add Nat.mul]. reflexivity. - - split; subst p; smpl_inO. + - unfold p. solve_proper. + - unfold p. smpl_inO. Qed. (** ** Running-time analysis *) @@ -773,9 +774,9 @@ Proof. - rewrite IHf1, IHf2. setoid_rewrite formula_enc_size at 3. nia. - rewrite IHf. setoid_rewrite formula_enc_size at 2. nia. Qed. -Lemma eliminateOR_poly : monotonic poly__eliminateOR /\ inOPoly poly__eliminateOR. +Lemma eliminateOR_poly : inOPoly poly__eliminateOR. Proof. - unfold poly__eliminateOR; split; smpl_inO. + unfold poly__eliminateOR; smpl_inO. Qed. (** tseytinAnd *) @@ -868,9 +869,9 @@ Proof. rewrite formula_size_enc_bound. unfold poly__tseytin', c__tseytinPBound1. leq_crossout. Qed. -Lemma tseytinP_poly : monotonic poly__tseytin' /\ inOPoly poly__tseytin'. +Lemma tseytinP_poly : inOPoly poly__tseytin'. Proof. - unfold poly__tseytin'; split; smpl_inO. + unfold poly__tseytin'; smpl_inO. Qed. (** tseytin *) @@ -889,10 +890,14 @@ Proof. unfold tseytin_time. rewrite tseytinP_time_bound, formula_maxVar_time_bound. unfold poly__tseytin; lia. Qed. -Lemma tseytin_poly : inOPoly poly__tseytin /\ monotonic poly__tseytin. +Lemma tseytin_poly : inOPoly poly__tseytin. Proof. - unfold poly__tseytin; split; smpl_inO; first [apply formula_maxVar_poly | apply tseytinP_poly]. -Qed. + unfold poly__tseytin; smpl_inO. + - exact formula_maxVar_poly. + - unfold poly__tseytin'. smpl_inO. +Qed. +#[export] Instance tseytin_mono: Proper (le ==> le) poly__tseytin. +Proof. unfold poly__tseytin, poly__formulaMaxVar, poly__tseytin'. solve_proper. Qed. (** reduction *) Lemma eliminateOR_enc_size_bound f : size (enc (eliminateOR f)) <= c__eliminateOrSize * size (enc f). @@ -911,22 +916,25 @@ Definition reduction_time (f : formula) := eliminateOR_time f + tseytin_time (el #[export] Instance term_reduction : computableTime' reduction (fun f _ => (reduction_time f, tt)). Proof. - extract. solverec. unfold reduction_time, c__reduction. solverec. + extract. solverec. reflexivity. Qed. Definition poly__reduction n := poly__eliminateOR n + poly__tseytin (c__eliminateOrSize * n) + c__reduction. Lemma reduction_time_bound f : reduction_time f <= poly__reduction (size (enc f)). Proof. unfold reduction_time. rewrite eliminateOR_time_bound, tseytin_time_bound. - poly_mono tseytin_poly. 2: apply eliminateOR_enc_size_bound. + rewrite eliminateOR_enc_size_bound. unfold poly__reduction. nia. Qed. -Lemma reduction_poly : monotonic poly__reduction /\ inOPoly poly__reduction. +Lemma reduction_poly : inOPoly poly__reduction. Proof. - unfold poly__reduction; split; smpl_inO; try apply inOPoly_comp; smpl_inO; first [apply tseytin_poly | apply eliminateOR_poly]. -Qed. - - + unfold poly__reduction; smpl_inO. + - exact eliminateOR_poly. + - apply inOPoly_comp; [solve_proper | exact tseytin_poly | smpl_inO]. +Qed. +#[export] Instance reduction_mono: Proper (le ==> le) poly__reduction. +Proof. unfold poly__reduction, poly__eliminateOR. solve_proper. Qed. + (** ** full reduction *) Theorem FSAT_to_SAT_poly : FSAT ⪯p SAT. Proof. @@ -935,7 +943,7 @@ Proof. + eexists. eapply computesTime_timeLeq. 2: apply term_reduction. cbn -[Nat.add Nat.mul]. intros f _. split; [ | easy]. apply reduction_time_bound. + apply reduction_poly. - + apply reduction_poly. + + solve_proper. + destruct (reduction_poly_size) as (h & H1 & H2). exists h; [apply H1 | apply H2 | apply H2]. - apply FSAT_to_SAT. Qed. @@ -947,7 +955,7 @@ Proof. + eexists. eapply computesTime_timeLeq. 2: apply term_reduction. cbn -[Nat.add Nat.mul]. intros f _. split; [ | easy]. apply reduction_time_bound. + apply reduction_poly. - + apply reduction_poly. + + solve_proper. + destruct (reduction_poly_size) as (h & H1 & H2). exists h; [apply H1 | apply H2 | apply H2]. - apply FSAT_to_3SAT. Qed. diff --git a/theories/NP/SAT/FSAT/FormulaEncoding.v b/theories/NP/SAT/FSAT/FormulaEncoding.v index 1d765b76..e046f932 100644 --- a/theories/NP/SAT/FSAT/FormulaEncoding.v +++ b/theories/NP/SAT/FSAT/FormulaEncoding.v @@ -458,10 +458,10 @@ Proof. unfold add_time. rewrite size_nat_enc_r with (n := step) at 1. unfold poly__tabulateStep; solverec. Qed. -Lemma tabulate_step_poly : monotonic poly__tabulateStep /\ inOPoly poly__tabulateStep. -Proof. - unfold poly__tabulateStep; split; smpl_inO. -Qed. +Lemma tabulate_step_poly : inOPoly poly__tabulateStep. +Proof. unfold poly__tabulateStep; smpl_inO. Qed. +#[export] Instance tabulate_step_mono: Proper (le ==> le) poly__tabulateStep. +Proof. unfold poly__tabulateStep. solve_proper. Qed. Lemma tabulate_step_length step s n: |tabulate_step step s n| = n. Proof. @@ -485,14 +485,15 @@ Qed. Lemma tabulate_formula_varsIn s step n t (g : nat -> nat): (forall start, formula_varsIn (fun n => n < g start) (t start)) - -> monotonic g + -> Proper (le ==> le) g -> forall f, f el tabulate_formula s step n t -> formula_varsIn (fun v => v < g (s + step * (n -1))) f. Proof. intros H H0 f Hel. unfold tabulate_formula in Hel. apply in_map_iff in Hel as (i & <- & Hel). apply in_tabulate_step_iff in Hel as (i' & H1 & ->). eapply formula_varsIn_monotonic. 2: apply H. - cbn. intros n' Hn'. unfold monotonic in H0. specialize (H0 (s + step * i') (s + step * (n -1)) ltac:(nia)). nia. + cbn. intros n' Hn'. + specialize (H0 (s + step * i') (s + step * (n -1)) ltac:(nia)). nia. Qed. Lemma tabulate_formula_length s step n t : |tabulate_formula s step n t| = n. @@ -541,10 +542,10 @@ Proof. unfold encodeListAt_time. rewrite list_size_length. unfold poly__encodeListAt; solverec. Qed. -Lemma encodeListAt_poly : monotonic poly__encodeListAt /\ inOPoly poly__encodeListAt. -Proof. - unfold poly__encodeListAt; split; smpl_inO. -Qed. +Lemma encodeListAt_poly : inOPoly poly__encodeListAt. +Proof. unfold poly__encodeListAt; smpl_inO. Qed. +#[export] Instance encodeListAt_mono: Proper (le ==> le) poly__encodeListAt. +Proof. unfold poly__encodeListAt. solve_proper. Qed. Lemma encodeListAt_varsIn start l: formula_varsIn (fun n => n >= start /\ n < start + |l|) (encodeListAt start l). Proof. diff --git a/theories/NP/SAT/SAT_inNP.v b/theories/NP/SAT/SAT_inNP.v index bff210b3..0f7cdc61 100644 --- a/theories/NP/SAT/SAT_inNP.v +++ b/theories/NP/SAT/SAT_inNP.v @@ -99,6 +99,7 @@ Section fixX. rewrite IHa. split; [ firstorder | intros [[-> | H2] H3]; [congruence | auto]]. Qed. + (*TODO: replace with Coq.Lists.List.nodup *) Fixpoint dedup (a : list X) := match a with | [] => [] | x :: a => if list_in_decb eqbX a x then dedup a else x :: dedup a @@ -422,8 +423,9 @@ Instance term_evalClause : computableTime' evalClause _ := projT2 _term_evalClau { intros (a & C). unfold evalClause_time. rewrite !list_size_length. rewrite maxSize_enc_size. rewrite size_prod. cbn. [p] : exact (n * n * n). - and_solve p. } - all: subst p; smpl_inO. + and_solve p. } + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. Arguments evalClause_time: simpl never. @@ -458,7 +460,8 @@ Instance term_evalCnf : computableTime' evalCnf _ := projT2 _term_evalCnf. inst_const. } rewrite sumn_map_const. rewrite list_size_length. rewrite size_prod. [p]: exact (n * isP__poly evalClause_poly n + n + 1). and_solve p. } - all: subst p; smpl_inO. + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. (** sat_verifierb *) @@ -488,7 +491,8 @@ Proof. intros cn a H. cbn. exists a; tauto. - unfold SAT, sat_verifier. intros cn [a H]. exists (compressAssignment a cn). split. + apply compressAssignment_cnf_equiv in H. cbn. apply H. - + apply assignment_small_size. cbn. apply compressAssignment_small. + + apply assignment_small_size, compressAssignment_small. + - solve_proper. } unfold inTimePoly. exists_poly p. repeat split. @@ -499,5 +503,6 @@ Proof. set (L_facts.size _). [p]: intros n. and_solve p. + intros [N a]. cbn. apply sat_verifierb_correct. } - all: subst p; smpl_inO. + - unfold p. smpl_inO. + - unfold p. solve_proper. Qed. diff --git a/theories/NP/SAT/kSAT.v b/theories/NP/SAT/kSAT.v index a70e35fd..8b444933 100644 --- a/theories/NP/SAT/kSAT.v +++ b/theories/NP/SAT/kSAT.v @@ -7,7 +7,7 @@ From Undecidability.L.Functions Require Import EqBool. Inductive kCNF (k : nat) : cnf -> Prop := | kCNFB : kCNF k [] -| kCNFS (N : cnf) (C : clause) : (|C|) = k -> kCNF k N -> kCNF k (C :: N). +| kCNFS (N : cnf) (C : clause) : (|C|) = k -> kCNF k N -> kCNF k (C :: N). #[export] Hint Constructors kCNF : core. @@ -76,12 +76,13 @@ Proof. instantiate (1 := encodable_nat_enc). instantiate (1 := fun n => (c__length + c__eqbComp nat) * (n + 1) + c__clauseLengthDecb). cbn -[Nat.add Nat.mul]. solverec. - - smpl_inO. + - solve_proper. } rewrite list_size_length. unfold poly__kCNFDecb, c__kCNFDecbBound1, c__kCNFDecbBound2. lia. -Qed. -Lemma kCNF_decb_poly : monotonic poly__kCNFDecb /\ inOPoly poly__kCNFDecb. -Proof. - unfold poly__kCNFDecb. split; smpl_inO. -Qed. +Qed. + +Lemma kCNF_decb_poly : inOPoly poly__kCNFDecb. +Proof. unfold poly__kCNFDecb. smpl_inO. Qed. +#[export] Instance kCNF_decb_mono: Proper (le ==> le) poly__kCNFDecb. +Proof. unfold poly__kCNFDecb. solve_proper. Qed. diff --git a/theories/NP/SAT/kSAT_to_SAT.v b/theories/NP/SAT/kSAT_to_SAT.v index 23264262..70ea9bf5 100644 --- a/theories/NP/SAT/kSAT_to_SAT.v +++ b/theories/NP/SAT/kSAT_to_SAT.v @@ -7,11 +7,11 @@ Proof. destruct k. { (* always return a trivial no-instance if k = 0 *) apply reducesPolyMO_intro with (f := fun N => [[(true, 0)]; [(false, 0)]]). - - exists (fun n => 13). - + extract. solverec. - + smpl_inO. - + smpl_inO. - + exists (fun n => size (enc [[(true, 0)]; [(false, 0)]])); [solverec | smpl_inO | smpl_inO]. + - exists (fun n => 13); [extract; solverec | smpl_inO | apply monotonic_c |]. + exists (fun n => size (enc [[(true, 0)]; [(false, 0)]])). + + solverec. + + smpl_inO. + + apply monotonic_c. - intros N. cbn. unfold kSAT. split; [lia | ]. intros [a H]. unfold satisfies, evalCnf in H; cbn in H. @@ -25,14 +25,15 @@ Proof. all: rewrite kCNF_decb_time_bound. instantiate (f := fun n => poly__kCNFDecb (n + size (enc (S k))) + 18). all: subst f; solverec. - + subst f; smpl_inO. apply inOPoly_comp; smpl_inO; apply kCNF_decb_poly. - + subst f; smpl_inO. apply kCNF_decb_poly. + + subst f; smpl_inO. + apply inOPoly_comp; [solve_proper | apply kCNF_decb_poly | smpl_inO]. + + unfold f. solve_proper. + evar (g : nat -> nat). exists g. * intros N. destruct kCNF_decb. instantiate (g := fun n => n + size (enc [[(true, 0)]; [(false, 0)]])). all: subst g; solverec. - * subst g; smpl_inO. - * subst g; smpl_inO. + * subst g. smpl_inO. + * unfold g. solve_proper. - intros N. split. + intros [H1 [H2 H3]]. apply kCNF_decb_iff in H2. rewrite H2. apply H3. diff --git a/theories/NP/TM/LM_to_mTM.v b/theories/NP/TM/LM_to_mTM.v index 8db8df12..83eb3a40 100644 --- a/theories/NP/TM/LM_to_mTM.v +++ b/theories/NP/TM/LM_to_mTM.v @@ -11,8 +11,6 @@ From Undecidability.TM.L Require M_LHeapInterpreter. Set Default Proof Using "Type". -(* Check LMtoTM.M. *) - From Undecidability Require Import LSum. From Complexity Require Import L.TM.CompCode. @@ -161,10 +159,6 @@ End M. From Complexity Require Import PolyTimeComputable. -(*REMOVE?*) -Import GenericNary UpToCNary. -From Coq Require Import CRelationClasses CMorphisms. - (* TODO MOVE :tidy up *) Lemma pTC_length X `{encodable X}: polyTimeComputable (@length X). Proof. @@ -173,10 +167,12 @@ Proof. { eapply computableTime_timeLeq. 2:exact _. solverec. rewrite size_list_enc_r. set (n:=L_facts.size _). [time]:refine (fun n => _). unfold time. reflexivity. } - 1,2:unfold time;now smpl_inO. - eexists (fun n => _). - {intros. rewrite !LNat.size_nat_enc, size_list_enc_r. set (n:= L_facts.size _). reflexivity. } - 1,2:unfold time;now smpl_inO. + - unfold time. smpl_inO. + - unfold time. solve_proper. + - eexists (fun n => _). + + intros. rewrite !LNat.size_nat_enc, size_list_enc_r. set (n:= L_facts.size _). reflexivity. + + smpl_inO. + + solve_proper. Qed. Smpl Add 1 simple apply pTC_length : polyTimeComputable. @@ -248,7 +244,7 @@ Smpl Add 5 lazymatch goal with Lemma mono_map_time X `{encodable X} (f: nat -> nat) (xs: list X): - monotonic f + Proper (le ==> le) f -> sumn (map (fun x => f (L_facts.size (enc x))) xs) <= length xs * f (L_facts.size (enc xs)). Proof. intros Hf. @@ -268,7 +264,8 @@ Proof. unshelve erewrite (_ : length x <= n). now apply size_list_enc_r. [time]:intro. unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO. + { unfold time. smpl_inO. } + { unfold time. solve_proper. } evar (size:nat -> nat). exists size. {intros x. rewrite size_list,sumn_map_add,sumn_map_c,map_map,map_length. rewrite sumn_map_le_pointwise. @@ -278,7 +275,8 @@ Proof. unshelve erewrite (_ : length x <= n). now apply size_list_enc_r. [size]:intro. unfold size. reflexivity. } - 1,2:now unfold size;smpl_inO. + { unfold size. smpl_inO. } + { unfold size. solve_proper. } Qed. @@ -297,7 +295,8 @@ Proof. set (n:=L_facts.size _). [time]:intro. unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO. + { unfold time. smpl_inO. } + { unfold time. solve_proper. } evar (size:nat -> nat). exists size. {intros x. rewrite size_list, sumn_map_add,sumn_map_c. @@ -323,7 +322,8 @@ Proof. } set (L_facts.size _). [size]:intros n. unfold size. reflexivity. } - 1,2:unfold size;smpl_inO. + - unfold size. smpl_inO. + - unfold size. solve_proper. Qed. Lemma pTC_app X Y `{encodable X} `{encodable Y} (f1 f2:X -> list Y): @@ -337,14 +337,16 @@ Proof. { rewrite LProd.size_prod,size_list_enc_r;cbn. nia. } set (L_facts.size _). [time]:intro. now unfold time. } - 1,2:now unfold time;smpl_inO. + { unfold time. smpl_inO. } + { unfold time. solve_proper. } { evar (size : nat -> nat). exists size. { intros [a b]. rewrite LProd.size_prod, !size_list,map_app,sumn_app,!sumn_map_add,!sumn_map_c. cbn [fst snd]. [size]:exact (fun x => x + 4). unfold size. lia. } - all:unfold size;smpl_inO. + - unfold size. smpl_inO. + - unfold size. solve_proper. } Qed. @@ -359,19 +361,21 @@ Proof. Unshelve. solverec. 1,2:now smpl_inO. evar (size : nat -> nat). exists size. unfold enc at 1;cbn;intros x. set (n0:=L_facts.size (enc x)). [size]:intros n0. repeat (unfold enc,size; cbn). reflexivity. - all:unfold size. all:smpl_inO. + - unfold size. smpl_inO. + - unfold size. solve_proper. } eapply pTC_app. 2:now apply pTC_cnst. eapply polyTimeComputable_composition. - 2:{ eapply pTC_map. exists (fun _ => 4). extract. solverec. 1,2:now smpl_inO. - exists (fun x => x+4). - {intros. now setoid_rewrite size_sum. } - all:smpl_inO. + 2:{ eapply pTC_map. + exists (fun _ => 4); [ | apply inOPoly_c | easy | ]. + - extract. solverec. + - exists (fun x => x+4); [ | smpl_inO | solve_proper]. + intro. now rewrite size_sum. } unfold Encode_map. cbn. - eapply polyTimeComputable_composition. eassumption. - eapply pTC_map. eassumption. + eapply polyTimeComputable_composition. assumption. + apply pTC_map. assumption. Qed. Smpl Add 5 unshelve simple eapply pTC_initValue : polyTimeComputable. @@ -385,18 +389,15 @@ Lemma pTC_Encode_Com : polyTimeComputable (Encode_Com). Proof. unfold Encode_Com;cbn. unfold Com_to_sum. change (fun x1 : sigNat => sigSum_X x1) with (@sigSum_X sigNat ACom). - eexists (fun x => x*(11 + c__app + c__map) + 16 + c__app + c__map). + eexists (fun x => x*(11 + c__app + c__map) + 16 + c__app + c__map); [ | smpl_inO | solve_proper | ]. {extract. solverec. rewrite map_time_const,app_length,!repeat_length,size_Tok_enc. cbn [length]. nia. } - 1,2:now smpl_inO. - eexists (fun x => x*5 + 33). - { intros [];cbn. 2-4:now cbv. - rewrite size_list;unfold enc;cbn - ["+"]. - rewrite map_app,map_repeat,sumn_map_add,sumn_map_c,map_app,sumn_app,map_repeat,map_map,app_length,repeat_length,map_length,sumn_repeat. - unfold enc. cbn;ring_simplify. rewrite LNat.size_nat_enc. unfold LNat.c__natsizeS, LNat.c__natsizeO, c__listsizeNil, c__listsizeCons. - nia. - } - 1,2:now smpl_inO. + eexists (fun x => x*5 + 33); [ | smpl_inO | solve_proper]. + intros [];cbn. 2-4:now cbv. + rewrite size_list;unfold enc;cbn - ["+"]. + rewrite map_app,map_repeat,sumn_map_add,sumn_map_c,map_app,sumn_app,map_repeat,map_map,app_length,repeat_length,map_length,sumn_repeat. + unfold enc. cbn;ring_simplify. rewrite LNat.size_nat_enc. unfold LNat.c__natsizeS, LNat.c__natsizeO, c__listsizeNil, c__listsizeCons. + nia. Qed. Lemma pTC_Encode_Prog : polyTimeComputable (Alphabets.Encode_Prog). @@ -409,7 +410,9 @@ Proof. eapply polyTimeComputable_composition. exact pTC_Encode_Com. eapply pTC_map. {eexists (fun x => _). eapply term_sigList_X. 1,2:now smpl_inO. - eexists (fun x => _). intros x. rewrite size_sigList. set (L_facts.size _). reflexivity. all:smpl_inO. + eexists (fun x => _). intros x. rewrite size_sigList. set (L_facts.size _). reflexivity. + - smpl_inO. + - solve_proper. } repeat smpl polyTimeComputable. Qed. @@ -418,9 +421,13 @@ Smpl Add 1 simple eapply pTC_Encode_Prog : polyTimeComputable. Lemma pTC_inl X Y `{encodable X} `{encodable Y} : polyTimeComputable (@inl X Y). Proof. - eexists (fun x => _). eapply term_inl. 1, 2: smpl_inO. - eexists (fun x => _). intros x. rewrite size_sum. set (L_facts.size (enc x)). reflexivity. - all: smpl_inO. + eexists (fun x => _). eapply term_inl. + - apply inOPoly_c. + - easy. + - eexists (fun x => _). + + intros x. rewrite size_sum. set (L_facts.size (enc x)). reflexivity. + + smpl_inO. + + solve_proper. Qed. Smpl Add 1 eapply pTC_inl : polyTimeComputable. @@ -527,10 +534,17 @@ Proof. now eapply pTC_id. 3, 4: smpl polyTimeComputable. 2:{ eexists (fun x => _). eapply term_sigList_X. 1,2:now smpl_inO. - eexists (fun x => _). intros x. rewrite size_sigList. set (size _). reflexivity. all:smpl_inO. + eexists (fun x => _). intros x. rewrite size_sigList. set (size _). reflexivity. + - smpl_inO. + - solve_proper. } - { eexists (fun x' => _). now apply (term_sigPair_Y). 1,2:now smpl_inO. - eexists (fun x => 4 + _). intros x. unfold enc;cbn. set (size _). reflexivity. all:smpl_inO. + { eexists (fun x' => _). now apply (term_sigPair_Y). + - apply inOPoly_c. + - easy. + - eexists (fun x => 4 + _). + + intros x. unfold enc;cbn. set (size _). reflexivity. + + smpl_inO. + + solve_proper. } } -unfold f__steps. nary apply pTC_destructuringToProj. @@ -540,4 +554,3 @@ Proof. repeat smpl polyTimeComputable. } Qed. - diff --git a/theories/NP/TM/L_to_LM.v b/theories/NP/TM/L_to_LM.v index ebc7305a..01b150b3 100644 --- a/theories/NP/TM/L_to_LM.v +++ b/theories/NP/TM/L_to_LM.v @@ -51,23 +51,23 @@ Proof. {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. now rewrite LTerm.size_term_enc_r at 1. } unfold time. unfold add_time, mult_time. rewrite H . reflexivity. } - 1,2:now unfold time;smpl_inO. - {unfold f. evar (resSize : nat -> nat). [resSize]:intros n0. eexists resSize. - {intros [[x mSize] steps]. - set(n0:=size (enc (x, mSize, steps))). - rewrite !LProd.size_prod;cbn [fst snd]. - setoid_rewrite size_nat_enc at 2. - eassert (steps <= n0) as ->. - {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. now rewrite size_nat_enc_r at 1. } - eassert (size (enc mSize) <= n0) as ->. - {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. easy. } - rewrite compile_enc_size. - eassert (size x <= n0) as ->. - {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. now rewrite size_term_enc_r at 1. } - unfold resSize. reflexivity. - } - 1,2:unfold resSize;smpl_inO. - } + - unfold time. smpl_inO. + - unfold time. solve_proper. + - unfold f. evar (resSize : nat -> nat). [resSize]:intros n0. eexists resSize. + + intros [[x mSize] steps]. + set(n0:=size (enc (x, mSize, steps))). + rewrite !LProd.size_prod;cbn [fst snd]. + setoid_rewrite size_nat_enc at 2. + eassert (steps <= n0) as ->. + {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. now rewrite size_nat_enc_r at 1. } + eassert (size (enc mSize) <= n0) as ->. + {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. easy. } + rewrite compile_enc_size. + eassert (size x <= n0) as ->. + {subst n0. rewrite !LProd.size_prod;cbn [fst snd]. now rewrite size_term_enc_r at 1. } + unfold resSize. reflexivity. + + unfold resSize. smpl_inO. + + unfold resSize. solve_proper. Qed. (* diff --git a/theories/NP/TM/TMGenNP.v b/theories/NP/TM/TMGenNP.v index 40b079de..c39a8096 100644 --- a/theories/NP/TM/TMGenNP.v +++ b/theories/NP/TM/TMGenNP.v @@ -84,15 +84,17 @@ Proof. destruct (Nat.leb_spec (sizeOfmTapesFlat t) maxSize). - rewrite Hf''. hnf in monof''. rewrite monof'' with (x':=x). + rewrite Hf''. + setoid_replace (size (enc M) + sizeOfmTapesFlat t + steps) with x + using relation le. 2:{rewrite H. subst x. rewrite !size_prod. cbn [fst snd]. rewrite <- !size_nat_enc_r. lia. } destruct execFlatTM. all:unfold f'. reflexivity. all:lia. } - all:unfold f'. - all:smpl_inO. + + unfold f'. smpl_inO. + + unfold f'. solve_proper. -evar (f:nat -> nat). [f]:intro x. exists f. +intros [[TM maxSize] steps] y. cbn. @@ -112,6 +114,6 @@ Proof. all:rewrite size_nat_enc_r at 1; subst;nia. } unfold f;reflexivity. - +unfold f;smpl_inO. - +unfold f;smpl_inO. + + unfold f;smpl_inO. + + unfold f. solve_proper. Qed. diff --git a/theories/NP/TM/mTM_to_singleTapeTM.v b/theories/NP/TM/mTM_to_singleTapeTM.v index a12c882a..46c0d52b 100644 --- a/theories/NP/TM/mTM_to_singleTapeTM.v +++ b/theories/NP/TM/mTM_to_singleTapeTM.v @@ -189,7 +189,8 @@ Section LMGenNP_to_TMGenNP_mTM. unfold add_time, mult_time. unshelve erewrite (_ : a0 <= n0). nia. unshelve erewrite (_ : b0 <= n0). nia. unshelve erewrite (_ : b <= n0). nia. unfold time. reflexivity. } - 1,2:unfold time;smpl_inO. + { unfold time. smpl_inO. } + { unfold time. solve_proper. } { evar (f__size : nat -> nat). [f__size]:intros n0. exists f__size. { intros [[a0 b0] b]. unfold f__nice. set (n0:=(L_facts.size (enc (a0, b0, b)))). @@ -200,7 +201,8 @@ Section LMGenNP_to_TMGenNP_mTM. change S with (plus 1). unfold f__size;reflexivity. } - all:unfold f__size;smpl_inO. + - unfold f__size. smpl_inO. + - unfold f__size. solve_proper. } } clearbody f__nice. @@ -211,15 +213,16 @@ Section LMGenNP_to_TMGenNP_mTM. eexists (fun _ => c0). { unfold t__size. extract. solverec. all:rewrite eqbTime_le_l. all:set (c:=L_facts.size (enc 0)). all:cbv in c;subst c. all:subst c0. 2:easy. nia. } - 1,2:smpl_inO. + { apply inOPoly_c. } + { apply monotonic_c. } { evar (f__size : nat -> nat). [f__size]:intros n0. exists f__size. { intros x. unfold t__size. set (n0:=(L_facts.size (enc x))). assert (Hx:x<=n0) by apply size_nat_enc_r. rewrite size_nat_enc. destruct _. 2:rewrite Hx;unfold f__size;reflexivity. unfold f__size. nia. } - - all:unfold f__size;smpl_inO. + - unfold f__size. smpl_inO. + - unfold f__size. solve_proper. } }clearbody t__size. @@ -251,7 +254,8 @@ Section LMGenNP_to_TMGenNP_mTM. rewrite sizeOfmTapes_by_size. set (L_facts.size _). unfold time. reflexivity. } - 1,2:now unfold time;change S with (plus 1);smpl_inO. + { unfold time. smpl_inO. } + { unfold time. solve_proper. } { evar (f__size : nat -> nat). [f__size]:intros n0. exists f__size. { intros x. unfold t__start. rewrite size_list_cons. subst g f. @@ -271,7 +275,8 @@ Section LMGenNP_to_TMGenNP_mTM. rewrite sumn_map_c. rewrite Vector.length_to_list. setoid_rewrite sizeOfmTapes_by_size. set (n0:= L_facts.size _). ring_simplify. unfold f__size. reflexivity. } - all:unfold f__size;smpl_inO. + - unfold f__size. smpl_inO. + - unfold f__size. solve_proper. } } clearbody f__steps t__start. @@ -283,13 +288,14 @@ Section LMGenNP_to_TMGenNP_mTM. extract. solverec. remember (L_facts.size (enc (a0, b0, b))) as n0 eqn:Hn0. rewrite !size_prod in Hn0. cbn [fst snd] in Hn0. - erewrite (mono__polyTC X0 (x':=n0)). 2:{ subst n0. repeat set (L_facts.size _). nia. } - rewrite (mono__polyTC X1 (x':=n0)). 2:{ subst n0. repeat set (L_facts.size _). nia. } + setoid_replace (size (enc b0)) with n0 using relation le at 1 by nia. + setoid_replace (size (enc a0)) with n0 using relation le at 1. + 2:{ subst n0. repeat apply Arith_prebase.le_plus_trans_stt. reflexivity. } set (c0 := 5+c__natsizeO +c__natsizeS). assert (H'' : L_facts.size (enc (b, sizeOfmTapes a0, b0)) <= n0*c0). { rewrite !size_prod. cbn [fst snd]. setoid_rewrite size_nat_enc at 2. rewrite sizeOfmTapes_by_size. subst n0. repeat set (L_facts.size _). nia. } - setoid_rewrite (mono__polyTC X (x':=n0*c0)). 2:exact H''. + rewrite H'' at 1. specialize (bounds__rSP (f:=f__nice)) as H'. setoid_rewrite <- size_nat_enc_r in H'. unfold mult_time, add_time. unshelve rewrite H'. now apply resSize__polyTC. @@ -297,7 +303,11 @@ Section LMGenNP_to_TMGenNP_mTM. rewrite sizeOfmTapes_by_size at 1. unshelve erewrite (_ : L_facts.size (enc a0) <= n0). now (subst n0;clear;repeat set (L_facts.size _);nia). unfold time. reflexivity. } - 1,2:now unfold time;smpl_inO;apply inOPoly_comp;smpl_inO. + { unfold time. smpl_inO. all: apply inOPoly_comp. + 1,4,7: solve_proper. + all: smpl_inO. + } + { unfold time. solve_proper. } { evar (f__size : nat -> nat). [f__size]:intros n0. exists f__size. { intros [[a0 b0] b]. remember (L_facts.size (enc (a0, b0, b))) as n0 eqn:Hn0. rewrite !size_prod in Hn0|-*. cbn [fst snd] in Hn0|-*. rewrite !size_nat_enc. @@ -309,19 +319,19 @@ Section LMGenNP_to_TMGenNP_mTM. setoid_rewrite mono__rSP. 2:exact H''. specialize (bounds__rSP (f:=t__size)) as Hsize. setoid_rewrite <- size_nat_enc_r in Hsize at 1. - unshelve rewrite Hsize. now apply resSize__polyTC. - setoid_rewrite (mono__rSP _ (x':=n0)) at 1 . 2:nia. + unshelve rewrite Hsize. now apply resSize__polyTC. + setoid_replace (size (enc b0)) with n0 using relation le at 1 by nia. specialize (bounds__rSP (f:=t__start)) as Hstart. - unshelve rewrite Hstart. now apply resSize__polyTC. - setoid_rewrite (mono__rSP _ (x':=n0)) at 1 . 2:subst;clear;repeat (set (L_facts.size _));nia. + unshelve rewrite Hstart. now apply resSize__polyTC. + setoid_replace (size (enc a0)) with n0 using relation le. + 2:subst;clear;repeat (set (L_facts.size _));nia. unfold f__size. reflexivity. } - 1,2:unfold f__size;smpl_inO; apply inOPoly_comp;smpl_inO. - + - unfold f__size. smpl_inO. + apply inOPoly_comp; [apply monotonic_rSP | apply poly__rSP | smpl_inO]. + - unfold f__size. solve_proper. } - - Qed. (* Print Assumptions LMGenNP_to_TMGenNP_mTM. *)