Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 10:51:13 -0800 (Wed, 01 Mar 2006)
Revision: 8807
Log message:

      - Derived a few Itt_union rules that used to be primitive (for no good
        reason).
      - A few minor changes in "sub" resource improvements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 12:54:25 -0800 (Wed, 01 Mar 2006)
Revision: 8808
Log message:

      Better usage of subtyping in nthHypT and dT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 18:37:23 -0800 (Wed, 01 Mar 2006)
Revision: 8811
Log message:

      When matching old subproofs with new subgoals during proof expansion, try
      keeping the old variable names in the goal intact. To do that, if the old
      subgoal (w/o the assumptions) is alpha equal to the new one, replace the goal
      (w/o the assumptions) with the old one in the new tactic arg.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 18:52:00 -0800 (Wed, 01 Mar 2006)
Revision: 8812
Log message:

      Use the labels mechanism instead of the "SelectOption 5" hack to control
      whether the "intensional" wf rules for list operations should be allowed. The
      label that controls these rules is "intensional_wf_option" (prohibited by
      default).
      
      P.S. The intentional wf rules have the form
         l in list --> all_list{l; x. ... } --> ...
      while the extensional ones have the form
         l in A list --> all x: A. ... --> ...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 19:09:40 -0800 (Wed, 01 Mar 2006)
Revision: 8813
Log message:

      Be smarter when using subtyping in nthHypT and dT 0 (improves the code I've
      committed in rev 8808).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 19:59:51 -0800 (Wed, 01 Mar 2006)
Revision: 8814
Log message:

      Added couple of nth_hyp annotations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 21:24:24 -0800 (Wed, 01 Mar 2006)
Revision: 8815
Log message:

      Added the missing wf condition to subtype_axiomFormation and fixed all the
      proofs that broke because of it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 23:16:34 -0800 (Wed, 01 Mar 2006)
Revision: 8816
Log message:

      Thin out "0 in nat"
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-01 23:46:16 -0800 (Wed, 01 Mar 2006)
Revision: 8817
Log message:

      Manually proved the elimination rule in reflect_pmn_core_terms; it's just a temporary solution for now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 00:12:57 -0800 (Thu, 02 Mar 2006)
Revision: 8818
Log message:

      Use the nilSqequal lemma ( l = [] in T List --> l ~ [] ) in *substT tactics
      (to avoid unnecessary wf subgoals).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 01:19:46 -0800 (Thu, 02 Mar 2006)
Revision: 8819
Log message:

      Removed an unnecessary wf condition.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 01:43:59 -0800 (Thu, 02 Mar 2006)
Revision: 8820
Log message:

      Removing an unnecessary wf condition.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 02:28:23 -0800 (Thu, 02 Mar 2006)
Revision: 8821
Log message:

      Added "vflatten{| A |} <--> A" to reduce.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 02:42:58 -0800 (Thu, 02 Mar 2006)
Revision: 8822
Log message:

      Call simpleReduceT before using forwardT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 10:12:28 -0800 (Thu, 02 Mar 2006)
Revision: 8823
Log message:

      Removed some unnecessary wf conditions and replaced some of the proofs that
      relied on the crw bug with ones that do not.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 16:49:39 -0800 (Thu, 02 Mar 2006)
Revision: 8824
Log message:

      Added TermAddr.null_address to TermAddr signature.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 17:56:02 -0800 (Thu, 02 Mar 2006)
Revision: 8825
Log message:

      Exclude the obsolete directory from the build.
      
      This directory has a lot of proofs that do not play nicely with the fixed
      refiner and I'd rather just ignore them (at least for now).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-02 18:07:47 -0800 (Thu, 02 Mar 2006)
Revision: 8826
Log message:

      Revised the proof with the SimpleStep elimination lemmas; also some other improvements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 18:36:59 -0800 (Thu, 02 Mar 2006)
Revision: 8827
Log message:

      Xin's recent commit made the weird caseAnalysis_7 lemma unnecessary, deleting.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 18:45:26 -0800 (Thu, 02 Mar 2006)
