rw only simplifies if piped through my own function

Stream: new members

[Tobias Grosser]

My first beginners question. I tampered with this since a while, but maybe somebody has a quick explanation for this:

https://gist.github.com/tobig/92b17c8cac76fd07e1537c9131a25260

[Tobias Grosser]

Rewriting with my own theorem works well, but if I directly use imp_iff_not_or things break

[Tobias Grosser]

with "function expected at"

[Tobias Grosser]

Probably a beginners mistake. It seems my declaration introduces some additional information which help the proof go through.

[Simon Hudon]

If you check the definition of imp_iff_not_or, (type #check imp_iff_not_or in your Lean buffer), you see that it does not take explicit arguments, only implicit ones

[Simon Hudon]

That means that they are meant to be inferred. But if you want to specify then, you can write @imp_iff_not_or and then you have to provide an argument for the implicit and explicit arguments.

[Simon Hudon]

For reference:

#check imp_iff_not_or
-- imp_iff_not_or : ?M_1 → ?M_2 ↔ ¬?M_1 ∨ ?M_2
#check @imp_iff_not_or
-- imp_iff_not_or : ∀ {a b : Prop} [_inst_1 : decidable a], a → b ↔ ¬a ∨ b

The curly brackets around a and b means that they are implicit arguments. The square brackets around decidable a means that it's a type class instance.

[Tobias Grosser]

https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments

[Tobias Grosser]

Works flawless. Need to read a little bit more on this.

[Tobias Grosser]

Thanks for the quick help.

[Simon Hudon]

No worries :)

[Tobias Grosser]

One last question:

[Tobias Grosser]

My proof looks now like this:

[Tobias Grosser]

        ((B → C) → (¬(A → C)     ∧ ¬(A ∨ B)))
      = ((B → C) → (¬(¬A ∨ C)    ∧ ¬(A ∨ B)))         : by rw @imp_iff_not_or A C
  ... = ((B → C) → ((¬(¬A) ∧ ¬C) ∧ ¬(A ∨ B)))         : by rw not_or_distrib
  ... = ((B → C) → ((¬(¬A) ∧ ¬C) ∧ (¬A ∧ ¬B)))        : by rw not_or_distrib
  ... = ((B → C) → ((A ∧ ¬C) ∧ (¬A ∧ ¬B)))            : by rw not_not
  ... = ((B → C) → ((A ∧ ¬C) ∧ ¬A ∧ ¬B))              : by rw and_assoc
  ... = ((B → C) → ((¬C ∧ A) ∧ ¬A ∧ ¬B))              : by rw and_comm (A) (¬C)
  ... = ((B → C) → (¬C ∧ A ∧ ¬A ∧ ¬B))                : by rw and_assoc
  ... = ((B → C) → (¬C ∧ (A ∧ ¬A) ∧ ¬B))              : by rw and_assoc
  ... = ((B → C) → (¬C ∧ ¬ B ∧ (A ∧ ¬A)))             : by rw and_comm (¬ B) (A ∧ ¬A)
  ... = ((B → C) → (¬C ∧ ¬ B ∧ false ))               : by rw and_not_self_iff A
  ... = ((B → C) → ((¬C) ∧ false ))                   : by rw and_false
  ... = ((B → C) → (false))                           : by rw and_false
  ... = (¬(B → C) ∨ false)                            : by rw imp_iff_not_or
  ... = ¬(B → C)                                      : by rw or_false
  ... = ¬(¬B ∨ C)                                     : by rw imp_iff_not_or 
  ... = ((¬¬B) ∧ (¬C))                                : by rw not_or_distrib
  ... = (B ∧ ¬C)                                      : by rw not_not

[Tobias Grosser]

It seems only imp_iff_not_or needs the '@'. All other functions are OK with explicit arguments (if given).

[Tobias Grosser]

Is there some schema when theorems take explicit arguments in mathlib?

[Mario Carneiro]

most iff theorems have implicit args

[Kenny Lau]

rw ← imp_iff_not_or

[Kenny Lau]

import logic.basic

local attribute [instance] classical.prop_decidable

