ToDual.lean

module

public import Mathlib.Order.Defs.PartialOrder
public import Mathlib.Order.Notation
public import Mathlib.Tactic.ToAdditive

@[expose] public section

variable {α : Type} [PartialOrder α] (a b c : α)

-- test that we can translate between structures, reordering the arguments of the fields
class SemilatticeInf (α : Type) extends PartialOrder α, Min α where
  le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c

class SemilatticeSup (α : Type) extends PartialOrder α, Max α where
  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c

attribute [to_dual] SemilatticeInf
-- The `reorder` argument is automatically inferred here:
attribute [to_dual existing] SemilatticeSup.sup_le SemilatticeInf.mk

@[to_dual]
lemma SemilatticeInf.le_inf' {α : Type} [SemilatticeInf α] (a b c : α) : a ≤ b → a ≤ c → a ≤ b ⊓ c :=
  SemilatticeInf.le_inf a b c

@[to_dual]
lemma SemilatticeSup.sup_le' {α : Type} [SemilatticeSup α] (a b c : α) : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
  SemilatticeSup.sup_le a b c

structure Lattice (α : Type) extends SemilatticeInf α, SemilatticeSup α

attribute [to_dual existing] Lattice.toSemilatticeInf

-- we can reorder arguments of arguments in `SemilatticeInf.mk`
@[to_dual]
instance [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
  le_inf

-- we can reorder arguments of arguments of arguments in `SemilatticeInf.casesOn`
attribute [to_dual existing] SemilatticeSup.casesOn
@[to_dual]
theorem SemilatticeSup.ext {α} {A B : SemilatticeSup α}
    (my_sorry : ∀ {p : Prop}, p) :
    A = B := by
  cases A
  cases B
  exact my_sorry

-- we can reorder arguments of arguments of arguments even when not using `to_dual existing/self`
@[to_dual (reorder := t mk, mk (1 2, sup_le (a b)))]
def SemilatticeSup.casesOn' {α} {motive : SemilatticeSup α → Sort*} (t : SemilatticeSup α)
    (mk : [PartialOrder α] → [Max α] →
      (sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c) → motive { sup_le }) :
    motive t :=
  t.casesOn mk

/--
info: SemilatticeInf.casesOn'.{u_1} {α : Type} {motive : SemilatticeInf α → Sort u_1}
  (mk :
    [inst : Min α] →
      [inst_1 : PartialOrder α] →
        (sup_le : ∀ (b a c : α), c ≤ a → c ≤ b → c ≤ a ⊓ b) →
          motive { toPartialOrder := inst_1, toMin := inst, le_inf := ⋯ })
  (t : SemilatticeInf α) : motive t
-/
#guard_msgs in
#check SemilatticeInf.casesOn'

class Semilattice (α : Type) extends SemilatticeInf α, SemilatticeSup α
attribute [to_dual existing] Semilattice.toSemilatticeSup

-- when reordering arguments in arguments that are being reordered,
-- there is a convenient syntax to specify this at the same time:
@[to_dual self (reorder := h₁ h₂ (a b))]
def SemilatticeSup.foo {α} [Semilattice α]
    (h₁ : ∀ a b : α, a ⊔ b ≤ b) (h₂ : ∀ a b : α, a ≤ b ⊓ a) (my_sorry : ∀ {p : Prop}, p) : False :=
  (my_sorry : _ → _ → _) h₁ h₂


-- If the given `reorder` is the same as the autogenerated one, we get a linter warning:
/--
warning: `to_dual` correctly autogenerated `(reorder := 3 4)` for le_imp_le.
You may remove the `(reorder := 3 4)` argument.

Note: This linter can be disabled with `set_option linter.translateReorder false`
-/
#guard_msgs in
@[to_dual self (reorder := a b)]
theorem le_imp_le : a ≤ b → a ≤ b := id

-- The comparison on `reorder`s can see that `a b` is the same as `b a`:
/--
warning: `to_dual` correctly autogenerated `(reorder := 3 4)` for le_imp_le'.
You may remove the `(reorder := 4 3)` argument.

Note: This linter can be disabled with `set_option linter.translateReorder false`
-/
#guard_msgs in
@[to_dual self (reorder := b a)]
theorem le_imp_le' : a ≤ b → a ≤ b := id

-- And it can see that `6 (x y), 5 (x y)` is `5 (x y), 6 (x y)`
/--
warning: `to_dual` correctly autogenerated `(reorder := 3 4, 5 (1 2), 6 (1 2))` for le_imp_le_of_forall.
You may remove the `(reorder := 3 4, 5 (1 2), 6 (1 2))` argument.

Note: This linter can be disabled with `set_option linter.translateReorder false`
-/
#guard_msgs in
@[to_dual self (reorder := a b, 6 (x y), 5 (x y))]
theorem le_imp_le_of_forall (_ : ∀ x y : α, x ≤ y) (_ : ∀ x y : α, x ≤ y) : a ≤ b → a ≤ b := id

-- It is possible to overwrite the autogenerated `reorder`:
/--
error: `to_dual` validation failed: expected
  ∀ {α : Type} (a : α) [inst : PartialOrder α] (b : α), b ≤ a → b ≤ a
but 'le_imp_le''' has type
  ∀ {α : Type} [inst : PartialOrder α] (a b : α), a ≤ b → a ≤ b
-/
#guard_msgs in
@[to_dual self (reorder := 2 3)]
theorem le_imp_le'' : a ≤ b → a ≤ b := id

-- We can even overwrite it with the empty `reorder`:
/--
warning: `to_dual self` is redundant when none of the arguments are reordered.
Please remove the attribute, or provide an explicit `(reorder := ...)` argument.
If you need to give a hint to `to_dual` to translate expressions involving `le_imp_le'''`,
use `to_dual_do_translate` instead

Note: This linter can be disabled with `set_option linter.translateRedundant false`
---
error: `to_dual` validation failed: expected
  ∀ {α : Type} [inst : PartialOrder α] (a b : α), b ≤ a → b ≤ a
but 'le_imp_le'''' has type
  ∀ {α : Type} [inst : PartialOrder α] (a b : α), a ≤ b → a ≤ b
-/
#guard_msgs in
@[to_dual self (reorder := )]
theorem le_imp_le''' : a ≤ b → a ≤ b := id

-- Test a larger permutation:

theorem refl₁ (a b c d e : Nat) : a + b + c + d + e = a + b + c + d + e := rfl

@[to_dual existing refl₁]
theorem refl₂ (b c a e d : Nat) : a + b + c + d + e = a + b + c + d + e := rfl

-- Test that we do not translate numerals like we do in `@[to_additive]`
/--
warning: `to_dual self` is redundant when none of the arguments are reordered.
Please remove the attribute, or provide an explicit `(reorder := ...)` argument.
If you need to give a hint to `to_dual` to translate expressions involving `one_le_one`,
use `to_dual_do_translate` instead

Note: This linter can be disabled with `set_option linter.translateRedundant false`
-/
#guard_msgs in
@[to_dual self]
theorem one_le_one [One α] : (1 : α) ≤ 1 := le_rfl

-- Test the name generated by `to_dual none`
@[to_dual none]
theorem bot_eq_top {α : Type} [Bot α] [Top α] : (⊤ : α) = ⊥ → (⊤ : α) = ⊥ := id

/-- info: bot_eq_top._to_dual_1 {α : Type} [Top α] [Bot α] : ⊥ = ⊤ → ⊥ = ⊤ -/
#guard_msgs in
#check bot_eq_top._to_dual_1

/- Test the translation of auxLemmas.
`_proof_i` lemmas are translated, but `_simp_i` lemmas are unfolded. -/
@[to_dual lt_le_trans]
theorem le_lt_trans (h₁ : a ≤ b) (h₂ : b < c) : a < c := by
  grind

theorem le_refl': ∀ a : α, a ≤ a := by
  simp

/--
info: fun {α} [PartialOrder α] a b c h₁ h₂ => lt_le_trans._proof_1_1 a b c h₁ h₂
---
info: fun {α} [PartialOrder α] => of_eq_true (Eq.trans (forall_congr fun a => Std.le_refl._simp_1 a) (implies_true α))
-/
#guard_msgs in
run_meta
  Lean.logInfo ((← Lean.getConstInfo ``lt_le_trans).value! (allowOpaque := true))
  Lean.logInfo ((← Lean.getConstInfo ``le_refl').value! (allowOpaque := true))

-- Test that we do not translate the order on `Prop`
instance Prop.le : LE Prop :=
  ⟨(· → ·)⟩

@[to_dual le_of_imp']
theorem Prop.le_of_imp (_h : a ≤ b) {p q : Prop} : (p → q) → p ≤ q := id

-- Dualize `a ≤ b` but not `p ≤ q`
/--
info: «Prop».le_of_imp' {α : Type} [PartialOrder α] (a b : α) (_h : b ≤ a) {p q : Prop} : (p → q) → p ≤ q
-/
#guard_msgs in
#check Prop.le_of_imp'

/-! Test the `to_dual_insert_cast` framework. -/

@[to_dual lt_sum_eq_of_le']
def lt_sum_eq_of_le [DecidableLE α] {a b : α} (hab : a ≤ b) :
    a < b ⊕' a = b :=
  if hba : b ≤ a then PSum.inr (le_antisymm hab hba) else PSum.inl (lt_of_le_not_ge hab hba)

set_option warn.classDefReducibility false in
@[to_dual DecidableLE1_dual]
def DecidableLE1 (h : ∀ a b : α, Decidable (a ≤ b)) : DecidableLE α := fun a b ↦ h a b

set_option warn.classDefReducibility false in
@[to_dual DecidableLE2_dual]
def DecidableLE2 (h : ∀ a b : α, Decidable (a ≤ b)) : DecidableLE α := id h

-- Not yet supported because it probably won't show up in practice
-- (though it wouldn't be too hard to fix `unfoldConsts` to support this)
/--
error: @[to_dual] failed to insert a cast to make `fun {α} [PartialOrder α] h =>
  h` have type `{α : Type} → [inst : PartialOrder α] → DecidableLE α → (a b : α) → Decidable (a ≤ b)`

fun {α} [PartialOrder α] h =>
  h : {α : Type} →
  [inst : PartialOrder α] →
    DecidableLE α →
      DecidableLE
        α does not have type {α : Type} → [inst : PartialOrder α] → DecidableLE α → (a b : α) → Decidable (a ≤ b).
-/
#guard_msgs in
@[to_dual DecidableLE3_dual]
def DecidableLE3 (h : DecidableLE α) : ∀ a b : α, Decidable (a ≤ b) := h

@[to_dual DecidableLE4_dual]
def DecidableLE4 (h : DecidableLE α) (a b : α) : Decidable (a ≤ b) := h a b

-- The arguments to `h` have been introduced, and swapped:
/--
info: fun {α} [PartialOrder α] h a b => h b a
---
info: fun {α} [PartialOrder α] h => id fun a b => h b a
---
info: fun {α} [PartialOrder α] h a b => h b a
-/
#guard_msgs in
open Lean in
run_meta
  logInfo m!"{(← getConstInfo ``DecidableLE1_dual).value!}"
  logInfo m!"{(← getConstInfo ``DecidableLE2_dual).value!}"
  logInfo m!"{(← getConstInfo ``DecidableLE4_dual).value!}"

-- The arguments to `inst✝` have been swapped:
/--
info: @dite (a < b ⊕' a = b) (b ≤ a) (inst✝ b a) (fun hba => PSum.inr ⋯) fun hba => PSum.inl ⋯
---
info: @dite (b < a ⊕' a = b) (a ≤ b) (inst✝ a b) (fun hba => PSum.inr ⋯) fun hba => PSum.inl ⋯
-/
#guard_msgs in
open Lean Meta in
run_meta
  lambdaTelescope (← getConstInfo ``lt_sum_eq_of_le).value! fun _ => (logInfo m!"{·.setPPExplicit true}")
  lambdaTelescope (← getConstInfo ``lt_sum_eq_of_le').value! fun _ => (logInfo m!"{·.setPPExplicit true}")

/-- `Ico a b` is the left-closed right-open interval $[a, b)$. -/
def Cov.Ico (a b : α) := fun x ↦ a ⩿ x ∧ x ⋖ b

/-- `Ioc a b` is the left-open right-closed interval $(a, b]$. -/
@[to_dual existing (reorder := a b)]
def Cov.Ioc (a b : α) := fun x ↦ a ⋖ x ∧ x ⩿ b

to_dual_insert_cast Cov.Ico := by grind

@[to_dual]
theorem Cov.Ico_def {a b x : α} : (a ≤ x ∧ ∀ ⦃c⦄, a < c → ¬c < x) ∧ x ⋖ b ↔ Cov.Ico a b x := Iff.rfl

/--
info: theorem Cov.Ioc_def : ∀ {α : Type} [inst : PartialOrder α] {a b x : α},
  (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b ⋖ x ↔ Cov.Ioc b a x :=
@Eq.mpr (∀ {α : Type} [inst : PartialOrder α] {a b x : α}, (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b ⋖ x ↔ Cov.Ioc b a x)
  (∀ {α : Type} [inst : PartialOrder α] {a b x : α},
    ((x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b < x ∧ ∀ ⦃c : α⦄, c < x → ¬b < c) ↔
      (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b < x ∧ ∀ ⦃c : α⦄, c < x → ¬b < c)
  (id
    (forall_congr fun {α} =>
      forall_congr fun [PartialOrder α] =>
        forall_congr fun {a} =>
          forall_congr fun {b} =>
            forall_congr fun {x} =>
              congr (congrArg Iff (congrArg (And (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c)) (CovBy._to_dual_cast_4 x b)))
                (Eq.trans (Cov.Ico._to_dual_cast_4 a b x)
                  (congr (congrArg And (WCovBy._to_dual_cast_4 a x)) (CovBy._to_dual_cast_4 x b)))))
  (@Eq.mp
    (∀ {α : Type} [inst : PartialOrder α] {a b x : α},
      (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b ⋖ x ↔ (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b ⋖ x)
    (∀ {α : Type} [inst : PartialOrder α] {a b x : α},
      ((x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b < x ∧ ∀ ⦃c : α⦄, c < x → ¬b < c) ↔
        (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c) ∧ b < x ∧ ∀ ⦃c : α⦄, c < x → ¬b < c)
    (forall_congr fun {α} =>
      forall_congr fun [PartialOrder α] =>
        forall_congr fun {a} =>
          forall_congr fun {b} =>
            forall_congr fun {x} =>
              congr (congrArg Iff (congrArg (And (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c)) (CovBy._to_dual_cast_4 x b)))
                (congrArg (And (x ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬x < c)) (CovBy._to_dual_cast_4 x b)))
    fun {α} [PartialOrder α] {a b x} => Iff.rfl)
-/
#guard_msgs in
#print Cov.Ioc_def

/-! Test that translated autoparams are marked with `meta`. -/

@[to_dual]
def Top.autoParamTest {a b : α} (h : a ≤ b := by grind) : a ≤ b := h

open Lean
run_meta guard <| isDeclMeta (← getEnv) ``Bot.autoParamTest._auto_1

-- Test that hypotheses can also have a translation when using `to_dual_insert_cast`
@[to_dual self]
def nonemptyIcc {a b : α} (_ : a ≤ b) := fun x ↦ a ≤ x ∧ x ≤ b

to_dual_insert_cast nonemptyIcc := by grind

-- Test that we can translate `LE` instances correctly
inductive WithBot (α : Type u) where
  | bot : WithBot α
  | coe : α → WithBot α

@[to_dual existing]
inductive WithTop (α : Type u) where
  | top : WithTop α
  | coe : α → WithTop α

inductive WithBot.LE : WithBot α → WithBot α → Prop where
  | bot_le (x : WithBot α) : WithBot.LE .bot x
  | coe_le_coe {a b : α} : a ≤ b → WithBot.LE (.coe a) (.coe b)

@[to_dual existing (reorder := 3 4)]
inductive WithTop.LE : WithTop α → WithTop α → Prop where
  | le_top (x : WithTop α) : WithTop.LE x .top
  | coe_le_coe {a b : α} : a ≤ b → WithTop.LE (.coe a) (.coe b)

attribute [to_dual existing] WithTop.LE.le_top

@[to_dual]
instance WithBot.instLE : _root_.LE (WithBot α) := ⟨WithBot.LE⟩

example (a : α) : WithTop.coe a ≤ .top := .le_top (WithTop.coe a)

-- The namespace is translated correctly for private names:
@[to_dual]
private theorem WithBot.coe_le_top : WithTop.coe a ≤ .top := .le_top (WithTop.coe a)

run_meta guard <| (← getEnv).contains ``WithTop.coe_le_bot

@[to_dual]
private abbrev WithBotPrivate := WithBot

@[to_dual]
private theorem WithBotPrivate.coe_le_top : WithTop.coe a ≤ .top := .le_top (WithTop.coe a)

run_meta guard <| (← getEnv).contains ``WithTopPrivate.coe_le_bot

set_option linter.unusedVariables false in
@[to_dual (rename := x → y, Pbot ↔ Ptop) renameTest']
def renameTest [Top α] [Bot α] (x : α) {P : α → Prop} (Ptop : P ⊤) (Pbot : P ⊥) : True := trivial

/--
info: renameTest' {α : Type} [Bot α] [Top α] (y : α) {P : α → Prop} (Pbot : P ⊥) (Ptop : P ⊤) : True
-/
#guard_msgs in
#check renameTest'

-- Test translation of binder names starting with `h`: `hmax` turns into `hmin`.
@[to_dual]
theorem eq_of_min_of_max (hmax : ∀ x, x ≤ a) (hmin : ∀ x, a ≤ x) : a = b :=
  le_antisymm (hmin b) (hmax b)

/--
info: eq_of_max_of_min {α : Type} [PartialOrder α] (a b : α) (hmin : ∀ (x : α), a ≤ x) (hmax : ∀ (x : α), x ≤ a) : a = b
-/
#guard_msgs in
#check eq_of_max_of_min

-- Test that the heuristic applies even when proofs are beta expanded
@[to_dual (dont_translate := β) le_of_lt_and_le_of_lt']
theorem le_of_lt_and_le_of_lt {β} [Preorder β] (a b : α) (c d : β) : (a < b → a ≤ b) ∧ (c < d → c ≤ d) :=
  ⟨le_of_lt, (fun γ [Preorder γ] (c d : γ) ↦ @le_of_lt γ _ c d) β c d⟩