Revision: 8828
Log message:

      Fixing a very nasty refiner bug, where the conditional rewrites were being
      applied incorrectly.
      
      This breaks 15 proofs (and makes everything that depend on them suspect).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 20:54:28 -0800 (Thu, 02 Mar 2006)
Revision: 8829
Log message:

      All the Itt_list_sloppy theorems were valid; I was able to fix all the proofs
      that broke.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-02 20:58:31 -0800 (Thu, 02 Mar 2006)
Revision: 8830
Log message:

      Hmm, some people told me the record theory was mature.  So
      far, I kind of agree, but the people never proved anything
      about type universes:(
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 21:04:09 -0800 (Thu, 02 Mar 2006)
Revision: 8831
Log message:

      Added a missing wf condition, making the original proof replay.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 23:15:19 -0800 (Thu, 02 Mar 2006)
Revision: 8832
Log message:

      My initial fix for the crw bug was not quite right either. Even this one is
      not correct, strictly speaking, but it will only be wrong on cases that we do
      not have (when we have the same context both on the hyp list of the outer
      judgment sequent and nested in one of the clause of that sequent).
      
      The correct fix is relatively simple, but will take at least a few hours -
      will do it after the paper deadlines.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 00:33:37 -0800 (Fri, 03 Mar 2006)
Revision: 8833
Log message:

      Fixed a few proofs that were broken by the "crw bug" fix.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 01:05:21 -0800 (Fri, 03 Mar 2006)
Revision: 8834
Log message:

      Tiny no-op code clean-up.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 01:18:09 -0800 (Fri, 03 Mar 2006)
Revision: 8835
Log message:

      A little progress towards fixing the forward-chaining rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 01:35:43 -0800 (Fri, 03 Mar 2006)
Revision: 8836
Log message:

      Adding the wf conditions that we will need to fix the proofs once the
      eta-expansion stuff is there.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-03 13:06:45 -0800 (Fri, 03 Mar 2006)
Revision: 8838
Log message:

      Added the eta module.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 14:28:12 -0800 (Fri, 03 Mar 2006)
Revision: 8839
Log message:

      Itt_hoas_eta
      - Fixed a few of the broken statements and added a few more
      - Proved all the lemma (every single proof is a simple byDefT, as this theory
        just wraps existing lemmas into an eta form).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 17:31:12 -0800 (Fri, 03 Mar 2006)
Revision: 8840
Log message:

      More accurate repeatT.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-03 17:48:41 -0800 (Fri, 03 Mar 2006)
Revision: 8841
Log message:

      Added some useful lemmas.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 18:18:46 -0800 (Fri, 03 Mar 2006)
Revision: 8842
Log message:

      Optimized the Refine.msequent_alpha_equal function.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 18:32:03 -0800 (Fri, 03 Mar 2006)
Revision: 8843
Log message:

      "Eta-converted" the Itt_hoas_bterm_wf theory. Still have to "eta-convert" the
      Itt_hoas_sequent_bterm and Itt_hoas_sequent_term ones.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-03 18:59:12 -0800 (Fri, 03 Mar 2006)
Revision: 8844
Log message:

      Made 't depend on 'x in eta_bind and eta_bind1.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-03 19:33:23 -0800 (Fri, 03 Mar 2006)
Revision: 8845
Log message:

      Minor optimization

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-04 21:58:59 -0800 (Sat, 04 Mar 2006)
Revision: 8846
Log message:

      Rearranged things a bit

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 09:57:31 -0800 (Sun, 05 Mar 2006)
Revision: 8847
Log message:

      Jason's relarex HOAS works great!
      
      Now most of the reflection stuff works again (and no eta ;-) ), except for:
      
      /itt_hoas_sequent_bterm/reduce_is_sequent_bterm_core_hyp
      /reflect_pmn_core_terms/intro_term_TyAll
      /reflect_pmn_core_terms/intro_term_Lambda
      /reflect_pmn_core_terms/intro_term_TyLambda
      
      Will look into those later today.
      
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 15:30:08 -0800 (Sun, 05 Mar 2006)
Revision: 8848
Log message:

      Added a few items to the typeinf resource.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 15:37:24 -0800 (Sun, 05 Mar 2006)
