Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-27 19:22:17 -0800 (Tue, 27 Dec 2005)
Revision: 8377
Log message:

      Added lof "rippling" (unrelated to Bundy's induction scheme).  The idea
      is cool, here is a summary:
      
         - It is easy to prove theorems like
              lof{i. f['i]; 'n} ~ lof{i. g['i]; 'n}
           for some concrete f['i] and g['i].  To be clear,
           I don't mean f and g are sovars, I mean they
           represent some concrete terms.
      
           Example:
               lof{i. lof_append{j1. lof_nth_prefix{j2. lof_nth{'x; 'j2}; 'j1; 'n1; 'n2};
                                 j2. lof_cons{j3. lof_nil; 'j2; lof_nth{'x; 'n2}};
                                 'i; 'n3; 'n4}; 'n5}
               <-->
               lof{i. lof_nth{'x; 'i}; 'n5}
      
         - It is not easy, and often impossible, to prove
           a similar theorem when the lof is not the immediate
           ancestor of f['i] and g['i].
      
           You might argue that this is all due the "free algebra" that I
           am using.  If you are dubious in this respect, please look at the
           "bind pushing" theorems in Itt_hoas_lof, like "lof_bind_nil".
           These theorems are not obviously expressible in nested form.
           See Itt_hoas_lof rev 8376, where I tried to do so.  To prove these
           theorems we need contexts, and some very hard arguments.  OTOH,
           the simple forms are trivial.
      
         - So the idea is to use the reversible lof conversion
           in rippling form:
      
              - sweep up (normalizeLofC)
              - sweep dn (reduceLofC)
              - repeat until nothing changes
      
           In each phase, the lof will pass through the right place
           so that an optimization can be performed.
      
      Summary:
         - This is a very cool idea.
         - I expect to be shunned:)
         - For comments, please see if you can understand what is going on--
           I am more than happy to help if needed.  Destructive comments are
           ok, but scientific constructive arguments are even better.
      
      Comments:
         - To see it work, try expanding the theorems in Pmn_core_terms
           (wf_term_TyAll finally works!)
      
         - It is unoptimized
           -- wf_term_TyAll takes 70k-100k primitive steps!
              I am daunted by optimizing a proof of this size...
      
           -- I believe most of the steps are because we have a
              massive number of redundant subgoals like
                  <H>; ... >- |H1| in nat
              In any give proof we may have thousands of the same
              (identical) goal of this form.
      
              It would be nice to have a tactic for explicit
              caching/redundant-subgoal-elimination.