mutual recursion -help (fmany - fsome)

Stream: new members

[lorã]

For this code

mutual
def fmany [Alternative f] (x : f α) : f (List α) := fsome x <|> pure []
def fsome [Alternative f] (x : f α) : f (List α) := pure (· :: ·) <*> x <*> fmany x
termination_by structural {
   sorry
}
end

I got this output

typeclass instance problem is stuck, it is often due to metavariables
  EmptyCollection ?m.13593

Thats only the second time that im trying to solve a mutual recursion problem, but this one is harder than the another. Can i ask for some help?

[Aaron Liu]

What is you argument that this pair of functions is terminating?

[lorã]

What is you argument that this pair of functions is terminating?

Sorry, i dont think i get it

[lorã]

this is a standard implementation in haskell, so I thought it should work

[Aaron Liu]

You need to make sure your implementation doesn't go into an infinite loop.

[lorã]

How can i fight with the lean system to prove that? Even the goal's not making a lot of sense to me. I tried to use the key word partial but also didnt work

[Aaron Liu]

section
instance [i : Nonempty α] [Pure f] : Nonempty (f α) :=
  i.elim fun a => ⟨pure a⟩
mutual
partial def fmany [Alternative f] (x : f α) : f (List α) := fsome x <|> pure []
partial def fsome [Alternative f] (x : f α) : f (List α) := pure (· :: ·) <*> x <*> fmany x
end
end

[Aaron Liu]

Though with partial you can't prove anything about the definitions

[Aaron Liu]

If you prove you definitions will never generate an infinite loop you don't have to use partial

[Aaron Liu]

Do note that every list in Lean is provably finite

[Aaron Liu]

Lean is also a strict language, unlike Haskell which is lazy.

[Mario Carneiro]

Here's a proof that this pair of functions can't be proved to terminate because the equations are inconsistent:

local instance [Alternative f] : Inhabited (f (List α)) := ⟨pure []⟩ in
mutual
partial def fmany [Alternative f] (x : f α) : f (List α) := fsome x <|> pure []
partial def fsome [Alternative f] (x : f α) : f (List α) := pure (· :: ·) <*> x <*> fmany x
end

axiom fmany_eq [Alternative f] (x : f α) : fmany x = (fsome x <|> pure [])
axiom fsome_eq [Alternative f] (x : f α) : fsome x = (pure (· :: ·) <*> x <*> fmany x)

structure Foo (_ : Type) where
  depth : Nat

instance : Alternative Foo where
  pure _ := ⟨0⟩
  seq _ b := ⟨(b ()).depth⟩
  failure := ⟨0⟩
  orElse a _ := ⟨a.depth + 1⟩

example : False := by
  suffices ∀ n (x : Foo Nat), (fmany x).depth = n → False from this _ ⟨0⟩ rfl
  intro n x eq
  induction n generalizing x with
    simp [fmany_eq, (· <|> ·), OrElse.orElse, Alternative.orElse] at eq
  | succ n ih =>
    simp [fsome_eq, Seq.seq] at eq
    exact ih _ eq