Short answer: totalize MAP2 and you can prove the desired congruence without
mentioning LENGTH.
Long answer : you can prove the congruence without the
LENGTH l1 = LENGTH l2
clause for a definition of MAP2 that is explicit about what happens when one
of the lists is empty and the other is not. Since the version of MAP2
in listTheory
has strictly less information than that, it can be patched together
from the more
detailed definition. And so any subsequent proofs using MAP2 will
still go through.
I suggest defining in listTheory the equivalent of
val MAP2_DEF =
Define
`(MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2) /\
(MAP2 f x y = [])`;
and then proving the current equations for MAP2:
store_thm ("MAP2",
``(!f. MAP2 f [] [] = []) /\
(!f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2)``,
METIS_TAC[MAP2_DEF]);
Then prove the congruence for MAP2, by using the induction theorem for MAP2_DEF,
or just plain list induction.
Cheers,
Konrad.
On Thu, Mar 29, 2012 at 7:02 PM, Ramana Kumar <[email protected]> wrote:
> Is it possible to get good termination condition extraction for functions
> like listTheory$MAP2?
> I can prove something like this:
> |- ∀l1 l1' l2 l2' f f'.
> (l1 = l1') ∧ (l2 = l2') ∧ (LENGTH l1 = LENGTH l2) ∧
> (∀x y. MEM x l1' ∧ MEM y l2' ⇒ (f x y = f' x y)) ⇒
> (MAP2 f l1 l2 = MAP2 f' l1' l2')
> But it's probably of the wrong form (because of the condition about the
> lengths being equal), and indeed adding it to the database in DefnBase
> doesn't help with termination condition extraction for uses of MAP2.
> Without a condition like that, though, I think the congruence is unprovable.
> Is there a right form?
>
> ------------------------------------------------------------------------------
> This SF email is sponsosred by:
> Try Windows Azure free for 90 days Click Here
> http://p.sf.net/sfu/sfd2d-msazure
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here
http://p.sf.net/sfu/sfd2d-msazure
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
