On Jan 4, 2008 9:59 AM, apfelmus
Felipe Lessa wrote:
How can we prove that (runPromptM prompt === id)? I was trying to go with
You probably mean
runPromptM id = id
Actually, I meant an specialization of 'runPromptM prompt': runPromptM id :: (Monad p) => Prompt p r -> p r runPromptM prompt :: (MonadPrompt p m) => Prompt p r -> m r runPromptM (prompt :: p a -> Prompt p a) :: Prompt p r -> Prompt p r [snip]
you could use mathematical induction . You can do the same here, but you need to use coinduction. For more, see also
Thanks for the tip! So I can define
approx :: Integer -> Prompt p r -> Prompt p r approx (n+1) (PromptDone r) = PromptDone r approx (n+1) (Prompt p c) = Prompt p (approx n . c)
runId :: Prompt p r -> Prompt p r runId = runPromptM prompt
and try to prove that ∀n. approx n (id x) == approx n (runId x) We can see trivially that approx n (id (PromptDone r)) == approx n (runId (PromptDone r)) For the case that x is (Prompt p c), we'll prove using induction. The base case n = 0 is trivially proven as ∀x. approx 0 x == ⊥. For the indutive case, approx (m+1) (runId (Prompt p c)) -- definition of runId = approx (m+1) (runPromptM prompt (Prompt p c)) -- definition of runPromptM for the Prompt case = approx (m+1) (prompt p >>= runPromptM prompt . c) -- definition of prompt in the Prompt instance = approx (m+1) (Prompt p return >>= runPromptM prompt . c) -- definition of (>>=) in the Prompt instance = approx (m+1) (Prompt p ((>>= runPromptM prompt . c) . return)) -- monad law '(return x >>= f) == f x' = approx (m+1) (Prompt p (runPromptM prompt . c)) -- definition of approx = Prompt p (approx m . runPromptM prompt . c) -- definition of runId = Prompt p (approx m . runId . c) -- definition of (.) twice = Prompt p (\x -> approx m (runId (c x))) -- induction hypothesis = Prompt p (\x -> approx m (id (c x)) -- definition of (.) twice = Prompt p (approx m . id . c) -- definition of approx = approx (m+1) (Prompt p (id . c)) -- law 'id . f == f' = approx (m+1) (Prompt p c) -- law 'x == id x' = approx (m+1) (id (Prompt p c)) Which was to be proven. ∎ I think I didn't commit any mistake above =). Thanks again for help, -- Felipe.