Stream: Beginner Questions

Topic: Proof of monotonicity for `partial_function`

view this post on Zulip Ghilain Bergeron (Mar 21 2024 at 16:28):

Hi everyone,

I've been trying to use partial_function to define the cartesian product of lazy lists as defined in the Coinductive AFP entry (which, from my understanding of corecursion, I cannot define as primitive corecursive).

partial_function (llist) lmaps :: ‹('a ⇒ 'b llist) ⇒ 'a llist ⇒ 'b llist› where
  ‹lmaps f xs = (case xs of LNil ⇒ LNil | LCons x xs ⇒ lappend (f x) (lmaps f xs))›

partial_function (llist) lproduct :: ‹'a llist llist ⇒ 'a llist llist› where
  ‹lproduct xss = (case xss of
      LNil ⇒ LCons LNil LNil
    | LCons xs xss ⇒ lmaps (λ i. lmap (LCons i) (lproduct xss)) xs)›

(I could have gone away with using lconcat (lmap (λ i. lmap (LCons i) (lproduct xss)) xs) instead of using lmaps.)

However, somehow, Isabelle is unable to proof monotonicity of the lproduct function, failing with the following error

exception THM 0 raised (line 83 of "goal.ML"):
•  Proof failed.
   1. ⋀x xs xss.
      monotone llist.le_fun lprefix
    (λlproduct. lmaps (λi. lmap (LCons i) (lproduct xss)) xs)
•  (⋀x xs xss.
   monotone llist.le_fun lprefix
    (λlproduct. lmaps (λi. lmap (LCons i) (lproduct xss)) xs)) ⟹
  (⋀x. monotone llist.le_fun lprefix
     (λlproduct.
      case x of LNil ⇒ LCons LNil LNil
      | LCons xs xss ⇒
       lmaps (λi. lmap (LCons i) (lproduct xss)) xs)

I tried to prove this subgoal myself, which is basically a one-liner 

lemma lproduct_mono:
  fixes xss :: ‹'a llist llist›
  assumes
    ‹⋀ (xs :: 'a llist) (xss :: 'a llist llist).
      mono_llist (λ lproduct. lmaps (λi. lmap (LCons i) (lproduct xss)) xs)›
  shows
    ‹mono_llist (λ lproduct.
      case_llist (LCons LNil LNil) (λ xs xss. lmaps (λi. lmap (LCons i) (lproduct xss)) xs) xss)›
  by (cases xss) (auto intro: assms)

After looking at the mono_tac function in the partial_function.ML file, I tried to change the proof to better reflect what I understand this tactic is doing, and ended up with 

  by (cases xss; hypsubst; subst llist.case; rule llist.const_mono assms)

which also works.

I'm not sure what's wrong here, neither how I can try to debug this issue. I even tried to add the partial_function_mono attribute on the lemma (as described in the reference manual), to no avail.

Is anybody familiar with partial_function or knows what may be going wrong here?

view this post on Zulip Ghilain Bergeron (Mar 21 2024 at 16:47):

Ah!
I understand what's missing now.
I have to prove that ⋀ xs xss. monotone llist.le_fun lprefix (λ lproduct. lmaps (λi. lmap (LCons i) (lproduct xss)) xs). I initially thought that the output was a bit broken for some reason. Now I have to see if I can actually prove this (or derive it one way or another).

view this post on Zulip Jan van Brügge (Mar 23 2024 at 11:27):

Have you tried corec instead of primcorec? That might work

view this post on Zulip Ghilain Bergeron (Mar 23 2024 at 12:04):

Using corec for lproduct requires that either lconcat or lmaps (depending on which one is used in the definition) be friendly, which I'm afraid I don't know how they can be :c

view this post on Zulip Jan van Brügge (Mar 23 2024 at 12:35):

ah true

Last updated: Apr 28 2024 at 04:17 UTC