lean-pipes: could someone help me finish?

Stream: lean4

[Serhii Khoma (srghma)]

hi, everyone. I have almost finished porting https://github.com/jwiegley/coq-pipes to lean

https://github.com/srhhma/lean-pipes/blob/main/Pipes/Basic.lean

Could someone help me?

How to prove that pushR terminates? (NOTE: pullR is similar)

TODO also (I think I can learn how to do it (with effort), but if someone wants to do it instead of me or give some advise - I will be very thankful):

1. prove categories
2. fill sorries

[Mario Carneiro]

inductive ProxyPushRWF (a' a b' b c' c m r) where
  | go : (b' → Proxy a' a b' b m r) → Proxy b' b c' c m r → ProxyPushRWF a' a b' b c' c m r
  | reg : Proxy a' a b' b m r → ProxyPushRWF a' a b' b c' c m r

inductive ProxyPushRWFRel :
    ProxyPushRWF a' a b' b c' c m r → ProxyPushRWF a' a b' b c' c m r → Prop where
  | go_request : ProxyPushRWFRel (.reg (k xb')) (.go k (.Request xb' _kb))
  | go_respond : ProxyPushRWFRel (.go k (kc' yc)) (.go k (.Respond xc kc'))
  | go_m : ProxyPushRWFRel (.go k (kx x)) (.go k (.M mx kx))
  | request : ProxyPushRWFRel (.reg (k a)) (.reg (.Request xa' k))
  | m : ProxyPushRWFRel (.reg (k x)) (.reg (.M mx k))
  | respond : ProxyPushRWFRel (.go k t) (.reg (.Respond xb k))

instance : WellFoundedRelation (ProxyPushRWF a' a b' b c' c m r) where
  rel := ProxyPushRWFRel
  wf := by
    refine ⟨fun p => ?_⟩
    have H1 (x k) (hk : ∀ y, Acc ProxyPushRWFRel (.reg (k y) : ProxyPushRWF a' a b' b c' c m r)) :
        Acc ProxyPushRWFRel (.go k x : ProxyPushRWF a' a b' b c' c m r) := by
      induction x with
      | Request => exact ⟨_, fun | _, .go_request => hk _⟩
      | Respond _ _ ih => exact ⟨_, fun | _, .go_respond => ih _⟩
      | M _ _ ih => exact ⟨_, fun | _, .go_m => ih _⟩
      | Pure => exact ⟨_, nofun⟩
    have H2 (x) : Acc ProxyPushRWFRel (.reg x : ProxyPushRWF a' a b' b c' c m r) := by
      induction x with
      | Request _ _ ih => exact ⟨_, fun | _, .request => ih _⟩
      | Respond _ _ ih => exact ⟨_, fun | _, .respond => H1 _ _ ih⟩
      | M _ _ ih => exact ⟨_, fun | _, .m => ih _⟩
      | Pure => exact ⟨_, nofun⟩
    cases p with
    | reg => exact H2 _
    | go => exact H1 _ _ (fun _ => H2 _)

mutual
  @[inline] def Proxy.pushR.go' [Inhabited r]
    (fb : b → Proxy b' b c' c m r)
    (k : b' → Proxy a' a b' b m r)
    (p : Proxy b' b c' c m r)
    : Proxy a' a c' c m r :=
    match p with
    | .Request xb' _kb => Proxy.pushR fb (k xb')
    | .Respond xc kc' => .Respond xc (fun c' => Proxy.pushR.go' fb k (kc' c'))
    | .M mx kx => .M mx (fun x => Proxy.pushR.go' fb k (kx x))
    | .Pure xr => .Pure xr
    termination_by ProxyPushRWF.go k p
    decreasing_by all_goals constructor

  @[inline] def Proxy.pushR [Inhabited r]
    (fb : b → Proxy b' b c' c m r)
    (p0 : Proxy a' a b' b m r) :
    Proxy a' a c' c m r :=
    match p0 with
    | .Request xa' k => .Request xa' (fun a => Proxy.pushR fb (k a))
    | .Respond xb k => Proxy.pushR.go' fb k (fb xb)
    | .M mx k => .M mx (fun x => Proxy.pushR fb (k x))
    | .Pure xr => .Pure xr
    termination_by (.reg p0 : ProxyPushRWF a' a b' b c' c m r)
    decreasing_by all_goals constructor
end

[Mario Carneiro]

and pull is indeed similar

inductive ProxyPullRWF (a' a b' b c' c m r) where
  | go : (b → Proxy b' b c' c m r) → Proxy a' a b' b m r → ProxyPullRWF a' a b' b c' c m r
  | reg : Proxy b' b c' c m r → ProxyPullRWF a' a b' b c' c m r

inductive ProxyPullRWFRel :
    ProxyPullRWF a' a b' b c' c m r → ProxyPullRWF a' a b' b c' c m r → Prop where
  | go_request : ProxyPullRWFRel (.go k (kc' yc)) (.go k (.Request xc kc'))
  | go_respond : ProxyPullRWFRel (.reg (k xb')) (.go k (.Respond xb' _kb))
  | go_m : ProxyPullRWFRel (.go k (kx x)) (.go k (.M mx kx))
  | request : ProxyPullRWFRel (.go k t) (.reg (.Request xb k))
  | respond : ProxyPullRWFRel (.reg (k a)) (.reg (.Respond xa' k))
  | m : ProxyPullRWFRel (.reg (k x)) (.reg (.M mx k))

instance : WellFoundedRelation (ProxyPullRWF a' a b' b c' c m r) where
  rel := ProxyPullRWFRel
  wf :=
    have H1 (x k) (hk : ∀ y, Acc ProxyPullRWFRel (.reg (k y) : ProxyPullRWF a' a b' b c' c m r)) :
        Acc ProxyPullRWFRel (.go k x : ProxyPullRWF a' a b' b c' c m r) := by
      induction x with
      | Respond => exact ⟨_, fun | _, .go_respond => hk _⟩
      | Request _ _ ih => exact ⟨_, fun | _, .go_request => ih _⟩
      | M _ _ ih => exact ⟨_, fun | _, .go_m => ih _⟩
      | Pure => exact ⟨_, nofun⟩
    have H2 (x) : Acc ProxyPullRWFRel (.reg x : ProxyPullRWF a' a b' b c' c m r) := by
      induction x with
      | Respond _ _ ih => exact ⟨_, fun | _, .respond => ih _⟩
      | Request _ _ ih => exact ⟨_, fun | _, .request => H1 _ _ ih⟩
      | M _ _ ih => exact ⟨_, fun | _, .m => ih _⟩
      | Pure => exact ⟨_, nofun⟩
    ⟨fun
      | .reg _ => H2 _
      | .go .. => H1 _ _ (fun _ => H2 _)⟩

mutual
  @[inline] def Proxy.pullR.go' [Inhabited r]
    (fb' : b' → Proxy a' a b' b m r)
    (k : b → Proxy b' b c' c m r)
    (p : Proxy a' a b' b m r) :
    Proxy a' a c' c m r :=
    match p with
    | .Request xa' ka => .Request xa' (fun a => Proxy.pullR.go' fb' k (ka a))
    | .Respond xb _kb' => (k xb).pullR fb'
    | .M mx kx => .M mx (fun x => Proxy.pullR.go' fb' k (kx x))
    | .Pure xr => .Pure xr
    termination_by ProxyPullRWF.go k p
    decreasing_by all_goals constructor

  @[inline] def Proxy.pullR [Inhabited r]
    (fb' : b' → Proxy a' a b' b m r)
    (p0 : Proxy b' b c' c m r) :
    Proxy a' a c' c m r :=
    match p0 with
    | .Request xb' k => Proxy.pullR.go' fb' k (fb' xb')
    | .Respond xc k => .Respond xc (fun c' => (k c').pullR fb')
    | .M mx k => .M mx (fun x => (k x).pullR fb')
    | .Pure xr => .Pure xr
    termination_by (.reg p0 : ProxyPullRWF a' a b' b c' c m r)
    decreasing_by all_goals constructor
end

[Serhii Khoma (srghma)]

@Mario Carneiro big big thank You, magician. Merged

---

I have also tried to do next

--- DISALLOWED NEXT
@[inline]
def Proxy.next
  [_root_.Pure m] [Bind m]
  (p : Producer a m r) :
  m (r ⊕ (a × (Producer a m r))) :=
  match p with
  | Proxy.Request v _  => False.elim v
  | Proxy.Respond a fu => pure (Sum.inr (a, fun _ => fu ()))
  | Proxy.M mx k => mx >>= fun x => Proxy.next (k x)
  | Proxy.Pure r => pure (Sum.inl r)

that coq accepts (interesting why? is coq unsafe?)

In lean it is disallowed bc Proxy ... is u+1 and I cannot put it in m : u

I have tried other different ideas

and my favorite is idea 3

inductive ProxyNextStep.{u} (b : Type u) (m : Type u → Type u) (r : Type u) : Type (u+1)
  | Respond {x : Type u} (downstreamOutput : Option b) (op : m x) (cont : x → ProxyNextStep b m r) : ProxyNextStep b m r
  | Pure    : r → ProxyNextStep b m r
@[inline] def Proxy.next [Monad m] (p : Producer b m r) : ProxyNextStep b m r :=
  match p with
  | Proxy.Request v _ => Empty.elim v
  | Proxy.Respond b fu => ProxyNextStep.Respond (.some b) (pure ()) (fun _ => Proxy.next (fu ()))
  | Proxy.M op cont => ProxyNextStep.Respond .none op (fun x => Proxy.next (cont x))
  | Proxy.Pure r => ProxyNextStep.Pure r
  termination_by structural p

but I'm still not sure it's the best. If someone has ideas - I will be very greatful.

[Serhii Khoma (srghma)]

Could someone help me to prove pushPullAssoc

theorem pushPullAssoc [Monad m] [LawfulMonad m]
  (f : b' → Proxy a' a b' b m r)
  (g : a  → Proxy b' b c' c m r)
  (h : c  → Proxy c' c b' b m r) :
  (f >+> g) >~> h = f >+> (g >~> h) := by
  sorry

this is an exact copy of push_pull_assoc from coq-pipes

I tried, but failed

Could someone teach me?

[Serhii Khoma (srghma)]

UPDATE on lib: added concurrency primitives https://github.com/srghma/lean-pipes/blob/6fe222d7bb5fca97e084c44a67b4e700e341111a/pipes/Pipes/Concurrent/MergeProducers.lean#L265

[Serhii Khoma (srghma)]

@Mario Carneiro (or anyone) Could You help

-- this is ok
inductive Proxy.{u} (a' a b' b : Type u) (m : Type u → Type u) (r : Type u) : Type (u + 1)
  | Request : a' → (a → Proxy a' a b' b m r) → Proxy a' a b' b m r
  | Respond : b → (b' → Proxy a' a b' b m r) → Proxy a' a b' b m r
  | M       {x : Type u} (op : m x) (cont : x → Proxy a' a b' b m r) : Proxy a' a b' b m r
  | Pure    : r → Proxy a' a b' b m r
-- but I cannot write
#reduce IO (Proxy Unit Empty Empty Unit IO Nat)
-- bc of `: Type (u + 1)`. But I need `: Type u`
-- why I have it? bc of `M       {x : Type u}`
-- Does anyone know some magic to allow me to write `IO (Proxy Unit Empty Empty Unit IO Nat)`?