porting logic.basic

Stream: mathlib4

[Scott Morrison]

Remember to curb your enthusiasm a little here: part of the point of asking for help porting theories is so that we can prioritize which tactics need porting. That is, we are fully expecting to quickly run into problems where a file can't / shouldn't be ported yet, and will have to wait on tactic development.

[Scott Morrison]

To be a little more concrete about what needs to happen with Logic.Basic, I would recommend someone tries the following:

• Open Logic.Basic in mathlib3port
• Copy and paste that to the bottom of Logic.Basic in mathlib4 (i.e. contrary to my suggestion for most existing files, which is that you just nuke the existing file).
• Now go through the material you just pasted in.
  • Hopefully most declarations will be flagged as errors because they already exist. Just delete them.
  • Fix up any errors in other declarations.
  • Do a manual pass looking for duplications with changed names.
  • Add any #align statements needed corresponding to thoses changes.
  • Reorder as appropriate to bring some semblance of order to the file.

[Mario Carneiro]

regarding "reorder as appropriate", I think we want to order the declarations in the same order as they appear in the mathlib file, unless this is impossible due to e.g. a different proof. That will minimize future diffs

[Scott Morrison]

I've had an initial attempt at porting logic.basic, by taking the output from mathport and deleting everything that already existed, then merging that with the current mathlib4 Logic.Basic.

[Scott Morrison]

I finished merging in that sense, but I left a bunch of errors in the mathport output, and may not get back to it immediately.

[Scott Morrison]

If someone would like to take over the mathlib4 branch logic_basic, I think that "just fixing all the errors" should suffice for reach a complete port now.

[Scott Morrison]

Two reasons to get this out of the way:

• it's at the root of all our (non-tactic) import trees, so blocking almost everything
• it's more complicated than most other things, because it contains a partial port of the mathlib3 content, but so does Std4

[Jakob von Raumer]

I'll have a look now

[Jakob von Raumer]

This hinges on Tactic.Symm to be implemented or at least the [symm] attribute being present. Should I maybe add a placeholder for attribute at least?

[Jakob von Raumer]

I noticed that some lemmas in Init which we previously stated as iffs are now stated in terms of equality. Do we know what the reasoning behind the change is?

[Mario Carneiro]

it's simpler for simp

[Mario Carneiro]

they should be considered as internal lemmas for simp

[Eric Rodriguez]

lol we just changed this in mathlib3

[Eric Rodriguez]

they were originally equalities and because dsimp in lean3 can now deal with iffs they were changed with iff

[Jakob von Raumer]

Okay, so we'll maybe use those and apply whatever the inverse of propext is called

[Mario Carneiro]

The plan is still to use iff where possible in mathlib. Leo has stated he is okay with renaming the lemmas in Init if they get in the way

[Jakob von Raumer]

Okay

[Jakob von Raumer]

What is the general plan for things that are missing or different in Init? I worked around some of them in logic.basic, but that's maybe not a good solution since they'll still be missing down the line, so maybe adding them directly to logic.basic or to Std.Logic might be an option?

[Jakob von Raumer]

I added some more notes to Logic.Basic

[Mario Carneiro]

Don't rewrite proofs to work around missing theorems if possible

[Mario Carneiro]

just add the missing theorems

[Mario Carneiro]

Renames are okay, use #align to tell mathport the new name

[Jakob von Raumer]

Is it okay if I add them to mathlib4 for now, and you'd elevate them to std4 later?

[Mario Carneiro]

yes

[Mario Carneiro]

they should already exist in std, do you have a specific list of theorems?

[Jakob von Raumer]

eq_true_intro, eq_true_false for example

[Mario Carneiro]

eq_true_intro is eq_true now

[Jakob von Raumer]

Added it to the align file

[Jakob von Raumer]

Mario Carneiro said:

The plan is still to use iff where possible in mathlib. Leo has stated he is okay with renaming the lemmas in Init if they get in the way

congr now only takes equalities, is that due to change?

[Mario Carneiro]

the attribute or the tactic?

[Jakob von Raumer]

The attribute foremost

[Mario Carneiro]

I think it is more likely that the tactic will change to allow <-> than the attribute

[Mario Carneiro]

the attribute is only used rarely anyway