Revision: 8849
Log message:

      Making the Dtactic.intro_item type abstract.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 15:54:28 -0800 (Sun, 05 Mar 2006)
Revision: 8850
Log message:

      Turned the intro_item type into a record type.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 17:50:15 -0800 (Sun, 05 Mar 2006)
Revision: 8851
Log message:

      Implemented full fall-back for the intro resource. Now dT 0 will fall back to
      less specific matches if the tactics for the more specific matches fail
      _unless_ the tactic was specifically added as a "last resort" one (using
      "wrap_intro ~fall_through:false").
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 17:51:33 -0800 (Sun, 05 Mar 2006)
Revision: 8852
Log message:

      Previous commit had a typo, sorry.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 18:57:35 -0800 (Sun, 05 Mar 2006)
Revision: 8853
Log message:

      Fixed couple of broken proofs. Most of the reflection proofs are now fully
      grounded!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 19:40:32 -0800 (Sun, 05 Mar 2006)
Revision: 8854
Log message:

      Fixed the remaining three broken reflection proofs. Now all the reflection
      proofs (except for the elim_pmn_core_judgments, which we never finished) are
      fully grounded.
      
      We are back in business!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 19:43:59 -0800 (Sun, 05 Mar 2006)
Revision: 8855
Log message:

      Moving eta to obsolete, as we've managed to make things work without it.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-09 13:44:47 -0800 (Thu, 09 Mar 2006)
Revision: 8864
Log message:

      Some modifications to make proving the elimination rule in reflect_pmn_core_terms a little easier.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-09 14:56:29 -0800 (Thu, 09 Mar 2006)
Revision: 8865
Log message:

      Somehow, my previous commit can compile on my machine, but is uncomplilable by the cron. Try if this works.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-10 11:18:59 -0800 (Fri, 10 Mar 2006)
Revision: 8866
Log message:

      Add the intial rule for multi-part elimination.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-10 11:32:08 -0800 (Fri, 10 Mar 2006)
Revision: 8867
Log message:

      Define a predicate proof_check{'r; 'assums; 'goal; 'witness} that
      says that a proof step checks against rule 'r.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-10 12:10:16 -0800 (Fri, 10 Mar 2006)
Revision: 8868
Log message:

      Add the initial SimpleStep case analysis rule.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-10 17:00:39 -0800 (Fri, 10 Mar 2006)
Revision: 8869
Log message:

      Added a genHypT tactic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-10 19:52:00 -0800 (Fri, 10 Mar 2006)
Revision: 8870
Log message:

      Added the ProofCheck lemmas.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-13 14:10:40 -0800 (Mon, 13 Mar 2006)
Revision: 8882
Log message:

      Squash is decidable when the type if decidable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-13 14:50:59 -0800 (Mon, 13 Mar 2006)
Revision: 8883
Log message:

      Need to use Lm_list_util.for_all2 instead of List.for_all2 when list lengths
      might not match.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-13 15:33:59 -0800 (Mon, 13 Mar 2006)
Revision: 8884
Log message:

      - Changed the SimpleStep definition to use ProofCheck and the ValidStep
        definition to use SimpleStep.
      
      - Proved stronger (dependent) elimination rules for the SimpleStep.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-15 19:39:05 -0800 (Wed, 15 Mar 2006)
Revision: 8896
Log message:

      Changes for compiling with strict quoting.
      The changes are backwards-compatible.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-15 22:45:10 -0800 (Wed, 15 Mar 2006)
Revision: 8905
Log message:

      Added elimination rules for let_sovar and let_cvar, which made proving elim_pmn_core_terms much easier.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-15 23:17:32 -0800 (Wed, 15 Mar 2006)
Revision: 8907
Log message:

      Some improvement; made the elimination rule proof a little more general.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-16 12:08:26 -0800 (Thu, 16 Mar 2006)