example {A B C : Prop} : _ = _ :=
calc
        ((B → C) → (¬(A → C)     ∧ ¬(A ∨ B)))
      = ((B → C) → (¬(¬A ∨ C)    ∧ ¬(A ∨ B)))         : by rw ← imp_iff_not_or
  ... = ((B → C) → ((¬(¬A) ∧ ¬C) ∧ ¬(A ∨ B)))         : by rw not_or_distrib
  ... = ((B → C) → ((¬(¬A) ∧ ¬C) ∧ (¬A ∧ ¬B)))        : by rw not_or_distrib
  ... = ((B → C) → ((A ∧ ¬C) ∧ (¬A ∧ ¬B)))            : by rw not_not
  ... = ((B → C) → ((A ∧ ¬C) ∧ ¬A ∧ ¬B))              : by rw and_assoc
  ... = ((B → C) → ((¬C ∧ A) ∧ ¬A ∧ ¬B))              : by rw and_comm (A) (¬C)
  ... = ((B → C) → (¬C ∧ A ∧ ¬A ∧ ¬B))                : by rw and_assoc
  ... = ((B → C) → (¬C ∧ (A ∧ ¬A) ∧ ¬B))              : by rw and_assoc
  ... = ((B → C) → (¬C ∧ ¬ B ∧ (A ∧ ¬A)))             : by rw and_comm (¬ B) (A ∧ ¬A)
  ... = ((B → C) → (¬C ∧ ¬ B ∧ false ))               : by rw and_not_self_iff A
  ... = ((B → C) → ((¬C) ∧ false ))                   : by rw and_false
  ... = ((B → C) → (false))                           : by rw and_false
  ... = (¬(B → C) ∨ false)                            : by rw imp_iff_not_or
  ... = ¬(B → C)                                      : by rw or_false
  ... = ¬(¬B ∨ C)                                     : by rw imp_iff_not_or
  ... = ((¬¬B) ∧ (¬C))                                : by rw not_or_distrib
  ... = (B ∧ ¬C)                                      : by rw not_not

[Tobias Grosser]

Is there a specific reason why 'iff' terms have implict arguments and others not?

[Kenny Lau]

import logic.basic

local attribute [instance] classical.prop_decidable

example {A B C : Prop} : _ = _ :=
calc
        ((B → C) → (¬(A → C) ∧ ¬(A ∨ B)))
      = ((B → C) → ((A ∧ ¬C) ∧ ¬(A ∨ B)))  : by rw not_imp
  ... = ((B → C) → ((A ∧ ¬C) ∧ ¬A ∧ ¬B))   : by rw not_or_distrib
  ... = ((B → C) → ((¬C ∧ A) ∧ ¬A ∧ ¬B))   : by rw and_comm (A) (¬C)
  ... = ((B → C) → (¬C ∧ A ∧ ¬A ∧ ¬B))     : by rw and_assoc
  ... = ((B → C) → (¬C ∧ (A ∧ ¬A) ∧ ¬B))   : by rw and_assoc
  ... = ((B → C) → (¬C ∧ ¬ B ∧ (A ∧ ¬A)))  : by rw and_comm (¬ B) (A ∧ ¬A)
  ... = ((B → C) → (¬C ∧ ¬ B ∧ false ))    : by rw and_not_self_iff A
  ... = ((B → C) → ((¬C) ∧ false ))        : by rw and_false
  ... = ((B → C) → (false))                : by rw and_false
  ... = ¬(B → C)                           : rfl
  ... = (B ∧ ¬C)                           : by rw not_imp

[Tobias Grosser]

Nice

[Tobias Grosser]

Really helpful.

[Tobias Grosser]

Thank you!

[Kenny Lau]

import logic.basic

local attribute [instance] classical.prop_decidable

example {A B C : Prop} : _ = _ :=
calc
        ((B → C) → (¬(A → C) ∧ ¬(A ∨ B)))
      = ((B → C) → ((A ∧ ¬C) ∧ ¬(A ∨ B)))  : by rw not_imp
  ... = ((B → C) → ((A ∧ ¬C) ∧ ¬A ∧ ¬B))   : by rw not_or_distrib
  ... = ((B → C) → ((A ∧ ¬A ∧ ¬B) ∧ ¬C))   : by rw and.right_comm
  ... = ((B → C) → (((A ∧ ¬A) ∧ ¬B) ∧ ¬C)) : by rw ← and_assoc
  ... = ((B → C) → ((false ∧ ¬B) ∧ ¬C))    : by rw and_not_self_iff A
  ... = ((B → C) → (false ∧ ¬C))           : by rw false_and
  ... = ((B → C) → (false))                : by rw false_and
  ... = ¬(B → C)                           : rfl
  ... = (B ∧ ¬C)                           : by rw not_imp

[Simon Hudon]

I'm a bit vague on the rule for iff and other rewrite rules but in general, if an argument can be inferred from other arguments, it should be implicit. For rewrite rules, I think all the arguments that can be inferred from the lhs of the equation should be implicit.

