## Stream: general

### Topic: Monotonic connectives

#### Seul Baek (Apr 04 2019 at 23:24):

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 (Apr 04 2019 at 23:40):

tauto, tauto!, or finish

#### Mario Carneiro (Apr 04 2019 at 23:42):

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

#### Simon Hudon (Apr 04 2019 at 23:54):

confirmed: mono solves it

#### Seul Baek (Apr 04 2019 at 23:59):

@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 (Apr 05 2019 at 00:01):

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

#### Simon Hudon (Apr 05 2019 at 00:05):

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 (Apr 05 2019 at 00:07):

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

#### Simon Hudon (Apr 05 2019 at 00:12):

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

#### Seul Baek (Apr 05 2019 at 00:15):

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

Awesome :)

#### Jesse Michael Han (Apr 05 2019 at 02:38):

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

Last updated: May 13 2021 at 21:12 UTC