Using rw and simp for theorems of my PSBP library

Stream: general

[Luc Duponcheel]

Hello all,

Thanks to Robin Arnez I am becoming more and more a
"proficient equality theorem prover", even up to the point
that writing theorems becomes "tedious" and I would like
Lean to take over the job for me.

I looked at the rw and simp documentation and looked at a few examples. So I tried to use rw and simp for my proofs but failed to
use them correctly.

I get messages similar to "simp could not proceed".

The code below contains the PSBP type classes,
corresponding "lawful" classes and a few theorems.
Especially the last theorem becomes very large and complex.
I also needed to add type annotations.

I would really appreciate if some member of the community
could get me started with rw and simp by replacing my
proofs by proofs using rw and simp similar to the
LawfulMonad proofs.

Thanks

By the way also using grind failed.

Thanks

Code listing

class Functional
    (program : Type → Type → Type) where
  asProgram {α β : Type} :
    (α → β) → program α β

export Functional (asProgram)

def first
    [Functional program] :
  program (α × β) α :=
    asProgram λ (α, _) => α

def second
    [Functional program] :
  program (α × β) β :=
    asProgram λ (_, β) => β

class Functorial
    (program : Type → Type → Type) where
  andThenF {α β γ : Type} :
    program α β → (β → γ) → program α γ

export Functorial (andThenF)

infixl:50 " >-> " => andThenF

class Creational
    (program : Type → Type → Type) where
  product {α β γ : Type} :
    program α β → program α γ → program α (β × γ)

export Creational (product)

infixl:60 " &&& " => product

class Sequential
    (program : Type → Type → Type) where
  andThen {α β γ : Type} :
    program α β → program β γ → program α γ

export Sequential (andThen)

infixl:50 " >=> " => andThen

def applyAtFirst
    [Functional program]
    [Creational program]
    [Sequential program] :
  program α β → program (α × γ) (β × γ) :=
    λ αpβ => (first >=> αpβ) &&& second

structure FromComputationValuedFunction
    (computation : (Type → Type)) (α β : Type) where
  toComputationValuedFunction : α → computation β

instance [Applicative computation] :
    Functional
      (FromComputationValuedFunction computation) where
  asProgram :=
    λ αfβ => ⟨λ α => pure $ αfβ α⟩

instance [Functor computation] :
    Functorial
      (FromComputationValuedFunction computation) where
  andThenF :=
    λ ⟨αfcβ⟩ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩

instance [Applicative computation] :
    Creational
      (FromComputationValuedFunction computation) where
  product := λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
    ⟨λ α => pure .mk <*> αfcβ α <*> αfcγ α⟩

instance [Monad computation] :
    Sequential
      (FromComputationValuedFunction computation) where
  andThen :=
    λ ⟨αfcβ⟩ ⟨βfcγ⟩ => ⟨λ α => αfcβ α >>= βfcγ⟩

class LawfulFunctional (program : Type → Type → Type)
    [Functional program]
    [Sequential program] : Prop where

  asProgram_sequential {α β γ : Type}
      (αfβ : α → β) (βfγ : β → γ) :
    (asProgram αfβ >=> asProgram βfγ : program α γ) =
      asProgram (βfγ ∘ αfβ)

class LawfulFunctorial (program : Type → Type → Type)
    [Functorial program] : Prop where
  andThenF_sequential
      (αpβ : program α β)
      (βfγ : β → γ)
      (γfδ : γ → δ) :
    (αpβ >-> βfγ >-> γfδ : program α δ) =
      (αpβ >-> (γfδ ∘ βfγ) : program α δ)

class LawfulCreational (program : Type → Type → Type)
    [Functional program]
    [Creational program]
    [Sequential program] : Prop where
  applyAtFirst_asProgram
    (αfβ : α → β) :
      (applyAtFirst (asProgram αfβ) : program (α × γ) (β × γ)) =
        asProgram (λ (α, γ) => (αfβ α, γ))

class LawfulSequential (program : Type → Type → Type)
    [Functional program]
    [Sequential program] : Prop where
  sequential_right_identity
    (αpβ : program α β) :
    (αpβ >=> identity : program α β) =
      αpβ
  sequential_left_identity
    (αpβ : program α β) :
    (identity >=> αpβ : program α β) =
      αpβ
  sequential_associativity
    (αpβ : program α β)
    (βpγ : program β γ)
    (γpδ : program γ δ) :
    ((αpβ >=> βpγ) >=> γpδ : program α δ) =
      (αpβ >=> (βpγ >=> γpδ))

