Zulip Chat Archive

Stream: general

Topic: Monotonic connectives


view this post on Zulip 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.

view this post on Zulip Chris Hughes (Apr 04 2019 at 23:40):

tauto, tauto!, or finish

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:42):

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

view this post on Zulip Simon Hudon (Apr 04 2019 at 23:54):

confirmed: mono solves it

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 05 2019 at 00:07):

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

view this post on Zulip Simon Hudon (Apr 05 2019 at 00:12):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 05 2019 at 00:18):

Awesome :)

view this post on Zulip 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