Re: [isabelle] Reasoning with the option type



Hi Eugene,

and there are lots of apparently unnecessary
> assumptions that float in and out.


You are completely right. My original (long) version would be like this
without
the unnecessary assumptions.

theorem
  fixes u::int and l::int
  assumes assm: "lâu"
  shows "sumO l u f = Some (â k=l..u. (f k))" (is "?P u")
  using assms
    proof (induct u rule: int_ge_induct)
      show "?P l"
       proof -
         have "sumO l l f = Some (f l)" by simp
         also have "... = Some (â k=l..l. (f k))" by simp
         finally show "sumO l l f = Some (â k=l..l. (f k))" by this
       qed
    next
      fix i::int
      assume hip01: "iâl" and HI:"?P i"
      show "sumO l (i+1) f = Some (â k=l..i+1. (f k))"
         proof -
            have
            "sumO l (i+1) f = (case sumO l i f of
             None â None | Some v â Some ((f (i+1) + v)))"
             using hip01 by simp
             also have "... = Some (f (i+1) + (â k=l..i. (f k)))"
             using HI and hip01 by simp
             also have "... = Some (â k=l..i+1. (f k))"
                proof -
                   have "{l..i + 1} = insert (i+1) {l..i}" using hip01
                     by auto
                   thus ?thesis by simp
                qed
              finally  show "sumO l (i+1) f = Some (â k=l..i+1. (f k))" by
this
         qed
    qed

Best!

On Tue, Apr 28, 2015 at 6:18 AM, Eugene W. Stark <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
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.