Re: [isabelle] Reasoning with the option type



Since the induction hypothesis contains meta implication, there is no other way to write it. You can, however, give names to your three different cases so you don't have to fix/assume everything yourself:


theorem
assumes "l â u"
shows "sumO l u f = Some (âk=l..u. f k)"  (is "?P l u f")
using assms
proof (induction l u f rule: sumO.induct[case_names 1 2 3])
  case (1 l f)
  show ?case by simp
next
  case (2 n m f)
  thus ?case using setsum_last_int by simp
next
  case (3 n m f)
  hence False by simp
  thus "?P n m f" by (rule FalseE)
qed


Cheers,

Manuel


On 28/04/15 17:11, Alfio Martini wrote:
Hi Manuel,

Thank you for the explanations about this more general technique. I have seen now that it is explained in detail in the "Programming and Proving" tutorial under the name of "computation induction". I have tried to see the logical structure underlying your version of the proof using Isar. I came up with the following and I assume there is a more elegant way to write it.

lemma setsum_last_int:
  "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}"
  by (subst setsum.insert[symmetric])
  (auto simp del: setsum.insert intro: setsum.cong)

 theorem
  assumes "l â u"
  shows "sumO l u f = Some (âk=l..u. f k)"  (is "?P l u f")
  using assms
   proof (induction l u f  rule: sumO.induct)
      fix l::int and f
      show "?P l l f" by simp
   next
      fix n::int and m and f
      assume "n<m" and "(n â m - 1 ==> ?P n (m - 1) f)"
      then  show "?P n m f"  using setsum_last_int by simp
   next
      fix n::int and m and f
      assume "m<n"  and "nâm"
      then have False by simp
      then show "?P n m f" by (rule FalseE)
   qed

It was very helpful, because I havenÂt seen before that the last goal follows by a simple contradiction. Yet, I am not comfortable with the way I wrote the induction hypothesis in the second goal. I had to use the metalogical symbol "==>". Assuming that I insist and writing all the details above, how could
I avoid using "==>"? I have no clue.

Best!

On Tue, Apr 28, 2015 at 6:56 AM, Manuel Eberl <eberlm at in.tum.de <mailto:eberlm at in.tum.de>> wrote:

    It is, of course, not unreasonable to do things by hand like you
    did in order to get to know the system better.

    I would, however, like to show you how to shorten the proof a bit
    more. Isabelle's automation is very powerful, but you have to help
    it along a bit. As a rule, when you try to prove a fact about a
    recursively-defined function, it is advisable to use the induction
    rule for that function that the function package gives you. It
    makes things easier, both for you and for the automation.

    So let's apply it and see what we end up with:

    theorem
      "l â u â sumO l u f = Some (âk=l..u. f k)"
    apply (induction l u f rule: sumO.induct)
    apply simp_all

    The remaining goal is then something like
    ân m f. n < m â f m + setsum f {n..m - 1} = setsum f {n..m}

    This should be intuitively obvious, we're just splitting off the
    last term in the sum from n to m. We can show this as an auxiliary
    lemma, e.g.

    lemma setsum_last_int:
      "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}"
      by (subst setsum.insert[symmetric]) (auto simp del:
    setsum.insert intro: setsum.cong)

    Now the proof is fully automatic:
    theorem
      "l â u â sumO l u f = Some (âk=l..u. f k)"
      by (induction l u f rule: sumO.induct) (simp_all add:
    setsum_last_int)


    Cheers,

    Manuel



    On 28/04/15 11:34, Alfio Martini wrote:

        Hi Eugene,

        Thank you for your feedback. Indeed it looks much shorter,
        since the
        simplifier takes care of the
        many intermediate steps I wrote it down. Anyway, at least for
        these
        exercises, I try to use Isabelle to check
        my handwritten proofs (or any handwritten proof that is made
        without
        assuming automated tools).
        That is why they look unnecessary  long. But I will use some
        of your
        suggestions in order to improve its presentation.

        Best!

        On Tue, Apr 28, 2015 at 6:18 AM, Eugene W. Stark
        <stark at cs.stonybrook.edu <mailto:stark at cs.stonybrook.edu>>
        wrote:

            I am not very experienced, but I looked at your proof.
            It seems very long, and there are lots of apparently
            unnecessary
            assumptions that float in and out.  I came up with the
            attached,
            which is rather shorter.  I did not see how the use of the
            option type introduces any complication here. Hopefully I did
            not misunderstand something important.

                                                             - Gene Stark


            On 04/27/2015 11:55 PM, Alfio Martini wrote:

                Dear Isabelle Users,

                In a previous thread (Isabelle: A logic of partial
                functions?) I asked
                some questions about the use of the constant
                "undefined" when
                dealing with partial functions, which  have to be made
                total according
                to the foundations of Isabelle.

                The long thread about my difficulties with
                Sledgehammer made
                me realize that my definition was not general enough.
                And after
                looking into the very well written tutorial on Code
                Generation, I
                was convinced that I had to deal with the option type.

                I'm  also very grateful to all that reply my original
                messages with
                many insightful and helpful observations.
                So, if some novice is interested I include here (my)
                proof of the
                total correctness of that sum algorithm.

                I only ask the evaluation of some more experienced
                user, if
                this is the correct way to reason  with the option
                type. It looks
                a bit clumsy.

                The thy file is attached. Many thanks for any remarks!

                Best!








--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio <http://www.inf.pucrs.br/alfio>
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.