Re: [Hol-info] Inducting over pairs

[Peter V. H. <pal...@tr...>]

On 10/18/07, Juan Perna <ji...@cs...> wrote:
> I am trying to prove a goal of the form:
>
> g `(stepWise s1 s2) /\ (seqWireSAT s1) /\ (seqWireSAT s2) ==> seqWireSAT (parMerge s1 s2)`;
>
> were `s1` and `s2` are of type seq as follows:
>
> Hol_datatype
>     `seq =
>            Empty
>          | CombBlk of hwAction set => seq
>          | ClkBlk  of clkAction set => seq`;
>
>
> and `stepWise` is a boolean predicate capturing the notion of structural equivalence (i.e., both
> sequences follow the same pattern of constructors).
>
> My question is whether there is a way of inducting on both `s1` and `s2` as a "whole" (probably as a
> pair). I am asking for this because I have attempted this proof by doing the induction in sequential
> order (i.e., Induct_on `s1` THEN Induct_on `s2`) and the inductive hypotheses I got weren't useful
> to prove the goal.

It looks like you need to prove the quantified goal

g `!s1 s2. (stepWise s1 s2) /\ (seqWireSAT s1) /\ (seqWireSAT s2) ==>
seqWireSAT (parMerge s1 s2)`;

First do an induction on s1, then do not do an induction on s2, but do
a case-split instead.  What this will do is provoide you an inductive
hypothesis from the induction on s1 that will be universally
generalized on s2, allowing you to adapt it to any s2 that is needed.
This is probably what limited the applicability of the inductive
hypotheses you were getting.

Depending on your actual situation, it might be better to induct on s2
and then case-split on s1, or possibly neither will work.  In that
extreme case, make your induction mathematical induction on the sum of
the sizes of the two data structures, as

g `!n s1 s2. (size s1 + size s2 = n) ==>
     (stepWise s1 s2) /\ (seqWireSAT s1) /\ (seqWireSAT s2) ==>
seqWireSAT (parMerge s1 s2)`;

Then either Induct or completeInduct_on `n` should work, but will be a
lot more labor.

Peter

-- 
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)