Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 12:52:01 -0800 (Tue, 01 Nov 2005)
Revision: 8071
Log message:

      Proved the induction principle on derivations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 20:01:07 -0800 (Tue, 01 Nov 2005)
Revision: 8075
Log message:

      Rebuilt the FSub languages directly from BTerm.
      I think this is the way to go, the theories are much smaller.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 20:33:50 -0800 (Tue, 01 Nov 2005)
Revision: 8076
Log message:

      Separate the judgments from the rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-02 16:35:41 -0800 (Wed, 02 Nov 2005)
Revision: 8080
Log message:

      I am working on rewriting and simplifying MetaPRL core IO - I want to change
      it so that the "role" of .cmoz/.prlb/.prla files is better established.
      
      In particular. my goals are
      
       - In the editor, the module is always taken from the .cmoz. (Optionally: if
         .prlb or .prla is newer, then the proofs are read and _merged_)
       - The .prlb is a "cache" for the .prla. If the .prla have changed since the
         .prlb was generated, the old .prlb is discarded (even if it happens to be
         newer).
       - Optionally: refuse to load .cmoz into toploop, if it was compiled against a
         version of MetaPRL that is different from the one currently running.
       - Longer term: only store proofs (and other items created or modified from
         the toploop) in .prlb/.prla. This way the .prla are much smaller, the
         locations are not stored in .prlb, the items created from the toploop are
         not discarded at repompile.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-02 16:43:10 -0800 (Wed, 02 Nov 2005)
Revision: 8081
Log message:

      Working on the new IO. This commit mostly just rips apart the old code,
      without yet contributing much new.
      
      Not even close to compiling.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-02 21:13:35 -0800 (Wed, 02 Nov 2005)
Revision: 8082
Log message:

      Added string options.  These are like selT, but you need to use
      addOptionT or withOptionT.
      
      The differences with selT:
         1. The option is a string (perhaps it should be an opname?)
         2. A rule annotation can have multiple options using the
            [StringOption "foo"; StringOption "bar"] intro/elim
            argument.
      
      The addOptionT adds the option for the entire rest of the proof tree.
      The withOptionT adds it for a single tactic.
      The removeOptionT removes it for the rest of the proof tree.
      The withoutOptionT removes it for a single tactic.
      
      Unfortunately, the addOptionT isn't currently working.  Somewhere,
      it looks like proof annotations are getting cleared.  Looking
      into it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 10:38:21 -0800 (Thu, 03 Nov 2005)
Revision: 8084
Log message:

      Commented the code in Proof_boot that was removing all annotations
      from IO proofs.
      
      If I understand correctly, this code was added to clean up old proofs
      where annotations were mistakenly lying around.  That is, it was added
      for backwards compatibility.
      
      The best solution is probably just to re-export those broken proofs
      to fix the problem.  Alternately, and less satisfying, we could add
      another annotation that says "I really want to keep my annotations."
      
      We may want to add an annotation check to the subgoal/cache matcher
      so that subgoals are considered to be equal only if the annotations
      match.  This is probably good enough, or we could add an explicit
      annotation transformation rulebox before pulling in a subgoal with
      different annotations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 16:47:41 -0800 (Thu, 03 Nov 2005)
Revision: 8085
Log message:

      Updated with Itt_dfun axioms instead of the Itt_rfun ones and Itt_pairwise
      axioms instead of Itt_pointwise ones.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 18:29:13 -0800 (Thu, 03 Nov 2005)
Revision: 8088
Log message:

      - Proved the nilSqequal rule (it used to be primitive).
      - Some more progress verifying ITT Core under the pairwise functionality.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 21:01:47 -0800 (Thu, 03 Nov 2005)