@[simp] theorem functional_sequential_theorem
    {α β γ : Type}
    [Monad computation]
    [LawfulMonad computation]
  (αfβ : α → β)
  (βfγ : β → γ) :
    (asProgram αfβ >=> asProgram βfγ :
      FromComputationValuedFunction computation α γ)
  = asProgram (βfγ ∘ αfβ) := by
  calc
    (asProgram αfβ >=> asProgram βfγ :
      FromComputationValuedFunction computation α γ)
        = (⟨λ α => pure $ αfβ α⟩ >=> ⟨λ β => pure $ βfγ β⟩)
          := rfl
    _   = ⟨λ α => (pure $ αfβ α) >>= λ β => pure $ βfγ β⟩
          := rfl
    _   = ⟨λ α => pure $ βfγ (αfβ α)⟩
          := congrArg
               FromComputationValuedFunction.mk
               (funext λ α => pure_bind (αfβ α) (pure ∘ βfγ))
          -- := congrArg _ (funext λ _ => pure_bind _ _)
    _   = ⟨λ α => pure $ (βfγ ∘ αfβ) α⟩
          := rfl
    _   = asProgram (βfγ ∘ αfβ)
          := rfl

@[simp] theorem sequential_associative_theorem
    {α β γ δ : Type}
    [Monad computation]
    [LawfulMonad computation]
  (αpβ : FromComputationValuedFunction computation α β)
  (βpγ : FromComputationValuedFunction computation β γ)
  (γpδ : FromComputationValuedFunction computation γ δ) :
    ((αpβ >=> βpγ) >=> γpδ :
      FromComputationValuedFunction computation α δ) =
      (αpβ >=> (βpγ >=> γpδ) :
        FromComputationValuedFunction computation α δ) :=
  let αfcβ : α → computation β := αpβ.toComputationValuedFunction
  let βfcγ : β → computation γ := βpγ.toComputationValuedFunction
  let γfcδ : γ → computation δ := γpδ.toComputationValuedFunction
  let βfcδ : β → computation δ := λ β => βfcγ β >>= γfcδ
  calc
    ((⟨αfcβ⟩ >=> ⟨βfcγ⟩) >=> ⟨γfcδ⟩ :
      FromComputationValuedFunction computation α δ)
        = (⟨λ α => αfcβ α >>= βfcγ⟩ >=> ⟨γfcδ⟩)
          := rfl
    _   = ⟨λ α => αfcβ α >>= βfcγ >>= γfcδ⟩
          := rfl
    _   = ⟨λ α => αfcβ α >>= (λ β => βfcγ β >>= γfcδ)⟩
          := congrArg
               FromComputationValuedFunction.mk
               (funext λ α => bind_assoc (αfcβ α) βfcγ γfcδ)
          -- := congrArg _ (funext λ _ => bind_assoc _ _ _)
    _   = ⟨λ α => αfcβ α >>= βfcδ⟩
          := rfl

