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.