Revision: 8089
Log message:

      Defined the IO module for .cmiz
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 21:08:10 -0800 (Thu, 03 Nov 2005)
Revision: 8090
Log message:

      - Proof steps match only if the annotations match.
      - Removed annotation removal during IO squashing.
      - Expanded all proofs that produce warning messages,
        and re-exported them.
      
      Note, I believe I hit the weak-memo bug, or something like it
      during proof expansion, and I got crazy terms appearing in
      unrelated theorems:(  I believe I have re-fixed all those
      broken proofs.  check-status reports that all is well.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 21:35:59 -0800 (Thu, 03 Nov 2005)
Revision: 8091
Log message:

      Added ty_exp_elim_slow for testing purposes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 22:00:17 -0800 (Thu, 03 Nov 2005)
Revision: 8092
Log message:

      Moving the closed branches out of the way.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 22:14:06 -0800 (Thu, 03 Nov 2005)
Revision: 8093
Log message:

      Adding lm_set.ml to the list of files to be included in the "magic" digest
      calculation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-03 22:16:24 -0800 (Thu, 03 Nov 2005)
Revision: 8094
Log message:

      Exploring the "this takes too long" example further. Simply running jproverT
      in /poplmark_naive/pmn_core_terms/ty_exp_elim_slow/1/1/1/1/1/2/2/1/1/1/1/2
      seems to take too long.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-04 09:27:20 -0800 (Fri, 04 Nov 2005)
Revision: 8095
Log message:

      Relaxed a bit the test for "may be patterns". If all occurrences of a second
      variable in the redex are "pattern-like" occurrences inside another second
      order variable (which means that in the actual match in may not occur at all
      if that other SO variable does not depend on its argument), the rewriter used
      to complain. I've changed it so that if that SO variable does not occur in the
      contractum, then rewriter accepts such rewrite.
      
      Example:
      
      interactive tunionHyp {| nth_hyp |} 'H :
         sequent { <H>; x: 'B['a]; <J['x]> >- 'x in Union x:'A. 'B['x]  }
         
      Here the rewriter used to complain that 'a does not have a pattern and needs
      to be passed in as an argument, which is clearly unnecessary in this case.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-04 10:05:14 -0800 (Fri, 04 Nov 2005)
Revision: 8096
Log message:

      - Updated the elimination rules for Union so that they better preserve binding
        names.
      
      - Fixed the proof of tunionElimination_disjoint
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-04 14:07:15 -0800 (Fri, 04 Nov 2005)
Revision: 8097
Log message:

      Apparently we had forgotten to save string attributes to the IO proof
      terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-04 20:36:28 -0800 (Fri, 04 Nov 2005)
Revision: 8100
Log message:

      Added the (Annotate of tactic_arg * tactic_arg) proof step.  This
      addresses the problem with proof annotations being dropped.
      
      Proof files (.prlb and .prla) are defined to be backwards-compatible,
      but not forwards-compatible.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 13:20:43 -0800 (Sat, 05 Nov 2005)
Revision: 8109
Log message:

      Save the current version with structural induction while I
      try the pure BTerm approach.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 15:50:05 -0800 (Sat, 05 Nov 2005)
Revision: 8110
Log message:

      Trying out the "well-formedness"-based Fsub logic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 20:40:58 -0800 (Sat, 05 Nov 2005)
Revision: 8111
Log message:

      Added the "reflected_logic" block, see Pmn_core_logic for an example.
      Currently working out the rule arguments, so the final few
      rules are disabled.
      
      The main goal is, for a rule
      
         interactive foo : <mt>
      
      Do 3 things:
         1. Define unfold_foo : foo <--> <mt>
         2. Add a wf rule, <H> >- foo IN ProofRule
         3. Add the provability rule (one direction of reflection):
      
            If <mt> == <t1> --> ... -> <tn>
            Add the real rule:
      
               <H> -> Provable{t1} -->
               ...
               <H> -> Provable{tn}
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-05 23:48:24 -0800 (Sat, 05 Nov 2005)
Revision: 8112
Log message:

      Further "autoT is taking too long" investagation - in 
      /poplmark_naive/pmn_core_terms_test/ty_exp_elim_slow/1/1/1/1/1/2/2/1/1/1/2/1
      even the simple_jproverT tactic is taking forever.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-06 18:03:10 -0800 (Sun, 06 Nov 2005)
Revision: 8116
Log message:

      Returned to requiring wf of sequents, so that we don't need wf-subgoals
      in the object logic.
      
      This mostly completes the initial phase of the Filter_parse reflection.
      You can define a logic of syntax, or a logic of rules, or any mixture.
      
         reflected_logic foo_logic =
         struct
            declare typeclass AExp
            declare typeclass BExp
      
            declare A : AExp
            declare B{'e : AExp} : AExp
            declare C{a: AExp. 'e['a] : BExp} : BExp
      
            interactive c_intro :
               sequent { <H>; a: A >- 'e['a] } -->
               sequent { <H> >- C{a. 'e['a]} }
         end
      
      Declarations are processed as normal in this block, plus 3 new parts
      are added.  Only the reflected rule makes sense.
      
      Each declaration/rule produces 3 parts:
         1. A definition (unfold_X : X <--> <definition>)
         2. A wf-goal (interactive X_wf : X in ProofRule)
         3. An ITT rule:
            interactive X_itt :
               <H1> >- Provable{$`(<H>; a: A >- e[a])} -->
               <H1> >- Provable{$`(<H> >- C{a. e[a]})}
      
      Plus you get the complete logic, containing all the rules
      that were defined (an no others).
      
         define foo_logic <--> [A; B; C; c_intro]
         define Provable{'e} <-->
            Itt_hoas_sequent_native!Provable{Sequent; foo_logic; 'e}
      
      I haven't proved any theorems, so we'll see how that goes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-06 18:18:30 -0800 (Sun, 06 Nov 2005)
Revision: 8117
Log message:

      OMake should be checked out from the 0.9.6.x branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-06 22:35:45 -0800 (Sun, 06 Nov 2005)
Revision: 8119
Log message:

      Minor fixes in the IO code. Still a long way to go.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 01:14:46 -0800 (Mon, 07 Nov 2005)
Revision: 8123
Log message:

      - env_arg.mli: use self-documentary type names (e.g. "Arg.usage_msg" instead
        of "string")
      
      - removed a little bit of unused code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 01:22:48 -0800 (Mon, 07 Nov 2005)
Revision: 8124
Log message:

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

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-11-07 17:49:13 -0800 (Mon, 07 Nov 2005)
Revision: 8125
Log message:

      Added a theorem in the object theory.
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 19:11:12 -0800 (Mon, 07 Nov 2005)
Revision: 8127
Log message:

      (Issue 543) Compute the full list of theories to build based on the
      inter-theory dependencies.
      
      Now that ITT is composed of a bunch of smaller subtheories, having to specify
      the full list of theories in mk/config became more annoying. This commit
      implements the notion of theory dependencies and uses it to compute the full
      list of theories to be compiled. Now setting THEORIES in mk/config to
      something like "poplmark/naive" should work, bringing in all the necessary
      dependencies.
      
      In order to work correctly, the theory/*/OMakefile:
      
      - MAY define or update the THEORY_DEPENCIES variable. This variable MUST
        contain an array of theory "names" (as before, the theory "name" is the
        directory name relative to $(ROOT)/theories). By default, THEORY_DEPENCIES
        is equal to "base"
      
      - SHOULD use either the Theory function (which takes a file list as an
        argument), or a VirtualTheory function (this takes a list of subdirectories
        as an argument and should be used for "virtual" theories that only bring
        together sub-theories, but do not contain any modules). Note that
        VirtualTheory overrides the THEORY_DEPENCIES variable, so any additonal
        modifications to THEORY_DEPENCIES in virtual theories (which usually
        shouldn't be necessary) need to go after the VirtualTheory call.
      
      - SHOULD NOT change the OCAMLINCLUDES variable (except for non-theory
        directories). The standard "Theory" function now sets OCAMLINCLUDES based on
        the value of THEORY_DEPENCIES, and if the resulting value is incorrect, it
        is usually a very good indication that THEORY_DEPENCIES is also incorrect.
      
      - SHOULD NOT use .SUBDIRS to bring in other theories; it should use
        THEORY_DEPENCIES or VirtualTheory mechanism instead.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-07 20:07:12 -0800 (Mon, 07 Nov 2005)
Revision: 8128
Log message:

      Added a Boolean beq_bterm{'t1; 't2} for alpha-equality
      ('t1 = 't2 in BTerm <=> (beq_bterm{'t1; 't2} && 't1 in BTerm && 't2 in BTerm)).
      
      Also added the tactic (tailIndT << 'l >>) for tail induction on
      *any* list, not just the variables.  Bah, my proofs in Itt_list2
      would have been much easier if I had proved this first.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 20:53:20 -0800 (Mon, 07 Nov 2005)
Revision: 8129
Log message:

      Aleksey & Alexei:
      
      - Simplified the induction axioms for integers and lists, deriving the
        original ones.
      
      - Annotated the induction rules for ints, nats, and lists with proper labels,
        increasing the list of labels that are considered to be "main" by thenMT.
      
      - Making progress re-verifying ITT Core axioms under pairwise functionality
        (but got stuck in Itt_int_ext, where the div_neg rule seems too suspicious).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 23:36:42 -0800 (Mon, 07 Nov 2005)
Revision: 8130
Log message:

      Centralized the nadling of the input search path.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-08 14:30:17 -0800 (Tue, 08 Nov 2005)
Revision: 8134
Log message:

      Making sure the THEORYNAME/THEORYDESCR mechanism plays nicely with the new
      THEORY_DEPENCIES feature.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-08 14:39:18 -0800 (Tue, 08 Nov 2005)
Revision: 8135
Log message:

      Tried making the THEORY_DEPENCIES code more rubust in presence of theory
      symlinks.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-08 14:56:54 -0800 (Tue, 08 Nov 2005)
Revision: 8138
Log message:

      More consistent error messages for values in mk/config
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-08 15:04:56 -0800 (Tue, 08 Nov 2005)
Revision: 8139
Log message:

      "THEORY_DEPENCIES" -> "THEORY_DEPS" (Oops, evils of too much cut&paste - I
      didn't, of course, mean to replicate a misspelling all over the place).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-08 15:23:45 -0800 (Tue, 08 Nov 2005)
Revision: 8140
Log message:

      This is like to be extremely contraversial.
      
      I added a "make_sequent" sequent, with an ML rewrite.
      
         make_sequent{'arg}{| x: Context{'e1}; y: Hypothesis{'e2['x]} >- 'concl['x; 'y] |}
      reduces to
         "sequent"{'arg;
             ['e1 @ [bind{length{'e1}; x. 'e2['x]}] @ nil]; 
             bind{length{'e1}; x. bind{y. 'concl['x; 'y]}}}
      
      My primary argument for doing so is that we want to reflect sequents as
      sequents, not something else.  However, since sequents are not primitive
      BTerms, and there are no induction forms defined for sequents in ITT,
      we have to do it primitively.  I realize this argument is not as
      strong as it should be.
      
      We need to be confident that this amounts to a definition.  I have not
      added the inverse rule because, among other things, it would have to
      be a conditional rewrite.
      
      This isn't just to make things pretty, I want to be able to use
      contexts in proofs.  For example, in Fsub, we would like a rule
      that looks as follows.
      
          Original FSub rule:
      
             <H>; x: ty1 >- e[x] in ty2 -->
             <H> >- lambda{x. e[x]} in TyFun{ty1; ty2} 
      
          Initial reflected version:
      
             <H1> >- 'H in CVar{0} -->
             <H1> >- 'ty1 in SOVar{|H|} -> ...
             <H1> >- Provable{make_sequent{| h: Context{'H}; x: Hypothesis{'ty1} >- e[x] in ty2|}} -->
             <H1> >- Provable{make_sequent{| h: Context{'H} >- lambda{x. e['x]} in TyFun{'ty1; 'ty2} |}
      
         Derived version:
             <H1> >- 'ty1 in SOVar{|H|} -> ...
             <H1> >- Provable{make_sequent{| h: <H>; x: Hypothesis{'ty1} >- e[x] in ty2|}} -->
             <H1> >- Provable{make_sequent{| h: <H> >- lambda{x. e['x]} in TyFun{'ty1; 'ty2} |}
      
      I admit, this "derived version" with real contexts may be a lost cause,
      but I'm not sure yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-08 19:27:00 -0800 (Tue, 08 Nov 2005)
Revision: 8146
Log message:

      The proof checkers are now (ProofStep -> bool) instead of (ProofStep -> univ[1]).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-08 19:43:28 -0800 (Tue, 08 Nov 2005)
Revision: 8147
Log message:

      Update the filter to use beq_ProofStep.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-08 19:57:25 -0800 (Tue, 08 Nov 2005)
Revision: 8148
Log message:

      Oops, I got a bit too aggressive on the Boolean proof checkers.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-09 00:19:55 -0800 (Wed, 09 Nov 2005)
Revision: 8149
Log message:

      - Made sure that documentation generator plays nicely with the new THEORY_DEPS
        mechanism.
      
      - Further clean-ups in the THEORY_DEPS implementation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-09 00:43:13 -0800 (Wed, 09 Nov 2005)
Revision: 8150
Log message:

      Finished implementing the .cmiz API
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-09 04:55:00 -0800 (Wed, 09 Nov 2005)
Revision: 8151
Log message:

      More TheoryDocument fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-09 16:14:18 -0800 (Wed, 09 Nov 2005)
Revision: 8153
Log message:

      Slight clarification.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-10 10:45:48 -0800 (Thu, 10 Nov 2005)
Revision: 8159
Log message:

      Proof checking is now completely decidable.
      
      A proof checker has the type
      
          ProofStep * ProofStepWitness -> bool
      
      where
      
          ProofStep == Sequent list * Sequent
          ProofStepWitness == BTerm list * BTerm list list
      
      I haven't converted Filter_reflection yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-10 12:52:28 -0800 (Thu, 10 Nov 2005)
Revision: 8161
Log message:

      Added the new explicit witness to Filter_reflection.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-11 03:31:16 -0800 (Fri, 11 Nov 2005)
Revision: 8162
Log message:

      Added a rewrite lemma to reduce: length{tail{'l; 'n} ~ 'n
      This significantly simplifes the proofs of the tail induction lemmas.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-11 05:10:57 -0800 (Fri, 11 Nov 2005)
Revision: 8163
Log message:

      Trying to make "AutoComplete" handling more efficient. In "AutoComplete" mode
      we want to abort on first goal that we can not complete, and not go all the
      way on all the branches and only then check whether all of them are complete.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-11 05:37:16 -0800 (Fri, 11 Nov 2005)
Revision: 8164
Log message:

      Added a comment pointing to issue 549.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-11 05:46:17 -0800 (Fri, 11 Nov 2005)
Revision: 8165
Log message:

      Adding omegaT to intro resource (with AutoComplete) for inequality
      conclusions.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-11 11:43:56 -0800 (Fri, 11 Nov 2005)
Revision: 8166
Log message:

      Proved some wf theorems.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-11-11 12:11:04 -0800 (Fri, 11 Nov 2005)
Revision: 8167
Log message:

      Some documentation on object theory

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-11-11 15:13:52 -0800 (Fri, 11 Nov 2005)
Revision: 8168
Log message:

      Proved that BTerm in U[i], and some other wf-theorems

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-12 11:18:07 -0800 (Sat, 12 Nov 2005)
Revision: 8169
Log message:

      Added a moveHypT tactic (based on the Itt_struct.exchange rule).
      
      moveHypT i j takes the hypothesys number i and moves is so that the _new_
      position of the hyp is j.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-12 11:22:23 -0800 (Sat, 12 Nov 2005)
Revision: 8170
Log message:

      MP_DEBUG=spell fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-12 15:47:42 -0800 (Sat, 12 Nov 2005)
Revision: 8171
Log message:

      Restructured the file, making it more modular (IMHO)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-12 16:20:23 -0800 (Sat, 12 Nov 2005)
Revision: 8172
Log message:

      When a negative "sequent context" argument was too small (the absolute value
      too large), we were raising an "Invalid Argument: index out of bounds" instead
      of a proper RefineError.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-12 16:28:46 -0800 (Sat, 12 Nov 2005)
Revision: 8173
Log message:

      Updated the irrefl_EliminationT tactic to work correctly with negative
      arguments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-12 17:29:04 -0800 (Sat, 12 Nov 2005)
Revision: 8174
Log message:

      Wrote a simple program for merging two .prla files. This is:
       - very approximate
       - completely untested
       - not built by default.
      
      To try it out, run "omake bin/merge_prla" followed by
      bin/merge_prla input1.prla input2.prla output.prla
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-12 19:06:02 -0800 (Sat, 12 Nov 2005)
Revision: 8175
Log message:

      Preparing to rename Itt_hoas_sequent_native to Itt_hoas_sequent.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-12 19:15:54 -0800 (Sat, 12 Nov 2005)
Revision: 8176
Log message:

      Renamed Itt_hoas_sequent_native to Itt_hoas_sequent.
      The name was getting laborious.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-14 04:08:48 -0800 (Mon, 14 Nov 2005)
Revision: 8178
Log message:

      Updated the handling of matching of sequent contexts (sequent context
      instances in redices), removing the potential for some bogus error from it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-14 04:18:53 -0800 (Mon, 14 Nov 2005)
Revision: 8179
Log message:

      Forgot to commit the updated filter_magic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-14 05:47:45 -0800 (Mon, 14 Nov 2005)
Revision: 8180
Log message:

      Fixed refiner's term extraction.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-15 01:38:39 -0800 (Tue, 15 Nov 2005)
Revision: 8184
Log message:

      Derived a slightly more convenient (in my and Alexei's opinion) induction rule
      for integers.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-15 17:16:05 -0800 (Tue, 15 Nov 2005)
Revision: 8186
Log message:

      A number of improvements in the .prla merging algorithm.
      
      In particular, it now handles cases where one file has a primitive proof and
      another - a real interactive one. In this case the "merge_prla" program will
      always drop the primitive one and keep the interacrive one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-15 23:26:16 -0800 (Tue, 15 Nov 2005)
Revision: 8188
Log message:

      - normalizeC should not call reduceC in the end, since reduceC might be doing
        something incompatible with arithT's or omegaT's assumptions.
      
      - updated ascii_io to be more efficient for large files (fixed a few places
        where it was not tail-recursive).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-16 02:41:48 -0800 (Wed, 16 Nov 2005)
Revision: 8189
Log message:

      - Made multiplication a defined function (not an axiomatized one). Now we only
        have a single primitive rewrite for multiplication of numerals, everything
        else is derived.
      
      - Proved a bunch of itt_int_ext theorems that had not been proven yet.
      
      - Updated the parser so that <<-1>> is parsed as <<number[-1:n]>>, not
        <<minus{number[1:n]}}>>
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-16 05:19:54 -0800 (Wed, 16 Nov 2005)
Revision: 8190
Log message:

      The .prla got corrupted. :-( Committing it again.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-16 19:32:27 -0800 (Wed, 16 Nov 2005)
Revision: 8192
Log message:

      Partition the files into
         1. sequents
         2. proofs (proofs are not dependent on sequents in general)
         3. and sequent proofs
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-11-17 21:48:18 -0800 (Thu, 17 Nov 2005)
Revision: 8194
Log message:

      1. Two minor optimizations for early detection of non-unifiable equations. Unfortunately, they do not help with the slow example in poplmark/naive.
      
      2. Added a counter (approximate) for recursive calls of path_checker - for debug purposes

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-17 22:33:09 -0800 (Thu, 17 Nov 2005)
Revision: 8195
Log message:

      Slight optimization of Yegor's "quick incompatibility test".
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 12:15:40 -0800 (Tue, 22 Nov 2005)
Revision: 8197
Log message:

      Added the context terms in extensions/meta_context_term
      
      This approach preserves the sequent argument down to the
      base case (so the argument is more like a turnstile
      modifier).  This way, there is no need for a special
      type of "core" sequent, all sequents have the usual
      form.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 17:10:47 -0800 (Tue, 22 Nov 2005)
Revision: 8199
Log message:

      Working on meta-implies.  Still working on the meta_dT tactic.
      
      Questions:
         1. We had thought to limit the meta-logic to third order.
            We can still do it, but is it worth it?
         2. I plan to add the meta-structural rules for
            cut, thinning, and copy.
      
      High-level arguments that these are conservative extensions.
      
         cut: prove cut-elimination.  For each use of the cut rule
            S1 --> ... --> Sn --> R
            S1 --> ... --> Sn --> R --> T
            -----------------------------
            S1 --> ... --> Sn --> T
      
            prove the 2 upper rules as separate theorems.
         thinning: state the rule without the thinned assumption
            and prove that instead.  The unthinned rule follows
            trivially.
         higher-order rules: reduce an order n inference to
            order n-1 by stating the introduction and elimination
            rules as separate theorems.
      
            For example, consider the following elimination rule.
      
               S1 --> ... --> Sn --> R1
               S1 --> ... --> Sn --> R2 --> T
               ---------------------------------------
               S1 --> ... --> Sn --> (R1 --> R2) --> T
      
            Suppose we have a proof of the lower rule.
            For each use of the elimination rule, prove 3
            separate theorems.
      
               ... --> R1
               ... --> R1 --> R2
               ... --> R2 --> T
      
      Also, the proof that teleportation is a conservative extension is
      the same.  Suppose we proved a theorem without contexts, but
      we used teleportation in the argument.  For each use of the
      teleportation rule on a sequence of hyps of length n,
      prove (n + 1) theorems, including the base case and n
      step theorems.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 17:41:51 -0800 (Tue, 22 Nov 2005)
Revision: 8200
Log message:

      The basic meta_dT works, but I haven't corrected the 
      resource annotations yet.
      
      The extracts are currently wrong.  I have to figure out
      the arguments to the extract function (like what a
      subgoal extract looks like).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 18:07:51 -0800 (Tue, 22 Nov 2005)
Revision: 8201
Log message:

      Added the meta-cut rule.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 19:55:14 -0800 (Tue, 22 Nov 2005)
Revision: 8202
Log message:

      Added the structural rules for the meta-logic, including cut and thinning.
      
      Unfortunately, these rules are ML rules, but only because we can't
      express the extract properly.
      
      Yes I know, meta-logical power is like a siren, and we can become
      entralled by her beauty--to our own peril.
      
      Still it would be cool if we could write down this stuff the right
      way.  For example, thinning.
      
         <H>; <J> --> E
         -----------------
         <H>; A; <J> --> E
      
      Here, <H> and <J> correspond to lists of assumptions.
      Crazy, yes.  At least they are not dependent:/
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-23 09:36:43 -0800 (Wed, 23 Nov 2005)
Revision: 8204
Log message:

      Generalized the type of ML extract functions.  The previous
      definitions had assumed that the assumptions (and their
      arities) was unchanged.
      
      Added extracts for all the ML rules.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-23 11:35:19 -0800 (Wed, 23 Nov 2005)
Revision: 8205
Log message:

      Minor changes.  Meta_implies should depend on Meta_struct, not
      vice-versa.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-23 12:20:42 -0800 (Wed, 23 Nov 2005)
Revision: 8206
Log message:

      Added the minimal boilerplate for context induction.
      The specification is the hard part.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-23 14:18:22 -0800 (Wed, 23 Nov 2005)
Revision: 8207
Log message:

      Trivial changes while I work out a plan.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-23 18:07:40 -0800 (Wed, 23 Nov 2005)
Revision: 8209
Log message:

      Added the TermMan.all_vars_info function.  The Perl script isn't
      configured for the type, so Refiner_debug will abort with
      a run-time error.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-23 20:33:25 -0800 (Wed, 23 Nov 2005)
Revision: 8210
Log message:

      Updating Refiner_debug to match the latest Jason's changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-25 15:26:14 -0800 (Fri, 25 Nov 2005)
Revision: 8211
Log message:

      Initial context induction tactics.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-25 15:46:42 -0800 (Fri, 25 Nov 2005)
Revision: 8212
Log message:

      Theory rearrangement.
         base -> meta/base
         extensions -> meta/extensions
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-25 19:22:16 -0800 (Fri, 25 Nov 2005)
Revision: 8215
Log message:

      Deriving the sequent_ind reight reduction.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 08:06:49 -0800 (Sat, 26 Nov 2005)
Revision: 8216
Log message:

      Proved right-reduction for sequent_ind{...}
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 09:30:05 -0800 (Sat, 26 Nov 2005)
Revision: 8217
Log message:

      Proved context thinning and context exchange.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 12:05:50 -0800 (Sat, 26 Nov 2005)
Revision: 8218
Log message:

      Added some defined versions of sequent_ind{...}
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 12:08:26 -0800 (Sat, 26 Nov 2005)
Revision: 8219
Log message:

      Rename the derived terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 13:03:50 -0800 (Sat, 26 Nov 2005)
Revision: 8221
Log message:

      Added the initial vector-list theory.
      Unfortunately, it looks like I'm hitting a rewriter bug.
      See Itt_vec_list1.reduce_vlist_cons for an example.
      
      Here is the failing fragment.
      
         happly{hlambda{'e; x. sequent_ind{... Sequent{ <J['x]> >- ... }}; 'e}
         --> sequent_ind{... Sequent{ <J['x]> >- ... }}
      
      In other words, the 'x in <J['x]> is not getting substituted.
      The two "x"s *should* be the same variable.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 14:13:09 -0800 (Sat, 26 Nov 2005)
Revision: 8222
Log message:

      Ouch!  Term_ds had an unfortunate typo.  This could potentially
      break a lot of proofs, but I haven't checked it.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 16:58:55 -0800 (Sat, 26 Nov 2005)
Revision: 8223
Log message:

      Considering reformulating recursive lists.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-26 17:27:26 -0800 (Sat, 26 Nov 2005)
Revision: 8224
Log message:

      Proved basic theorems for vector lists.
      
      For now, the lists are dependent.  So, for example,
         vlist{| x: 1; y: 'x +@ 1 |} <--> vlist{| 1; 2 |}
      
      The dependencies produce complications, as you might
      imagine.  However, there doesn't seem to be any payoff
      in coding "nondependent" lists by substituting a constant
      (like it) for the hyp vars, so I'll stick with this for now.
      
      Likely, for real non-dependent lists, we would need contexts
      with no self-dependencies.  This might not help all that much
      either.
      
      Note that dependent values can be extremely useful in general,
      especially for coding things like mutually recursive functions
      and mutually recursive types.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-27 14:45:04 -0800 (Sun, 27 Nov 2005)
Revision: 8225
Log message:

      Proved that the second phase of sequent reflection is well-formed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-27 19:37:51 -0800 (Sun, 27 Nov 2005)
Revision: 8227
Log message:

      Partial progress on the front-end to the sequent definition.
      However, it is now clear (see email <438A792E.50709@cs.caltech.edu>
      in metaprl-research) that I can't use the fundamental theorem of
      HOAS.  Instead, we'll have to define vector-bind terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-28 11:09:57 -0800 (Mon, 28 Nov 2005)
Revision: 8233
Log message:

      Proved the final wf goal.
      
         [wf] std_sequent{| <H> >- C |} in StdSequent{0} -->
         bsequent{| <H> >- C |} in Sequent
      
      Sequent is the "ugly" sequent triple (BTerm * BTerm list * BTerm),
      where the depths are increasing.
      
      The wf subgoal is unfortunate, but it may be the best we can do.
      What we really want to say is that all the terms in the sequent
      are "closed" wrt their dependencies, but this is impossible.
      
      So this approach is to prove that the std-style sequent is
      well-formed.  There are lemmas for many of the cases.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-28 12:57:59 -0800 (Mon, 28 Nov 2005)
Revision: 8234
Log message:

      Stated a provability theorem, just to see what it looks like.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-28 18:55:59 -0800 (Mon, 28 Nov 2005)
Revision: 8239
Log message:

      Addressing some of the comments by the second reviewer.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-28 19:25:51 -0800 (Mon, 28 Nov 2005)
Revision: 8241
Log message:

      Added couple of paragraphs to the end of the "Summary and Future Work"
      sect6ion describing our latest work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-28 19:29:21 -0800 (Mon, 28 Nov 2005)
Revision: 8242
Log message:

      Fixing a few typos

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-29 18:33:16 -0800 (Tue, 29 Nov 2005)
Revision: 8243
Log message:

      HOSC paper: Addressing another reviewer's comment

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-29 18:38:32 -0800 (Tue, 29 Nov 2005)
Revision: 8244
Log message:

      HOSC paper: fixing couple of typos

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-30 03:25:29 -0800 (Wed, 30 Nov 2005)
Revision: 8245
Log message:

      HOSC paper: addressing couple of more reviewer's comments

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 08:15:28 -0800 (Wed, 30 Nov 2005)
Revision: 8246
Log message:

      Committing some half-completed work before we lose it.  The
      Itt_hoas_sequent_term1 sequent-coding converts a sequent to ugly form
      without any wf subgoals, using a bind-pushing trick similar to the one
      in Itt_hoas_debruijn.  The arguments have to be carefully constructed,
      it is about half done.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 08:18:36 -0800 (Wed, 30 Nov 2005)
Revision: 8247
Log message:

      Further cleanup.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-30 11:55:58 -0800 (Wed, 30 Nov 2005)
Revision: 8248
Log message:

      HOSC paper: "CloseRec is an administrative ter.m"
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 12:30:40 -0800 (Wed, 30 Nov 2005)
Revision: 8249
Log message:

      Added a section on the runtime.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 14:12:43 -0800 (Wed, 30 Nov 2005)
Revision: 8250
Log message:

      More changes, added a reference to A-normal form.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-30 14:42:06 -0800 (Wed, 30 Nov 2005)
Revision: 8252
Log message:

      HOSC paper: spelling

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 14:53:38 -0800 (Wed, 30 Nov 2005)
Revision: 8253
Log message:

      Recent changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-30 17:23:05 -0800 (Wed, 30 Nov 2005)
Revision: 8254
Log message:

      Jason's final copy.