Converting lemmas to lemmas

Stream: general

[Damiano Testa]

Dear All,

I have been playing around a bit with the idea of auto-generating more lemmas in the style of to_additive. I have a very simple-minded implementation of a command that tries to autogenerate the statement of a lemma that is the "to_opposite" of a give one. (Note: it currently makes no attempt at proving the "opposite" statement, it just states it -- proofs would be a follow up!)

Here is a quick demo on docs#mul_le_mul_left:

-- the actual lemma in the library
theorem mul_le_mul_left [PosMulMono α] [PosMulMonoRev α] (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c := sorry
-- and the following one
theorem mul_le_mul_right [MulPosMono α] [MulPosMonoRev α] (a0 : 0 < a) : b * a ≤ c * a ↔ b ≤ c := sorry

With the command that I have been trying out, this is what you can do:

-- you state your lemma
theorem mul_le_mul_left [PosMulMono α] [PosMulMonoRev α] (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c := sorry
-- and maybe you prove it
-- then
rev mul_le_mul_left (0 * 0) α  -- this autogenerates
/-
@[reverse mul_le_mul_left]
lemma mul_le_mul_right : ∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α]
  [inst_3 : MulPosMono α] [inst_4 : MulPosMonoRev α], 0 < a → (b * a ≤ c * a ↔ b ≤ c) := by
  sorry
-/

The syntax of rev is as follows:

rev name operation type

where

• name is the name of the declaration;
• operation is the (binary) operation that you want to reverse;
• type is the Type on which the reversal should occur (i.e. rev looks for (operation : type → type → type) in the statement of name).

The idea is that the autogenerated lemma may in the future be proved automatically, but right now the attribute @[reverse decl] is supposed to maintain them in synch.

[Damiano Testa]

I know that this came up several times and that there are plenty of possible further developments, but I thought that maybe starting with something small, that simply suggests the "new" lemma statement might be a useful stepping stone for further improvement.

[Damiano Testa]

If there is interest in this, I can polish what I have a little and start a PR.