@[simp] theorem creational_applyFirstAt_asProgram_theorem
    {α β γ : Type}
    [Monad computation]
    [LawfulMonad computation]
  (αfβ : α → β) :
    (applyAtFirst (asProgram αfβ) :
      FromComputationValuedFunction computation (α × γ) (β × γ)) =
      (asProgram (λ (α, γ) => (αfβ α, γ))) :=
  calc
    (applyAtFirst (asProgram αfβ))
        = applyAtFirst ⟨λ α => pure $ αfβ α⟩ :=
        rfl
    _   = ((first : FromComputationValuedFunction computation (α × γ) α) >=>
            (⟨λ α => pure $ αfβ α⟩)) &&& second :=
        rfl
    _   = (((asProgram λ (α, _) => α) :
            FromComputationValuedFunction computation (α × γ) α) >=>
              (⟨λ α => pure $ αfβ α⟩)) &&& second :=
        rfl
    _   = ((⟨λ (α, _) => pure α⟩ :
            FromComputationValuedFunction computation (α × γ) α) >=>
              (⟨λ α => pure $ αfβ α⟩)) &&& second :=
        rfl
    _   = (⟨λ (α, _) => pure α >>= (λ α => pure $ αfβ α)⟩ :
            FromComputationValuedFunction computation (α × γ) β) &&& second :=
        rfl
    _   = (⟨(λ (α, _) => pure $ αfβ α)⟩ :
            FromComputationValuedFunction computation (α × γ) β) &&& second :=
        congrArg
          (λ (αfcβ : α → computation β) => ((⟨λ (α, _) => αfcβ α⟩ :
            FromComputationValuedFunction computation (α × γ) β) &&& second))
          (funext (λ α => pure_bind α (λ α => pure $ αfβ α)))
    _   = (⟨λ (α, _) => pure $ αfβ α⟩ :
            FromComputationValuedFunction computation (α × γ) β) &&& second :=
        rfl
    _   = (⟨λ (α, _) => pure $ αfβ α⟩ :
            FromComputationValuedFunction computation (α × γ) β) &&&
              (asProgram (λ (_, γ) => γ) :
                FromComputationValuedFunction computation (α × γ) γ) :=
        rfl
    _   = (⟨λ (α, _) => pure $ αfβ α⟩ :
            FromComputationValuedFunction computation (α × γ) β) &&&
              (⟨λ (_, γ) => pure $ γ⟩ :
                FromComputationValuedFunction computation (α × γ) γ) :=
        rfl
    _   = ⟨λ (α, γ) => (pure Prod.mk <*> (pure $ αfβ α)) <*> (pure $ γ)⟩ :=
        rfl
    _   = (⟨λ (α, γ) => (pure Prod.mk <*> (pure $ αfβ α)) <*> (pure $ γ)⟩) :=
        rfl
    _   = (⟨λ (α, γ) => (Prod.mk <$> (pure $ αfβ α)) <*> (pure $ γ)⟩ :
             FromComputationValuedFunction computation (α × γ) (β × γ)) :=
        congrArg
          (FromComputationValuedFunction.mk ∘
            ((λ αfcγfβaγ => λ (α, γ) => αfcγfβaγ α <*> (pure $ γ)) :
              (α → computation (γ → (β × γ))) → ((α × γ) → computation (β × γ))))
          (funext λ α => (pure_seq (Prod.mk) (pure $ αfβ α)))
    _   = (⟨λ (α, γ) => (pure $ Prod.mk (αfβ α)) <*> (pure $ γ)⟩ :
             FromComputationValuedFunction computation (α × γ) (β × γ)) :=
        congrArg
         (FromComputationValuedFunction.mk ∘
           ((λ αfβaγ => λ (α, γ) => αfβaγ α <*> (pure $ γ)) :
             (α → computation (γ → (β × γ))) → ((α × γ) → computation (β × γ))))
          (funext λ α => (map_pure (Prod.mk) (αfβ α)))
    _   = (⟨λ (α, γ) => Prod.mk (αfβ α) <$> (pure $ γ)⟩) :=
        congrArg
         FromComputationValuedFunction.mk
          (funext λ (α, γ) => (pure_seq (Prod.mk (αfβ α)) (pure $ γ)))
    _   = (⟨λ (α, γ) => pure (Prod.mk (αfβ α) γ)⟩) :=
        congrArg
         FromComputationValuedFunction.mk
          (funext λ (α, γ) => (map_pure (Prod.mk (αfβ α)) γ))
    _   = (⟨λ (α, γ) => pure $ (αfβ α, γ)⟩) :=
        rfl
    _   = (asProgram (λ (α, γ) => (αfβ α, γ))) :=
        rfl

[Robin Arnez]

The last proof can be replaced by simp [applyAtFirst, asProgram, product, first, second]. You need to tell it to unfold everything in order for it to see the real definitions.

[Robin Arnez]

Alternatively, you can unfold definitions entirely yourself and then let simp do the rest:

  change
    ⟨fun x : α × γ => pure Prod.mk <*> (pure x.fst >>= fun a => pure (αfβ a)) <*> pure x.snd⟩ =
    (⟨fun x : α × γ => pure (αfβ x.fst, x.snd)⟩ : FromComputationValuedFunction computation _ _)
  simp

[Kenny Lau]

alternatively you can mark those definitions as @[simp] to tell simp to always unfold those definitions

[Robin Arnez]

I don't that's the goal though in the same way you won't unfold + or >>= by default

[Luc Duponcheel]

OK, gonna give it a try, you're my hero, Robin!

[Luc Duponcheel]

Lean is an amazing system, and this community really rocks!

On the one hand I am glad that I could calculate complex proofs myself, but, let's face it, those manual proofs are complex "getting the types right puzzles" that a system like Lean should be able to do (and can do (!)) for us.

Note that I used "complex" (as opposed to "simple") and not "difficult" as opposed to "easy". Human beings can only deal with a limited amount of complexity. Very complex things can become difficult for us. Computers can deal with unlimited complexity (there are memory and CPU limitations). Our task is to let them deal with difficulty as well. Systems like Lean are a big step forwards in order to accomplish that task.

Thanks so much all of you!

[Luc Duponcheel]

You may wonder why I do this PSBP (Program Description Based Programming) project. Just like computations (monads) are effectful expression specifications, (what I call) programs are effectful function specifications. 32 years ago I worked on the fundaments of computations and computation transformers at the University of Utrecht. Computations (monads) are mainstream now in many programming language libraries. Now that I am retired, I think that programs are the way to go. Why? Well because computations (and expression) are operational artifacts, while programs (and functions) are denotational artifacts (they have a meaning and can be given a meaningful name). For example, the associativity law of computations is an operational law (and difficult to remember). The associativity law of programs is a denotational law (and easy to remember).