Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 09:15:20 -0800 (Sun, 01 Jan 2006)
Revision: 8387
Log message:

      Rephrased the Provable intro rules, using the SubLogic judgment
      instead of a fixed logic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 12:56:24 -0800 (Sun, 01 Jan 2006)
Revision: 8388
Log message:

      Added initial Provability tactic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 13:53:31 -0800 (Sun, 01 Jan 2006)
Revision: 8389
Log message:

      Added Itt_list_set for new set-style theorems about lists.
      Eventually we should move some theorems from Itt_list2 into
      this file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 11:27:09 -0800 (Mon, 02 Jan 2006)
Revision: 8390
Log message:

      Added less ambiguous names for some of the refiner functions (for names
      like "eq", "hyps", "concl", etc.).
      
      Partial progress in Provable theorems, added a unification tactic.
      
      This commit is mainly just in case we have a power failure here--
      it is raining very hard.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 16:23:06 -0800 (Mon, 02 Jan 2006)
Revision: 8391
Log message:

      Added vector binders to the BTerm normalizer.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 16:27:30 -0800 (Mon, 02 Jan 2006)
Revision: 8392
Log message:

      Rename Meta_extensions_theory to Meta_context_theory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 17:32:11 -0800 (Mon, 02 Jan 2006)
Revision: 8393
Log message:

      Still working on well-formedness of reflected vector terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-03 13:05:49 -0800 (Tue, 03 Jan 2006)
Revision: 8394
Log message:

      Added a simple forward-chaining tactic in support/tactics/forward.ml
      It is a lot like dT elimination, but it checks that progress is being made.
      Perhaps there is a more generic way to do it.  The proof cache used to
      do forward chaining, and I imagine JProver does too.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-04 08:30:00 -0800 (Wed, 04 Jan 2006)
Revision: 8396
Log message:

      Changed the proof witness code in Itt_hoas_sequent_proof from
      unification-based to naming-based.
      
      Added more forward reasoning.  We have most of the facts, but
      we need a few more about mk_bterm, mainly that if a mk_bterm
      is well-formed, so are its subterms.  The theorems in
      Itt_hoas_bterm_wf are currently unproved.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-04 17:26:50 -0800 (Wed, 04 Jan 2006)
Revision: 8397
Log message:

      Completed proofs in Itt_hoas_bterm_wf. However, I added a well-formedness
      subgoal (subterms in List) to mk_bterm_wf_forward. Does it matter?
      
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-04 17:51:15 -0800 (Wed, 04 Jan 2006)
Revision: 8398
Log message:

      Now really proved theorems in Itt_hoas_bterm_wf, with useless well-formedness subgoals removed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 13:16:41 -0800 (Thu, 05 Jan 2006)
Revision: 8401
Log message:

      Include the SVN revision number (when available) in the MetaPRL version string.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 17:18:52 -0800 (Thu, 05 Jan 2006)
Revision: 8406
Log message:

      - Minor clean-up of the debugging code.
      - Added a license header.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-05 20:29:45 -0800 (Thu, 05 Jan 2006)