Revision: 8912
Log message:

      Last revision was a mistake (this is awk, not fsubst).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-16 16:43:54 -0800 (Thu, 16 Mar 2006)
Revision: 8916
Log message:

      MLDEBUG_PATH depends on project-directories, not dependencies.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-16 19:04:04 -0800 (Thu, 16 Mar 2006)
Revision: 8925
Log message:

      Working on reflecting proper rules in Poplmark.
      Unfortunately, need a stronger definition of sequent
      types.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-17 10:40:30 -0800 (Fri, 17 Mar 2006)
Revision: 8926
Log message:

      Added "hyp cases" types.  Probably soon to be modified, see message
      on metaprl-research to be posted soon.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-17 14:51:03 -0800 (Fri, 17 Mar 2006)
Revision: 8927
Log message:

      Use "Attempt #2", which is equivalent to "Attempt #1", but
      safer, although somewhat more complicated when reflected.
      
      The Pmn_core_logic now at least passes the type checker.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-17 18:33:28 -0800 (Fri, 17 Mar 2006)
Revision: 8928
Log message:

      Added support for xquote0 on sequents (untested).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-17 19:09:24 -0800 (Fri, 17 Mar 2006)
Revision: 8929
Log message:

      Declare terms for rule names and the logic name in .cmiz (untested).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-17 19:33:20 -0800 (Fri, 17 Mar 2006)
Revision: 8930
Log message:

      Minor touchup on Aleksey's fix.
      
      I think the signature code for Rule/Rewrite/CondRewrite
      are premature, but no big deal currently.  Was there some
      other intent here?
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-17 19:59:44 -0800 (Fri, 17 Mar 2006)
Revision: 8931
Log message:

      For terms declared in the signature, say
      
          declare foo{...}
      
      also declare the proof-checking term in the reflected theory
      
          declare term_foo
      
      Long term, we have the issue of dealing with privately-declared
      terms.  Short-term, we will soon have the issue of dealing with
      privately-declared rules (which are our usual style).
      
      I'm not sure what to do, but perhaps we'll just declare the rules
      in the interface too for now.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-17 20:35:29 -0800 (Fri, 17 Mar 2006)
Revision: 8932
Log message:

      Starting work on reflecting proper rules.  Will finish up
      this part tomorrow morning.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-17 23:15:45 -0800 (Fri, 17 Mar 2006)
Revision: 8933
Log message:

      Added a test file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 10:03:57 -0800 (Sat, 18 Mar 2006)
Revision: 8934
Log message:

      NOTE: the magic number has changed.  The change is
      binary-compatible, but you should save your work anyway.
      
      This adds support for reflecting proper rules.
      Reflect_pmn_core_logic now compiles.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 13:11:12 -0800 (Sat, 18 Mar 2006)
Revision: 8935
Log message:

      
      Added theory inheritance.
      
      This also changes the elimination rules to include the
      sub-logics.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 13:46:14 -0800 (Sat, 18 Mar 2006)
Revision: 8936
Log message:

      Added support for interactive theorems.  This adds a reflected
      intro rule that corresponds to the theorem, but otherwise
      the rule is not considered to be part of the logic.
      
      Also added Pmn_core_terms_test2 that restates the theorem
      in Pmn_core_terms_test.  We should probably work on this one.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 15:03:06 -0800 (Sat, 18 Mar 2006)
Revision: 8937
Log message:

      Added the ProvableJudgment{'logic; 't} that requires that the term
      't be a Judgment.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 19:04:16 -0800 (Sat, 18 Mar 2006)
Revision: 8938
Log message:

      Reflect the sequent declarations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 20:21:53 -0800 (Sat, 18 Mar 2006)
Revision: 8939
Log message:

      Working on display forms.  Need to commit before I can move files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 20:54:01 -0800 (Sat, 18 Mar 2006)