[Tobias Grosser]

I see. Thanks @Simon Hudon

[Mario Carneiro]

example {A B C : Prop} : ((B → C) → (¬(A → C) ∧ ¬(A ∨ B))) = (B ∧ ¬C) :=
by apply classical.cases_on A;
   apply classical.cases_on B;
   apply classical.cases_on C; simp

The idea behind the rule for iff is that these are more often used as combined unidirectional rules, and in this case any argument present on both lhs and rhs are inferrable

[Simon Hudon]

Have you tried tauto?

[Mario Carneiro]

doesn't seem to do anything

[Mario Carneiro]

propext $ by tauto works though

[Simon Hudon]

Right! You need the propositions to be decidable

[Kenny Lau]

example {A B C : Prop} : ((B → C) → (¬(A → C) ∧ ¬(A ∨ B))) = (B ∧ ¬C) :=
by apply classical.cases_on A;
apply classical.cases_on B;
apply classical.cases_on C; simp

that's the proof of completeness!

[Simon Hudon]

propext $ by tauto works though

Interesting! That should be worth adding to the tactic

[Mario Carneiro]

mathlib tries to avoid equality of propositions though

[Mario Carneiro]

it's always stated as an iff

[Kenny Lau]

example {A B C : Prop} : ((B → C) → (¬(A → C) ∧ ¬(A ∨ B))) = (B ∧ ¬C) :=
by by_cases A; by_cases B; by_cases C; simp*

[Mario Carneiro]

oh, of course - simp will rewrite A to true or false given the by_cases assumption

[Tobias Grosser]

Nice. I am currently translating some student exercises, so I try to use the 'calc' mode to really show step-by-step how things evolve.

[Tobias Grosser]

This worked quite well so far. Nice to see that the tactics work so well too.

[Mario Carneiro]

you should be able to use <-> in those calc blocks

[Tobias Grosser]

Yes, I can replace = with <->

[Tobias Grosser]

Does this have any benefits?

[Mario Carneiro]

only it's more idiomatic; rw and friends will work either way

[Tobias Grosser]

Why exactly is it more idiomatic?

[Mario Carneiro]

because it's easier to work with iff since you can destruct it, and you don't need the propext axiom to prove things about it

[Simon Hudon]

= has stronger precedence than <-> and the other connectives so <-> yields formulas with fewer brackets

[Tobias Grosser]

Great.

[Tobias Grosser]

Need to get back to normal life. Thanks for your help.

[Mario Carneiro]

But "idiomatic" really just means that it is used, like a convention - it doesn't need a reason per se, it's valuable because it is the convention

[Mario Carneiro]

i.e. it will make it easier to fit with and apply existing theorems

[Tobias Grosser]

I understand the meaning of idiomatic.

[Tobias Grosser]

Wanted understand the underlying motivation.

[Mario Carneiro]

so another answer is "there are two options, we picked one"

[Tobias Grosser]

If I want my proofs to be understood in the end, it helps to learn the choices you as a community have taken.

[Mario Carneiro]

I think logic textbooks usually use <->

[Mario Carneiro]

or sometimes ≡

[Tobias Grosser]

I can learn them easier if I can get an intuition where things come from.

[Keeley Hoek]

Cool fact: rewrite_search solves this problem instantly:

local attribute [search] imp_iff_not_or not_or_distrib not_not and_assoc and_comm and_not_self_iff and_false not_not

example {A B C : Prop} : ((B → C) → (¬(A → C) ∧ ¬(A ∨ B))) = (B ∧ ¬C) :=
  by rewrite_search_using [`search]

[Scott Morrison]

We really need to think about automatic lemma selection for rewrite_search.

[Scott Morrison]

Possible just finer attribute tagging (e.g. [search logic], [search list], [search category_theory]).

[Scott Morrison]

Perhaps even teach rewrite_search to automatically select from different bundles of lemmas depending on what it sees in the goal.

[Keeley Hoek]

At least for me, just printing out every definition in a modest real-ish maths environment takes 30 seconds, so I think some form of bundling will have to be the way to go. Maybe barring some emergency "show me the way" mode.

[Keeley Hoek]

Though "find me a lemma" mode could be a useful tactic in its own right I suppose

[Keeley Hoek]

I guess that's what I'll try next

[Patrick Massot]

We really need to think about automatic lemma selection for rewrite_search.

This is all very nice, but don't forget that this is a whole research area. So don't expect this to be super easy, and maybe have a look at what already exists. I think the keyword is "relevance filter"