use Proper and rewrite from stdlib for monotonicity

_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

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,27 +77,35 @@ 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
   {
     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.

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.