Monotonic connectives

Stream: general

[Seul Baek]

I keep running into goals of the form A → B, where A and B consist entirely of monotonic connectives and quantifiers (∨, ∧, ∀, ∃) and the implication A_i → B_i holds trivially for any pair (A_i, B_i) of corresponding subprops (e.g., h : s1 → s2 ⊢ (p ∧ q ∨ s1) → (p ∧ q ∨ s2)). Is there a standard way to deal with this kind of goals?

Here's what I'm using right now: https://github.com/skbaek/mathlib/blob/mono_con/src/tactic/mono_con.lean It works for my needs, but I'm wondering if there is a more principled approach.

[Chris Hughes]

tauto, tauto!, or finish

[Mario Carneiro]

in theory mono should do that, but I haven't checked how well it performs

[Simon Hudon]

confirmed: mono solves it

[Seul Baek]

@Chris Hughes Oops, I meant cases in which the implications between subprops are mostly trivial, such that you want to reduce the goal into proving implications between only the non-trivial ones. For instance, if the goal was

example (α : Type) (p q : Prop) (r1 r2 s1 s2 : α → Prop) :
  (∀ x : α, r1 x ∧ ∃ y : α, (p ∧ q ∨ s1 y)) →
  (∀ x : α, r2 x ∧ ∃ y : α, (p ∧ q ∨ s2 y))

then it'd be convenient to have a tactic that reduces it to r1 x → r2 x and s1 y → s2 y for arbitrary x and y. I don't think finish, safe, or tauto does it, although I may be using them incorrectly.

[Seul Baek]

@Simon Hudon Does it work with quantifiers? It'd solve all my problematic cases if it did

[Simon Hudon]

I think I have the code somewhere to make it work with quantifiers but I don't think it made it into mathlib

[Simon Hudon]

https://github.com/unitb/lean-lib/blob/master/src/util/meta/tactic/monotonicity/predicate.lean

[Simon Hudon]

If you feel like making a PR out of it, I'd love that

[Seul Baek]

Hmm, it looks like combining intro_mono with mono and adding an option for recursive application would give me what I want

[Simon Hudon]

Awesome :)

[Jesse Michael Han]

tauto! indeed solves the first example in your file, but annoyingly you have to manually instantiate some of the universal quantifiers in the second

example (p q r s1 s2 : Prop) (h : s1 → s2) :
  (p ∨ q ∧ (r ∨ s1)) → (p ∨ q ∧ (r ∨ s2)) :=
by tauto!

example (α : Type) (p1 p2 q1 q2 : Prop) (r1 r2 s1 s2 : α → Prop)
  (h1 : p1 → p2) (h2 : q1 → q2)
  (h3 : ∀ x, r1 x → r2 x) (h4 : ∀ x, s1 x → s2 x) :
  (∀ x : α, r1 x ∨ ∃ y : α, (p1 ∨ s1 y ∧ q1)) →
  (∀ x : α, r2 x ∨ ∃ y : α, (p2 ∨ s2 y ∧ q2)) :=
by {intros H x, specialize h3 x, specialize H x, safe; solve_by_elim}

this makes me appreciate mono more