Help needed to write laws and theorems of my PSBP library

Stream: general

[Luc Duponcheel]

Hello folks,

I have a question about how to get started with
calculational proofs of laws of my PSBP library.

Below is minimal documented code that illustrates
what I want to do.

I know that there are tactics like simp to let
Lean do the details, but I first want to write
calculational proofs myself.

All comments are welcome.

Code listing

/-

two type classes specifying that

functions can, somehow, be used as programs
programs can be composed sequentially

-/

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

export Functional (asProgram)

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

export Sequential (andThen)

infixl:50 " >=> " => andThen

/-

two type class instances implementing the
specifications above as computation valued functions

functions can, somehow, be used as programs
programs can be composed sequentially

note the program composition order is
first left and then right,
while the function composition order is
right left and then left

... just a choice ...

-/

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

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

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

/-

type class specifying
the equational relationship between
sequential function composition and
sequential program composition

-/

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β)

/-

the code below illustrates
the calculational proof steps
of a theorem proving
law asProgram_sequential of LawfulFunctional
using pure_bind law of LawfulMonad
as a

I simply put the steps in a list

-/

def asList  {α β γ : Type}
    [Applicative computation]
    [Monad computation]
    [Functional (FromComputationValuedFunction computation)]
    [Sequential (FromComputationValuedFunction computation)]
    (αfβ : α → β) (βfγ : β → γ) :
  List (FromComputationValuedFunction computation α γ) :=
    [ asProgram αfβ >=> asProgram βfγ
    -- definition asProgram
    , ⟨λ α => pure $ αfβ α⟩ >=> ⟨λ β => pure $ βfγ β⟩
    -- definition >=>
    , ⟨λ α => (pure $ αfβ α) >>= λ β => pure $ βfγ β⟩
    -- pure_bind law of LawfulMonad
    , ⟨λ α => pure $ βfγ (αfβ α)⟩
    -- definition ∘
    , ⟨λ α => pure $ (βfγ ∘ αfβ) α⟩
    -- definition asProgram
    , asProgram (βfγ ∘ αfβ)
    ]

theorem asProgram_sequential_theorem_1 {α β γ : Type}
   [Applicative computation]
   [Monad computation]
   [Functional (FromComputationValuedFunction computation)]
   [Sequential (FromComputationValuedFunction computation)]
   [LawfulFunctional (FromComputationValuedFunction computation)]
   (αfβ : α → β) (βfγ : β → γ) :
    (asProgram αfβ >=> asProgram βfγ :
      FromComputationValuedFunction computation α γ) =
      (asProgram (βfγ ∘ αfβ) :
        FromComputationValuedFunction computation α γ) :=
        let left : FromComputationValuedFunction computation α γ :=
          asProgram αfβ >=> asProgram βfγ
        let right : FromComputationValuedFunction computation α γ :=
          left = right
        -- calc
        --   left = (⟨λ α => pure $ αfβ α⟩ >=> ⟨λ β => pure $ βfγ β⟩) := rfl
        --   _    = ⟨λ α => (pure $ αfβ α) >>= λ β => pure $ βfγ β⟩   := rfl
        --   _    = ⟨λ α => pure $ βfγ (αfβ α)⟩                       := pure_bind
        --   _    = ⟨λ α => pure $ ((βfγ ∘ αfβ) α)⟩                   := rfl
        --   _    = right                                             := rfl

[Robin Arnez]

The proof would like this:

theorem asProgram_sequential_theorem_1 {α β γ : Type}
    [Monad computation] [LawfulMonad computation]
    (αfβ : α → β) (βfγ : β → γ) :
    (asProgram αfβ >=> asProgram βfγ :
      FromComputationValuedFunction computation α γ) =
      (asProgram (βfγ ∘ αfβ) :
        FromComputationValuedFunction computation α γ) :=
  let left : FromComputationValuedFunction computation α γ :=
    asProgram αfβ >=> asProgram βfγ
  let right : FromComputationValuedFunction computation α γ :=
    asProgram (βfγ ∘ αfβ)
  calc
    left = (⟨λ α => pure $ αfβ α⟩ >=> ⟨λ β => pure $ βfγ β⟩) := rfl
    _    = ⟨λ α => (pure $ αfβ α) >>= λ β => pure $ βfγ β⟩   := rfl
    _    = ⟨λ α => pure $ βfγ (αfβ α)⟩                       := congrArg _ <| funext fun _ => pure_bind _ _
    _    = ⟨λ α => pure $ ((βfγ ∘ αfβ) α)⟩                   := rfl
    _    = right                                             := rfl

Note:

[Applicative computation]
[Functional (FromComputationValuedFunction computation)]
[Sequential (FromComputationValuedFunction computation)]

can already be determined from Monad computation so you basically declare 3 instances that might be completely different from the implementations above (so you'd have to prove "this works for any exotic Functional (FromComputationValuedFunction computation) instance" which would be false).
Also, you need to specify [LawfulMonad computation] to get pure_bind. The actual application of pure_bind gets a bit more complicated then but you can basically use congrArg to go inside of the ⟨...⟩ and funext to go into the λ α => ...

[Luc Duponcheel]

Robin, thanks for the reply, gonna try it out asap (gonna first do some race bycicle cycling (good weather)). Of course, already knew that Monad computation implied Applicative computation. Without any [...]'s, Lean suggested me Functional (FromComputationValuedFunction computation) and I simply forgot to remove them afterwards, sorry.

[Luc Duponcheel]

Robin, about congrArg, and funext, ok, that was the thing I was wondering how to do. I knew about congrArg (but >=> is an operation with 2 arguments, not 1, therefore the extra underscore _ I suppose ), but I did not know about funext (and how to glue everything together).

Thanks so much, now I can start with all the laws of my PSBP library!

(but first some :cyclist:)

Cool

[Robin Arnez]

To be precise, it's congrArg FromComputationValuedFunction.mk _ here which turns a = b into FromComputationValuedFunction.mk a = FromComputationValuedFunction.mk b (i.e. ⟨a⟩ = ⟨b⟩) and then funext turns ∀ a, x[a] = y[a] into (λ a, x[a]) = λ a, y[a]