Revision: 8408
Log message:

      Re-added the Itt_hoas_sequent.bterm2_is_bterm rule.  However, this is
      not recommended because this kind of rule can break normal dT reasoning.
      
      Instead, I think these kind of rules are better accomplished with some
      kind of forward chaining (even the autoT kind should work fine, but I
      don't know how to enable it).
      
      Replaced the tactic in Pmn_core_terms.intro_term_TyAll with a terminating
      version.  Currently, expand_all () takes about 10sec for me.  Let me
      know if it doesn't terminate for you.
      
      Re-added pmn_core_terms.prla, so that you get the terminating tactics.
      Will remove this again once we all the proofs work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 22:36:35 -0800 (Thu, 05 Jan 2006)
Revision: 8409
Log message:

      (Issue 560) Give a better error message when a theory does not exist.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 22:42:29 -0800 (Thu, 05 Jan 2006)
Revision: 8410
Log message:

      (Issue 561) The format of editor/ml/mldebug.dir is different on Windows.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-06 08:43:04 -0800 (Fri, 06 Jan 2006)
Revision: 8411
Log message:

      Updated the incomplete proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 10:50:37 -0800 (Fri, 06 Jan 2006)
Revision: 8413
Log message:

      Incrementing the version numbers for the ASCII and binary formats to account
      for the new "const" modifier added in rev 8383.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 14:14:27 -0800 (Fri, 06 Jan 2006)
Revision: 8415
Log message:

      Spelling fixes

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 15:40:10 -0800 (Fri, 06 Jan 2006)
Revision: 8416
Log message:

      Revision-based status checking.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-01-06 17:55:10 -0800 (Fri, 06 Jan 2006)
Revision: 8417
Log message:

      Fixed the problem noticed by Aleksey - one-only-constraint case was treated incorrectly

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 21:31:31 -0800 (Fri, 06 Jan 2006)
Revision: 8418
Log message:

      - Itt_nat should extend Itt_omega
      
      - Now that "meta" is a virtual theory (that is needed for "omake doc"), it
        needs to be listed explicitly in THEORIES_ALL (in mk/defaults)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 22:16:30 -0800 (Fri, 06 Jan 2006)
Revision: 8419
Log message:

      - Updated arithT to generate fewer wf subgoals.
      - Proved all the rules that were left unproven in Itt_int_arith.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 23:27:00 -0800 (Fri, 06 Jan 2006)
Revision: 8420
Log message:

      Minor omegaT optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 00:07:35 -0800 (Sat, 07 Jan 2006)
Revision: 8421
Log message:

      Another minor omegaT optimization (that should reduce the number of wf
      subgoals that it generates).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 09:14:17 -0800 (Sat, 07 Jan 2006)
Revision: 8422
Log message:

      Making "omake clean" more clean.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-07 10:43:32 -0800 (Sat, 07 Jan 2006)
Revision: 8423
Log message:

      Simplfy the BTerm normalizer a bit.  This now uses a single
      sweepDnC pass to push binds into the subterms, then does
      a rippling phase.
      
      This cuts the number of primitive steps by about a factor of 3,
      but it is still huge, around 30k for wf_term_TyAll.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 11:36:28 -0800 (Sat, 07 Jan 2006)
Revision: 8424
Log message:

      Adding poplmark/naive to the "THEORIES=all" list.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 13:36:44 -0800 (Sat, 07 Jan 2006)
Revision: 8425
Log message:

      In proof browsing UI ("down 0"), give more information about the rewrites.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-08 12:51:03 -0800 (Sun, 08 Jan 2006)
Revision: 8427
Log message:

      Updated the forward-chainer to use a more efficient algorithm (bug #562).
      
      Made some progress with reflection, intro_term_TyFun is now proved.
      
      The following rule would be *really* nice, but I don't know if it
      is true or provable.
      
         <H>; append{l1; l2} in list; <J>; l1 in list; l2 in list >- C -->
         <H>; append{l1; l2} in list; <J> >- C
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-08 15:57:10 -0800 (Sun, 08 Jan 2006)
Revision: 8430
Log message:

      Added sqsimple{BTerm{'n}} to sqsimple resource
      
      Note: I have not proven bterm_sqsimple2 in order not to create conflict with
      Jason's work.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-08 21:01:22 -0800 (Sun, 08 Jan 2006)
Revision: 8431
Log message:

      Ok, enough for now.  The basic rules in Pmn_core_terms are proved.
      
      Forward-chaining has the following problem--a forward chaining
      rule might introduce a wf subgoal that would normally be proved
      by forward chaining on a later hyp.  Using forward chaining on
      the wf subgoal will result in a loop.  NOTE: wrt forward chaining,
      this is a major issue.
      
      For the moment, I added precedences to the forward chainer.  This
      is only a temporary fix.
      
      Added a fair number of new rules.  This is ad-hoc at the moment.
      Basically, I just see what isn't proved, and I add the appropriate
      theorems.  I'm not sure if we can make this systematic, but we
      should think about it.
      
      All rules in Pmn_core_terms are proved, but just *look* at the stats!
      500k primitive steps is totally--umm--amazing/terrible etc.
      Time for expand_all ():
         User time 293.000000; System time 2.820000; Real time 340.365773
      
         Refiner status:
            wf_term_TyTop
            is a derived object with a complete grounded proof (1 rule boxes, 3164 primitive steps, 248 dependencies)
         Refiner status:
            wf_term_TyFun
            is a derived object with a complete grounded proof (1 rule boxes, 15765 primitive steps, 249 dependencies)
         Refiner status:
            wf_term_TyAll
            is a derived object with a complete grounded proof (1 rule boxes, 35857 primitive steps, 254 dependencies)
         Refiner status:
            wf_Types
            is a derived object with a complete grounded proof (1 rule boxes, 38 primitive steps, 260 dependencies)
         Refiner status:
            mem_term_TyTop_Types
            is a derived object with a complete grounded proof (1 rule boxes, 101 primitive steps, 264 dependencies)
         Refiner status:
            mem_term_TyFun_Types
            is a derived object with a complete grounded proof (1 rule boxes, 103 primitive steps, 264 dependencies)
         Refiner status:
            mem_term_TyAll_Types
            is a derived object with a complete grounded proof (1 rule boxes, 105 primitive steps, 264 dependencies)
         Refiner status:
            intro_term_TyTop
            is a derived object with a complete grounded proof (1 rule boxes, 14782 primitive steps, 295 dependencies)
         Refiner status:
            intro_term_TyFun
            is a derived object with a complete grounded proof (1 rule boxes, 254485 primitive steps, 295 dependencies)
         Refiner status:
            intro_term_TyAll
            is a derived object with a complete grounded proof (1 rule boxes, 491120 primitive steps, 300 dependencies)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 12:51:02 -0800 (Mon, 09 Jan 2006)
Revision: 8433
Log message:

      Experimenting with optimization.
      
        - Tried adding a checker to the normalizer to prevent it from
          running if the term is already in normal form.  This doesn't
          seem to help at all, so it is disabled.
      
        - Add a hack to try folding the equality into a membership
          before normalization.
      
             member{'T; 'e} <--> 'e = 'e in 'T
      
          This helps a lot, about 25% faster/shorter proofs.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 14:20:12 -0800 (Mon, 09 Jan 2006)
Revision: 8434
Log message:

      Investigate a new plan of attack, where we prove theorems for all the
      common cases, say for mk_bterm up to arity 5.
      
      Place all the common cases in a "naive" BTerm normalizer, and run
      it before the general normalizer.
      
      This will continue to work, because it falls back to the general
      normalizer, but it should be faster if we have theorems for the common
      cases.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 14:30:17 -0800 (Mon, 09 Jan 2006)
Revision: 8435
Log message:

      Proved the initial set of simple theorems.
      
      The tactic will need some bind coalescing, and the routine stuff
      like eliminating mk_term, subst, bind.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 19:24:22 -0800 (Mon, 09 Jan 2006)
Revision: 8438
Log message:

      Added the "simple" BTerm normalizer.  This didn't work as well
      as I had expected.  It cut the proof steps about 1/3, but I thought
      it would be more.  intro_term_TyAll is now about 100k primitive
      steps.
      
      Adding a fallback to the general form doesn't currently work,
      need to investigate.
      
      If you want to try using the original rule, in Itt_hoas_bterm_wf
      change normalizeBTermSimpleC to normalizeBTermForceC.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-09 20:13:56 -0800 (Mon, 09 Jan 2006)
Revision: 8439
Log message:

      Teaching autoT that (1 = 2 in nat) and (1 = 2 in int) are contradictory
      hypotheses.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-10 05:47:00 -0800 (Tue, 10 Jan 2006)
Revision: 8440
Log message:

      Memory usage optimization in prefix_thenLocalLabelT

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-10 12:34:59 -0800 (Tue, 10 Jan 2006)
Revision: 8441
Log message:

      Minor reduceT optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-10 13:05:12 -0800 (Tue, 10 Jan 2006)
Revision: 8442
Log message:

      Small arithT optimization.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 13:27:50 -0800 (Tue, 10 Jan 2006)
Revision: 8444
Log message:

      Minor changes as I try to understand the problem with label
      munging.  I am beginning to believe that the label erasure
      is probably due to the UI, and the labels are actually "main".
      
      So the problem may be that multiple "main" labels are
      appearing for some reason.  Still tracking down.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-10 14:42:53 -0800 (Tue, 10 Jan 2006)
Revision: 8445
Log message:

      reduceC for +@ and *@ optimization:
      do not try to reassociate things that can be simply computed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-10 14:46:16 -0800 (Tue, 10 Jan 2006)
Revision: 8446
Log message:

      The poplmark/naive theory was missing a "clean" target.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 15:09:14 -0800 (Tue, 10 Jan 2006)
Revision: 8448
Log message:

      Check whether forward-chaining ever produces more than one "main" subgoal.
      
         - Added a new tactical 
           
              checkSubgoalsT : (tactic_arg list -> unit) -> tactic -> tactic
      
           so that it is possible to look at the results of an inference.
      
         - Pass the location to annotation_processors so that we can print
           more informative error messages if necessary.
      
      However, all this does not help, since each step of forward-chaining
      produces exactly one subgoal labeled "main", but we still get multiple
      "main" subgoals after everything is finished.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 15:26:03 -0800 (Tue, 10 Jan 2006)
Revision: 8449
Log message:

      Minor adjustment fixes the problem with forward-chaining:
         use thenMT after rwhAll unfold_bsequent
      
      Apparently, the "assertion" goals produced by conditional rewrites are
      being relabeled to "main" by the forward-chainer.  I don't know why.
      
      However, there are a lot of rules in ITT with explicit [main] labels.
      So this means we'll get explicit "main" subgoals popping up randomly.
      
      BTW: what is going on with omegaT breaking all the proofs?  For some
      reason these get labeled as _my_ fault:b
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 15:30:54 -0800 (Tue, 10 Jan 2006)
Revision: 8450
Log message:

      Oops, actually I did break the proofs with a bogus addrC.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 16:47:34 -0800 (Tue, 10 Jan 2006)
Revision: 8451
Log message:

      Added the four expressions (of type Exp).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 16:59:48 -0800 (Tue, 10 Jan 2006)
Revision: 8452
Log message:

      Added all syntax except the fsub sequent.
      Expansion time is currently 214sec.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-11 00:48:41 -0800 (Wed, 11 Jan 2006)
Revision: 8453
Log message:

      - Use the location information (that is now available thanks to Jason's rev
        8448 changes) in error messages generated by the annotation processors.
      
      - Figured out how to fix filter_main so that the locations generated by the
        MetaPRL parser contain the correct file name.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-11 09:22:31 -0800 (Wed, 11 Jan 2006)
Revision: 8454
Log message:

      Reduce annotations on conditional rewrites --- for all the 0-arity SO
      variables that occur in assumptions, run reduceC on the corresponding subterms
      _before_ applying the rewrite.
      
      For example, if you have:
      
      interactive_rw reduce_foo {| reduce |} :
         'a in footype -->
         foo{'a; 'b; 'a} <--> ...
      
      then the reduce resorce will get the following rewrite:
      
         addrC [1] reduceC thenC addrC [3] reduceC thenC reduce_foo
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-11 13:32:26 -0800 (Wed, 11 Jan 2006)
Revision: 8455
Log message:

      Modifying a bit the reduce annotation approach that I've added in the previous
      commit.
      
      Now the reduce annotations perform the following check on all the rewrites
      (regardless of whether they are conditional or not) - if a SO var will be
      duplicated by a rewrite (i.e. it appears more than once in the
      "contractum+assumptions"), then the reduceC will be called on the
      corresponding subterms before the rewrite is applied.
      
      For example,
      
      interactive_rw foo_reduce {| reduce |} :
         'a in footype -->
         'b in footype -->
         'c in footype -->
         foo{'a;'b;'b;'c;'d;'e} <--> foobar{'a;'b;'d;'d;'e}
      
      will add
         addrC [1] reduceC thenC addrC [2] reduceC thenC addrC [3] reduceC thenC
         addrC [5] reduceC thenC foo_reduce
      
      (the rewrite will duplicate 'a, 'b and 'd, so those are normalized
      before-hand).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-11 19:41:06 -0800 (Wed, 11 Jan 2006)
Revision: 8456
Log message:

      Add a conversion from sequents to BTerms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-12 15:46:39 -0800 (Thu, 12 Jan 2006)
Revision: 8458
Log message:

      Reproved all the theorems in Itt_hoas_proof1 without 'ty_sequent
      (it is now BTerm).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-12 15:52:16 -0800 (Thu, 12 Jan 2006)
Revision: 8459
Log message:

      Forgot to commit the proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-12 17:38:29 -0800 (Thu, 12 Jan 2006)
Revision: 8460
Log message:

      Added an intro annotation on a rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-12 18:04:02 -0800 (Thu, 12 Jan 2006)
Revision: 8461
Log message:

      The Itt_hoas_util.elim_bdepth rule ("OmegaT is failing on some artihmetic, so
      make it simpler.") is no longer needed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-12 20:15:02 -0800 (Thu, 12 Jan 2006)
Revision: 8463
Log message:

      Working on the inverse function that transforms a BTerm back into
      a Sequent.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-13 12:09:21 -0800 (Fri, 13 Jan 2006)
Revision: 8465
Log message:

      Added the sequent_of_bterm{'e} that converts back from a BTerm
      to a Sequent.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-13 12:26:04 -0800 (Fri, 13 Jan 2006)
Revision: 8466
Log message:

      Convert sequents to BTerms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-13 13:04:02 -0800 (Fri, 13 Jan 2006)
Revision: 8467
Log message:

      Working on proof steps.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-13 14:37:05 -0800 (Fri, 13 Jan 2006)
Revision: 8468
Log message:

      Further cleanup wrt BTerm sequents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-13 14:42:11 -0800 (Fri, 13 Jan 2006)
Revision: 8469
Log message:

      - Do pro-active normalization of the numerical expressions (so that they are
        normalized before they are duplicated). This is done by changing the
        annotation processor for all the hoas_lof/hoas_normalize resources.
      
      - substl coalescing (substl_substl_lof2) is not a part of the normalizeLofC
        (it has the exactly right style and it is wasteful to dedicate a separate
        sweepUpC to it).
      
      - Tried making the "constant reduction" more robust. In particular, when
        normalizeLofC performs a "constant reduction", it will now follow up by
        using reduceC to fully propagate the constant. I've removed Jason's "I
        believe they are too fragile" comment because I think it no longer applies.
        Also, moved the hd_lof rewrite into the "constant reduction" section (where
        it belongs).
      
      This reduces the THEORIES=all expansion time and #of primitive steps by >10%.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-13 15:28:40 -0800 (Fri, 13 Jan 2006)
Revision: 8470
Log message:

      Rippling is no longer needed!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-13 18:53:10 -0800 (Fri, 13 Jan 2006)
Revision: 8471
Log message:

      - Filter: when copying proofs from an old .prla/.prlb/.cmoz, pick up any
      available proof - regardless whether it refers to a rewrite, a conditional
      rewrite, or a rule. It used to be the case that if one removes a condition in
      a rewrite (making it an unconditional one), the old proof will not get picked
      up, which seems wrong.
      
      - The crw_args field name is misleading, renamed it to crw_assums.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-13 19:05:45 -0800 (Fri, 13 Jan 2006)
Revision: 8472
Log message:

      Minor optimization: use "n>0" instead of "not{n=0 in nat}" in conditional
      rewrites.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-13 20:10:29 -0800 (Fri, 13 Jan 2006)
Revision: 8473
Log message:

      Now that the arithmetical reduction is in place, the lof_nil lists will always
      have a length that is literally 0 (as opposed to simply being equal to 0).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-14 00:52:29 -0800 (Sat, 14 Jan 2006)
Revision: 8474
Log message:

      Proved the "provable_elim" theorem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-14 08:20:34 -0800 (Sat, 14 Jan 2006)
Revision: 8475
Log message:

      I think we do not need the type BSequent for the bterms that represent
      sequents, so I'm going to try and weaken it to BTerm{0}.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-14 09:06:07 -0800 (Sat, 14 Jan 2006)
Revision: 8476
Log message:

      Allow bindings in the forward rules in Itt_hoas_bterm_wf.
      Will need to add them in other places too.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-14 13:07:34 -0800 (Sat, 14 Jan 2006)
Revision: 8477
Log message:

      Trying to optimize onSomeHypT (autoT's version of onSomeHypT nthHypT).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-14 15:20:05 -0800 (Sat, 14 Jan 2006)
Revision: 8478
Log message:

      - Added to nth_hyp: 't in BTerm{'d} --> 'd = bdepth{'t} in int
      
      - Refreshed itt_hoas_sequent_bterm.prla (since a lot of ruleboxes in it are no
        longer needed).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-14 17:07:24 -0800 (Sat, 14 Jan 2006)
Revision: 8479
Log message:

      Well, after much work, I'll probably need to take another approach
      to wf reasoning.
      
      Suppose we know
      
           sequent_bterm{"sequent"{arg; hyps; concl}} in BSequent
      
      where
           sequent_bterm is the Sequent -> BTerm{0} function
           BSequent is the type of well-formed BTerms than specify sequents
      
      What we would like is to know
           arg in BTerm{0}
           hyps in CVar{0}
           concl in BTerm{|hyps|}
      
      Of course, this is not true.  If the arg,hyps,concl are ill-formed,
      then we may get anything, even a BSequent.
      
      What we *do* know is that
      
           sequent_of_bterm{sequent_bterm{"sequent"{arg; hyps; concl}}} in Sequent
      
      However, sequent_of_bterm may return a sequent triple that is
      aribtrarily different from the triple (arg, hyps, concl).
      
      No idea what to do, thinking.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-14 19:22:31 -0800 (Sat, 14 Jan 2006)
Revision: 8480
Log message:

      The dest_bterm_mk_term2 rewrite in Itt_hoas_bterm had wf conditions that were
      too restrictive. I've relaxed the conditions and renamed the rewrite into
      dest_bterm_mk_term.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-14 20:00:18 -0800 (Sat, 14 Jan 2006)
Revision: 8481
Log message:

      Working on relaxed wf constraints.
      
         The @tt[Itt_hoas_relax] module defines some transformations
         with relaxed wf subgoals.
      
         The goal here is to define a type << Bind >> that includes
         all the terms in Itt_hoas_base.  It will follow trivially
         that << BTerm subtype Bind >>.  It will also follow that
         any term of the form << bind{'n; x. inr{math_ldots}} >>
         will be in the << Bind >> type.
      
         We can then show the eta-rules for << Bind >> terms, and
         then a corresponding rule for
         << dest_bterm{'e; l, r. 'base['l; 'r]; d, o, s. 'step['d; 'o; 's]} >>
         that uses relaxed terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-14 21:12:36 -0800 (Sat, 14 Jan 2006)
Revision: 8482
Log message:

      Merged in the trunk changes (revisions 8281:8481):
         svn merge -r 8281:8481 svn+ssh://svn.metaprl.org/svnroot/mojave/metaprl
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-15 01:14:09 -0800 (Sun, 15 Jan 2006)
Revision: 8483
Log message:

      Added elimination rules which do not do thinning. The one with bindings is hard; not proved yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-15 13:09:18 -0800 (Sun, 15 Jan 2006)
Revision: 8484
Log message:

      Proved the relaxed eta-reduction rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-15 16:12:26 -0800 (Sun, 15 Jan 2006)
Revision: 8485
Log message:

      Proved eta-reduction under mk_bterm.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-15 17:47:20 -0800 (Sun, 15 Jan 2006)
Revision: 8486
Log message:

      Basic relaxed theory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-15 21:29:33 -0800 (Sun, 15 Jan 2006)
Revision: 8487
Log message:

      Reproved the Itt_hoas_sequent_bterm1 using relaxed properties.
      Proved the forward-chaining rules.  My proofs should be cleaned
      up, I was too lazy.
      
      The forward rules have the following wf requirements
      
         hyps in CVarRelaxed{0}
         concl in Bind{length{hyps}}
      
      These goals are extremely easy to prove via theorems like
      Itt_hoas_relax.mk_bterm_in_bindn:
      
         "wf" : <H> >- n = m in nat -->
         "wf" : <H> >- subterms in list -->
         <H> >- mk_bterm{n; op; subterms} in Bind{m}
      
      They also hold, by construction, on all bsequent{| ... >- ... |}.
      
      Current state:
         - We need better tactics for membership in Bind.  It is often
           a mistake to use (x in BTerm => x in Bind), so there are a
           bunch of nth_hyp to control the application.  This is
           inefficient, and we get too many cases that are not covered.
      
         - Need to prove the properties for bsequent{| ... |}, and
           reprove the forward rules in Itt_hoas_sequent_term1.
           Note that these are the strong rules (the non-eta-expanded
           rules).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-16 20:13:40 -0800 (Mon, 16 Jan 2006)
Revision: 8488
Log message:

      NOTE: this is a moderate change to the internal way we handle
      resource annotations.
      
         - Resource arguments are now passed as labeled initial arguments to
           the annotation processor.  If you have an annotation processor
           that takes arguments, you define it as a function that takes
           the arguments and produces an annotation processor.
      
               val process_elim_resource_annotation :
                   ?options: elim_option list -> (term * (int -> tactic)) annotation_processor
      
         - The argument may be required or optional as desired.
      
         - Unlabeled arguments are relabeled as "options".
           Note that a function is allowed to take multiple arguments
           with the same label.
      
         - The annotation_processor and rw_annotation_processor types no
           longer require the first type argument.
      
      Changes to the "reduce" resource:
      
         - Added a ~select:<string> argument to the annotation processor
           that can be used to control when the rewrite
           is allowed.  By default, if the argument is not specified,
           the rewrite is always allowed.
      
         - You now need to use the wrap_reduce function when you add conversions
           manually (this is why so many files were changed in this update).
      
              let resource reduce +=
                 << foo >>, wrap_reduce reduce_foo
      
      Notes:
         - Since dT arguments are declared as optional, it is legal to
           write {| intro |} instead of {| intro [] |}.
      
         - We should allow other options to the reduce resource,
           including type inference, etc.
      
         - It is ok with me if we collect the reduce options into a list,
           like we do for dT.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-16 21:53:28 -0800 (Mon, 16 Jan 2006)
Revision: 8489
Log message:

      Define super-relaxed rewrites.  I forgot that bsequent{| ... |}
      only ensures bounds on the binding depths, not the exact binding
      depth.
      
      The type Bind{n} contains all terms bind{n; y. e[y]}.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 00:49:22 -0800 (Tue, 17 Jan 2006)
Revision: 8490
Log message:

      Added the ?select option to wrap_reduce.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 08:52:35 -0800 (Tue, 17 Jan 2006)
Revision: 8491
Log message:

      For reduce, the ~select argument should be a string list.
      
      Internally, these lists are converted to SymbolSet.t.
      
      We should probably consider representing the options in the tactic_arg
      as a SymbolSet.t.  Or perhaps as an OpnameSet.t.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 09:02:28 -0800 (Tue, 17 Jan 2006)
Revision: 8492
Log message:

      Proved the relaxed reduction rules.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 13:39:18 -0800 (Tue, 17 Jan 2006)
Revision: 8494
Log message:

      Changes to options:
      
         - Options are now based on opnames, so that we don't get
           accidental collisions between unrelated theories.
      
         - The tactic_arg options are OptionAllow and OptionExclude.
           So
      
              # Allow rules labeled with the given opname
              withAllowOptionT : term -> tactic -> tactic
      
              # Exclude rules labeled with the given opname
              withExcludeOptionT : term -> tactic -> tactic
      
           To make this work, we need to extend option annotations
           for rules.  Not done yet.
      
         - The Top_options.select resource can be used to specify
           default options for a theory.
      
           [Ping Aleksey]  I get confused by Mp_resource.  Currently,
           theory-local resources are pruned during close_theory.
           I don't know if this works.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 14:45:46 -0800 (Tue, 17 Jan 2006)
Revision: 8495
Log message:

      Further changes (this is all I plan to do for the moment).
      
         - All annotation processors require two optional arguments
      
             ?select: term list    
                - the rule will only apply if a specific
                  option is given (only the opnames of the term matter)
      
             ?labels: term list
                - the rule applies by default, but can be disabled
                  by the withExcludeOptionT option.
      
      As before, the "select" resource can be used to specify options
      on a theory-wide basis.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 15:35:52 -0800 (Tue, 17 Jan 2006)
Revision: 8496
Log message:

      Roll back the changes to Mp_resource.  Clearly I don't know what I am
      doing.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 16:10:55 -0800 (Tue, 17 Jan 2006)
Revision: 8497
Log message:

      Forgot to commit option_sig.ml.
      
      Added a proof_initialize resource that can be used to initialize
      the initial tactic_arg.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 16:53:49 -0800 (Tue, 17 Jan 2006)
Revision: 8498
Log message:

      Allow preprocessing on the tactic_arg before the proof is created.
      This probably isn't quite right.  When the "select" resource is changed,
      existing proofs will not be changed.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-17 17:28:31 -0800 (Tue, 17 Jan 2006)
Revision: 8499
Log message:

      Finally proved the elimination rule thanks to Aleksey; my original statement was wrong.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-17 17:49:18 -0800 (Tue, 17 Jan 2006)
Revision: 8500
Log message:

      Cleaned the theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-17 18:28:43 -0800 (Tue, 17 Jan 2006)
Revision: 8501
Log message:

      Minor: eagerly compose the functions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 20:53:03 -0800 (Tue, 17 Jan 2006)
Revision: 8502
Log message:

      Reproving theorems in Itt_hoas_sequent_bterm2.
      
      Unfortunately, I forgot to rename the terms to Itt_hoas_sequent_bterm2
      in the .prla before I started working... Apparently if I do it now,
      I get a ASCII IO error, weird.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-17 23:44:07 -0800 (Tue, 17 Jan 2006)
Revision: 8503
Log message:

      *** WARNING : BREAKS BINARY COMPATIBILITY ***
      ***  Export your proofs before updating!  ***
      
      This adds a private/public flag to all the resource improvements (including
      annotations). The public improvements get inherited by ancestors, while
      private ones remain local to the current theory.
      
      Syntax: 
      
      private let resource += ...
      public let resource += ...
      
      interactive foo {| public intro [AutoMustComplete]; private intro [] |} ...
      
      The private/public flag is optional, "public" is assumed by default.
      
      Note: short of not breaking the existing code, this is completely untested.
      Will try testing tomorrow, unless Jason beats me to it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-18 11:11:32 -0800 (Wed, 18 Jan 2006)
Revision: 8504
Log message:

      Implemented Aleksey's scheme for options.
      
         - Each rule/rewrite gets a set of labels.
           They are defined, for example, as follows:
      
              interactive foo {| intro ~labels:[<< foo >>] |} ...
      
         - The "select" resource is an ordered list
           opname * option_info, where
      
              option_info =
                 OptionAllow
               | OptionExclude
               | OptionIgnore
      
         - A rule is selected as follows, searching down the options
           list, for each option:
              1. (opname, OptionAllow) when opname in labels
                 Allowed
              2. (opname, OptionExclude) when opname in labels
                 Rejected
      
      An (opname, OptionIgnore) cancels all previous entries for the opname.
      For efficiency, the resource implementation squashes the options list,
      removing duplicate and OptionIgnore entries (preserving the semantics).
      
      Note that rules without labels are always allowed.
      
      If you want a rule to be off by default:
      
         declare foo_option
      
         let resource select += << foo_option >>, OptionExclude
      
         interactive foo {| intro ~labels:[<< foo_option >>] |} : ...
      
      You can override later several ways:
      
         1. use the resource, usually private
      
            private let resource select += << foo_option >>, OptionAllow
      
         2. use a tactical locally
      
            BY withAllowOptionT << foo_option >> (...)
      
         3. use a tactic for the rest of the proof
      
            BY addAllowOptionT << foo_option >> (...)
      
      There are other tactics, if you want more control:
         addOptionT : term -> string -> tactic
         withOptionT : term -> string -> tactic
      ...
      
      Notes:
         - Currently, the withoutOptionT is still defined.  It should
           probably be defined as
      
              withoutOptionT t =
                 withOptionT t "ignore"
      
         - It might be nice to label every rule with its name.