Revision: 8940
Log message:

      Added "smart" display forms for quoted terms.
      
      This removes display-form translation in Filter_reflect.
      The display of quoted terms uses the $`/$'[d]/$,
      syntax.
      
      $`        : mk_term{...}
      $'[d]     : mk_bterm{d; ...}
      $,        : unquoted term
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-18 21:04:05 -0800 (Sat, 18 Mar 2006)
Revision: 8941
Log message:

      Forgot to display variables correctly.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-19 09:42:25 -0800 (Sun, 19 Mar 2006)
Revision: 8942
Log message:

      Generate the reflected interface file reflect_foo.ppi from
      the implementation file foo.cmoz.
      
      Basically, when we reflect a theory, we want _everything_.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-19 12:27:58 -0800 (Sun, 19 Mar 2006)
Revision: 8943
Log message:

      Made some progress proving wf for elimination-style rules.
      See Reflect_itt_hoas_base_theory.wf_rule_meta_axiom.
      
      We have a two hard subgoals, and a few junk ones.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-20 09:44:55 -0800 (Mon, 20 Mar 2006)
Revision: 8944
Log message:

      Half-finished theorems for proving
      
         bind{'n; x. substl{'y; nth_prefix{'x; 'm}}} in BTerm
      
      The main theorem needs an extra lemma
         Itt_hoas_lof.normalize_mk_bterm_subst
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-20 17:53:00 -0800 (Mon, 20 Mar 2006)
Revision: 8945
Log message:

      Adding detection of stale binaries in directory that no longer has sources
      (after sources have been moved to another directory).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-20 21:02:29 -0800 (Mon, 20 Mar 2006)
Revision: 8946
Log message:

      Almost done proving the nth_prefix lemma.  Grinding through the
      base case.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-24 16:02:19 -0800 (Fri, 24 Mar 2006)
Revision: 8948
Log message:

      The ge_elim resource options should be optional.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-24 16:07:57 -0800 (Fri, 24 Mar 2006)
Revision: 8949
Log message:

      Couple of small lemmas

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-24 17:56:32 -0800 (Fri, 24 Mar 2006)
Revision: 8950
Log message:

      Use relaxed reasoning in proofRuleAuxWFT tactic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-25 14:22:12 -0800 (Sat, 25 Mar 2006)
Revision: 8951
Log message:

      FOL should be using nth_hyp.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-25 14:24:29 -0800 (Sat, 25 Mar 2006)
Revision: 8952
Log message:

      Minor: proactively normalize BTerm{'n +@ 0 } and CVar{'n +@ 0}
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-25 14:47:59 -0800 (Sat, 25 Mar 2006)
Revision: 8953
Log message:

      Made some progres on the nth_prefix lemma. Now it remains to prove bind_subst_nth_prefix_wf_aux0; unfortunately, I couldn't figure out how. bind_substl_nth_prefix_nth_suffix and bind_substl_nth_prefix can be ignored.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-27 08:59:07 -0800 (Mon, 27 Mar 2006)
Revision: 8955
Log message:

      Proved a bunch of theorems about well-formedness of
      reflected terms.  This solves most of the intro proofs
      for elimination-style rules.  I'll finish it off soon.
      
      There were a couple of conflicts with .prla files.
      I've renamed my copies to .prla2.  I'll see what I can
      do to merge them.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-27 22:07:21 -0800 (Mon, 27 Mar 2006)
Revision: 8956
Log message:

      More progress on wf theorems.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-27 23:31:00 -0800 (Mon, 27 Mar 2006)
Revision: 8957
Log message:

      Added some lemmas. Itt_hoas_proof_ind.provable_sub is unfinished yet.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-29 07:40:37 -0800 (Wed, 29 Mar 2006)
Revision: 8961
Log message:

      Almost finished with the lemmas for the elim-style rules,
      just one annoying one left.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-29 15:30:58 -0800 (Wed, 29 Mar 2006)
Revision: 8962
Log message:

      Finally proved the lemmas about SubLogic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-29 19:11:38 -0800 (Wed, 29 Mar 2006)
