Re: [isabelle] Induction on the length of computation sequences (in Isabelle)



Hi Alfio,

To answer your two questions:

> 1) Is this a correct way to encode a proof of an invariant of a tail
> recursive function?

Yes, to use the induction-scheme by the function method is the usual way
in Isabelle/HOL. of course, the induction-scheme is independent of the
function itself: you can use other induction-schemes (like nat_induct),
and you can also use the induction scheme tail_multn.induct to prove
theorems no involving tail_multn.

> 2) Is there a more elegant way to approach this problem?
 
I find it quite elegant. Do you have anything more elegant in mind?
Obviously, if you have more specific theorems to prove you might use a
different approach.

Btw, sometimes when defining tail-recursive functions the
function-package is not enough and you might want to use
partial_function.

Greetings,
 - Johannes

Am Freitag, den 09.10.2015, 14:46 -0300 schrieb Alfio Martini:
> Dear Users,
> 
> Whenever I want to (manually) prove that an invariant of a tail recursive
> function is true,
> I perform induction on  the length of computation sequences. For instance,
> consider the following
> example:
> 
> fun tail_multn::"nat => nat => nat => nat" where
>   "tail_multn 0 n a = a" |
>   "tail_multn (Suc m) n a = tail_multn m n (a+n)"
> 
> Thus, a state s_ k (0<=k<=n) for a computation of this function is a triple
> s_k=(m_k,n_k,a_k) in nat x nat x nat.
> Now, using induction on k, I can prove that
> 
> P(k)=def all m,n,a:nat. tail_multn m n a = m_k*n_k+ a_k
> 
> The only way I was able to encode this proof in Isabelle was using
> computation induction,
> after reading carefully the presentation of this material in "Programming
> and Proving".
> 
> So, my proof in Isabelle is given by:
> 
> lemma "tail_inv": "tail_multn x y a = x*y +a"
>   apply (induction x y a  rule: tail_multn.induct)
>   apply (simp_all)
> done
> 
> Two questions:
> 
> 1) Is this a correct way to encode a proof of an invariant of a tail
> recursive function?
> 2) Is there a more elegant way to approach this problem?
> 
> Best!
> 






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