[Jakob von Raumer]

What's missing from logic.basic is now:

• Some errors on [elabAsElim] attributes
• Errors on iff-valued [congr] attributes
• Three proofs where simp leaves goes by not replacing using h : P to replace P by True in the goal

[Mario Carneiro]

just comment out the broken attributes for now

[Mario Carneiro]

I don't understand the third category, can you give an example?

[Jakob von Raumer]

theorem dite_eq_iff : dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c := by
  by_cases P <;> simp [*, exists_prop_of_false not_false]

[Mario Carneiro]

ah, can you mwe that? I don't have exists_prop_of_false

[Jakob von Raumer]

This is self contained:

theorem foo {p : Prop} {q : p → Prop} : ¬p → ¬∃ h' : p, q h' :=
  mt Exists.fst

theorem dite_eq_iff : dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c := by
  by_cases P <;> simp [*, foo not_false]

[Scott Morrison]

I put in term mode proofs for the three places simp is not finishing, so at least the branch builds now.

[Scott Morrison]

I've put this up at https://github.com/leanprover-community/mathlib4/pull/484 to hear from the linter.

[Jakob von Raumer]

Scott Morrison said:

I put in term mode proofs for the three places simp is not finishing, so at least the branch builds now.

Might still be good to investigate what the simplifier fails to do there /cc @Sebastian Ullrich

[Sebastian Ullrich]

Could you report an mwe as a lean4 issue?

[Jakob von Raumer]

Scott Morrison said:

I've put this up at https://github.com/leanprover-community/mathlib4/pull/484 to hear from the linter.

Linter says

#check forall_forall_const.{u_2 u_1} /- simp can prove this:
  by simp only [forall_const]
One of the lemmas above could be a duplicate.

but for some reason, simp only [forall_const] does not suffice for me, but I have to put in iff_self :thinking:

[Jakob von Raumer]

@Sebastian Ullrich https://github.com/leanprover/lean4/issues/1762

[Sebastian Ullrich]

[Meta.Tactic.simp.discharge] h1, failed to discharge hypotheses ∀ (h : P), A h ↔ ?q' h

I'm not surprised it refuses to instantiate that metavariable. I vaguely recall a previous thread/issue on this.

[Jakob von Raumer]

It's not super important to have that I guess. If it's only an issue when having an existential quantification over a Prop, it's not going to be super common...

[Sebastian Ullrich]

The output looks the same at https://leanprover-community.github.io/lean-web-editor/#code=example%20%28P%20%3A%20Prop%29%20%28h%20%3A%20P%29%20%28A%20%3A%20P%20%E2%86%92%20Prop%29%0A%20%20%28h1%20%3A%20%E2%88%80%7Bp%20p'%20%3A%20Prop%7D%20%7Bq%20q'%20%3A%20p%20%E2%86%92%20Prop%7D%0A%20%20%20%20%28hq%20%3A%20%E2%88%80%20h%2C%20q%20h%20%E2%86%94%20q'%20h%29%20%28hp%20%3A%20p%20%E2%86%94%20p'%29%2C%20Exists%20q%20%3D%20%E2%88%83%20h%20%3A%20p'%2C%20q'%20%28hp.2%20h%29%29%0A%20%20%28h2%20%3A%20%E2%88%80%28p%20%3A%20true%20%E2%86%92%20Prop%29%2C%20%28%E2%88%83%20x%2C%20p%20x%29%20%E2%86%94%20p%20true.intro%29%20%3A%20%E2%88%83%20%28h%20%3A%20P%29%2C%20A%20h%20%3A%3D%20by%0A%20%20simp%20only%20%5Bh%2C%20h1%2C%20h2%5D%0A

[Jakob von Raumer]

Uh, I edited the MWE to boil it down a bit more

[Jakob von Raumer]

But yea, that's weird

[Jakob von Raumer]

Oh, importing logic.basic changes it

[Jakob von Raumer]

Okay, I think I'm on it. congr lemmas are used silently by simp, and exists_prop_congr' is congr

[Jakob von Raumer]

Yes, in the end it boils down to the issue that iff-lemmas can't be congr lemmas right now in Lean 4

[Jakob von Raumer]

Made a new issue: https://github.com/leanprover/lean4/issues/1763