Revision: 8963
Log message:

      In assumption 
         [main] sequent { ...; u: BTerm{'d}; bdepth{'u} = 'd in int; ... >- ... }
       - The second hyp is redundant.
       - The current policy is to avoid the explicit "main" labels.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-29 19:58:55 -0800 (Wed, 29 Mar 2006)
Revision: 8964
Log message:

      (Re: Rev 8943) Minor proof simplification.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-03-29 22:21:12 -0800 (Wed, 29 Mar 2006)
Revision: 8965
Log message:

      This finishes the intro forms of elimination-style rules.  There is
      a bug in term_match_table (I believe) that requires some manual coding
      of resources that have sequent patterns.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 00:37:46 -0800 (Thu, 30 Mar 2006)
Revision: 8966
Log message:

      Added limited fallback to reduceC. ReduceC used to only try the very firts
      match. Now it will try all matches for the most specific pattern. It still
      will not fall back from more specific to less specific matches.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 02:38:52 -0800 (Thu, 30 Mar 2006)
Revision: 8967
Log message:

      Small optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 05:17:38 -0800 (Thu, 30 Mar 2006)
Revision: 8968
Log message:

      - Rewrote the forward-chainer:
        - to be more efficient (less idT calls, etc)
        - to more aggressively prohibit "no progress" steps
        - to thin out dups during forward chaining (where we already know that they
          are dups)
      
        This sped up status-all by almost a third!
      
      - Fixed the broken proofs in itt_hoas_sequent_term_wf.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 06:22:39 -0800 (Thu, 30 Mar 2006)
Revision: 8969
Log message:

      Small optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 06:51:45 -0800 (Thu, 30 Mar 2006)
Revision: 8970
Log message:

      Thin some "useless" hyps during forward chaining.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 11:03:17 -0800 (Thu, 30 Mar 2006)
Revision: 8971
Log message:

      Proactively run simpleReduceC on all the subgoals that forward chainer
      generates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 13:52:05 -0800 (Thu, 30 Mar 2006)
Revision: 8972
Log message:

      Use options instead of exceptions in get_with_arg/get_with_args/get_univ_arg
      (as we are catching these exceptions right away almost everywhere).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 14:10:09 -0800 (Thu, 30 Mar 2006)
Revision: 8973
Log message:

      Adding extra elimination rules for "all i: Index{l}. P[i]" for the cases when
      l is an explicit nil or cons.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 14:54:42 -0800 (Thu, 30 Mar 2006)
Revision: 8974
Log message:

      Trivial no-op.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 15:30:40 -0800 (Thu, 30 Mar 2006)
Revision: 8975
Log message:

      Minor optimization.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-03-30 20:02:38 -0800 (Thu, 30 Mar 2006)
Revision: 8976
Log message:

      Proved two missing elimination rules for sequents with non-zero depth

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 21:33:37 -0800 (Thu, 30 Mar 2006)
Revision: 8977
Log message:

      Fixed a few of the corner cases in the forward chainer.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-31 05:36:39 -0800 (Fri, 31 Mar 2006)
Revision: 8978
Log message:

      Small follow-up to my previous commit

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-31 12:07:25 -0800 (Fri, 31 Mar 2006)
Revision: 8979
Log message:

      Implemented one of the elimination tactics.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-31 17:02:29 -0800 (Fri, 31 Mar 2006)
Revision: 8980
Log message:

      Added some forward rules. Now the test rule in "pmn_core_terms_test" is almost proved except for the "base_theory" subgoal.
      
      However, I do not know how to prove sequent_bterm_forward0, which basically states that "sequent_bterm{s} in BTerm" implies "s in Sequent".
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-03-31 17:04:16 -0800 (Fri, 31 Mar 2006)
Revision: 8981
Log message:

      Changed definiton of Sequent{'d}. Now the argument of the sequent from Sequent{d} must have the depth d.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-31 17:27:28 -0800 (Fri, 31 Mar 2006)
Revision: 8982
Log message:

      The forward-chaining rules for equality should not have high priority
      (especially when the membership version is more efficient - we should give the
      membership rules a chance to act before the equality rules kick in).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-03-31 17:33:04 -0800 (Fri, 31 Mar 2006)
Revision: 8983
Log message:

      Rearranged some rules.