[Merged by Bors] - fix(tactic/monotonicity): support monotone in mono

scripts/nolints.txt

@@ -1899,8 +1899,8 @@ apply_nolint tactic.interactive.mono_cfg doc_blame
 apply_nolint tactic.interactive.mono_head_candidates doc_blame
 apply_nolint tactic.interactive.mono_key doc_blame
 apply_nolint tactic.interactive.mono_selection doc_blame
-apply_nolint tactic.interactive.monotoncity.check doc_blame unused_arguments
-apply_nolint tactic.interactive.monotoncity.check_rel doc_blame unused_arguments
+apply_nolint tactic.interactive.monotonicity.check doc_blame 
+apply_nolint tactic.interactive.monotonicity.check_rel doc_blame 
 apply_nolint tactic.interactive.monotonicity.attr doc_blame
 apply_nolint tactic.interactive.same_operator doc_blame
 apply_nolint tactic.interactive.side doc_blame
@@ -2317,4 +2317,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/tactic/monotonicity/basic.lean

@@ -69,7 +69,7 @@ let fn₀ := e₀.get_app_fn,
 meta def get_operator (e : expr) : option name :=
 guard (¬ e.is_pi) >> pure e.get_app_fn.const_name
 
-meta def monotoncity.check_rel (xs : list expr) (l r : expr) : tactic (option name) :=
+meta def monotonicity.check_rel (l r : expr) : tactic (option name) :=
 do guard (same_operator l r) <|>
      do { fail format!"{l} and {r} should be the f x and f y for some f" },
    if l.is_pi then pure none
@@ -81,21 +81,22 @@ def mono_key := (with_bot name × with_bot name)
 open nat
 
 meta def mono_head_candidates : ℕ → list expr → expr → tactic mono_key
-| 0 _ h := failed
+| 0 _ h := fail!"Cannot find relation in {h}"
 | (succ n) xs h :=
   do { (rel,l,r) ← if h.is_arrow
            then pure (none,h.binding_domain,h.binding_body)
            else guard h.get_app_fn.is_constant >>
                 prod.mk (some h.get_app_fn.const_name) <$> last_two h.get_app_args,
-       prod.mk <$> monotoncity.check_rel xs.reverse l r <*> pure rel } <|>
+       prod.mk <$> monotonicity.check_rel l r <*> pure rel } <|>
          match xs with
          | [] := fail format!"oh? {h}"
          | (x::xs) := mono_head_candidates n xs (h.pis [x])
          end
 
-meta def monotoncity.check (lm_n : name) (prio : ℕ) (persistent : bool) : tactic mono_key :=
+meta def monotonicity.check (lm_n : name) : tactic mono_key :=
 do lm ← mk_const lm_n,
    lm_t ← infer_type lm,
+   lm_t ← expr.dsimp lm_t { fail_if_unchanged := ff } tt [] [simp_arg_type.expr ``(monotone)],
    (xs,h) ← mk_local_pis lm_t,
    mono_head_candidates 3 xs.reverse h
 
@@ -133,7 +134,7 @@ meta def monotonicity.attr : user_attribute
          (native.rb_lmap.mk mono_key _)  }
 , after_set := some $ λ n prio p,
   do { (none,v) ← monotonicity.attr.get_param n | pure (),
-       k ← monotoncity.check n prio p,
+       k ← monotonicity.check n,
        monotonicity.attr.set n (some k,v) p }
 , parser := prod.mk none <$> side }
 
@@ -162,4 +163,3 @@ attribute [mono] add_le_add mul_le_mul neg_le_neg
          sub_le_sub abs_le_abs
 attribute [mono left] add_lt_add_of_le_of_lt mul_lt_mul'
 attribute [mono right] add_lt_add_of_lt_of_le mul_lt_mul
-open tactic.interactive

src/tactic/monotonicity/interactive.lean

@@ -132,7 +132,7 @@ meta def match_ac'
  | es [] := do
 return ([],es,[])
 
-meta def match_ac (unif : bool) (l : list expr) (r : list expr)
+meta def match_ac (l : list expr) (r : list expr)
 : tactic (list expr × list expr × list expr) :=
 do (s',l',r') ← match_ac' l r,
    s' ← mmap instantiate_mvars s',
@@ -213,7 +213,7 @@ do (full_f,ls,rs) ← same_function l r,
    if a
    then if c
    then do
-     (s,ls,rs) ← monad.join (match_ac tt
+     (s,ls,rs) ← monad.join (match_ac
                    <$> parse_assoc_chain f l
                    <*> parse_assoc_chain f r),
      (l',l_id) ← fold_assoc f i ls,
@@ -353,6 +353,7 @@ end
 meta def match_rule (pat : expr) (r : name) : tactic expr :=
 do  r' ← mk_const r,
     t  ← infer_type r',
+    t  ← expr.dsimp t { fail_if_unchanged := ff } tt [] [simp_arg_type.expr ``(monotone)],
     match_rule_head pat [] r' t
 
 meta def find_lemma (pat : expr) : list name → tactic (list expr)
@@ -467,7 +468,7 @@ do t ← target,
         fail format!"ambiguous match: {msg}\n\nTip: try asserting a side condition to distinguish between the lemmas"
    end
 
-meta def mono_aux (dir : parse side) (cfg : mono_cfg := { mono_cfg . }) :
+meta def mono_aux (dir : parse side) :
   tactic unit :=
 do t ← target >>= instantiate_mvars,
    ns ← get_monotonicity_lemmas t dir,
@@ -521,15 +522,14 @@ by mono*
 meta def mono (many : parse (tk "*")?)
   (dir : parse side)
   (hyps : parse $ tk "with" *> pexpr_list_or_texpr <|> pure [])
-  (simp_rules : parse $ tk "using" *> simp_arg_list <|> pure [])
-  (cfg : mono_cfg := { mono_cfg . }) :
+  (simp_rules : parse $ tk "using" *> simp_arg_list <|> pure []) :
   tactic unit :=
 do hyps ← hyps.mmap (λ p, to_expr p >>= mk_meta_var),
    hyps.mmap' (λ pr, do h ← get_unused_name `h, note h none pr),
    when (¬ simp_rules.empty) (simp_core { } failed tt simp_rules [] (loc.ns [none])),
    if many.is_some
-     then repeat $ mono_aux dir cfg
-     else mono_aux dir cfg,
+     then repeat $ mono_aux dir
+     else mono_aux dir,
    gs ← get_goals,
    set_goals $ hyps ++ gs
 

test/monotonicity/test_cases.lean

@@ -78,3 +78,13 @@ do test_pp "test1"
    test_pp "test3"
            "([3] ++ [2], ([5] ++ [4], ([], append (some [1]) _ (some [2]))))"
            (parse_mono_function' ``([1] ++ [3] ++ [2] ++ [2]) ``([1] ++ [5] ++ ([4] ++ [2])))
+
+@[mono]
+lemma test {α : Type*} [preorder α] : monotone (id : α → α) :=
+λ x y h, h
+
+example : id 0 ≤ id 1 :=
+begin
+  mono,
+  simp,
+end