# Zulip Chat Archive

## 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

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

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