Parent Directory | Revision Log
Sticky Revision: |
- Added an option to be have "THEORIES=all" in mk/config (instead of THEORIES="long list of theories"). I will change all my nightly scripts to use THEORIES=all. - Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex that would automatically contain \inputs corresponding to TEXTHEORIES. (Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES was changed). - Minor fixes in some display forms. - Removed theories/caml that never had anything useful. - Removed a few files from theories/ocaml_doc that seemed to be there by accident (Jason, can you confirm?).
- Now substitution (s1=s2 in S) for conclution (t in T[s1]) produces a wf subgoal s:S |- T[s] Type (instead of s:S |- (t in T[s]) Type which was annoying) - Now assertEqT is more powerful than it was.
- added rules applyEquality to intro resource - many rules (e.g. letT and elimination rules for the intersection and union types) produces equality hypotheses in the subgoals that rarely used in practice. Now such rules thin these hypotheses by default. To avoid this one can use doNotThinT = thinningT false.
- All rules in record theories are prooved (except some simple arith facts). - Now progressT checks whether the assumptions are changed (not only the goal). - Add a new operator tsquash{A}={Top|A}
- More record theorems are proved - I restored eta-reduction rule, which is valid (with correct mechanism for conditional rewrites)
1. I added new primitive rules: Itt_struct.exchange Itt_pointwise.hypSubstPointwise Itt_pointwise.contextSubstPointwise The last two rules show the differences between pointwise and pairwise functionality. They are valid in pointwise functionality (as well as quoationtElimination2). 2. Itt_struct3 contains some rules that derived from these new ones. But thesd rules are valid in both functionalities. 3. I moved definition of natural numbers to a new theory Itt_nat. To prove induction for natural numbers one needs Itt_struct3. I almost proved it (leaving some simple arithmetic subgoals, that should be killed by arith) 4. I defined record type. Itt_record is a main theory of records. Itt_record_exm contains some examples. 5. I add a new conversion * applyAllC : conv list -> conv that applies all conversions to all subterms and a tactic * rwa : conv list -> int -> tactic = rw (applyAllC convs)
Display form fixes. - TeX: all object-level terms (theorem statements, etc) are now typeset in math mode. - Tex: variable names are now parsed to detect indeces. In particular, 'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}. - Tex: `|' symbol in display forms is now always handled correctly. - Numerous small fixes.
I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals with both the meta-level squash operator (Base_trivial!squash{}) and the type theory squash operator (Itt_squash!squash{'A}). This makes sense because these two operators are almost exectly the same in nature except for oe being a meta-level operator and another - an object-level one. This commit also renames Itt_hide!hide into Itt_squash!squash. This means that we now have two operators named "squash", however this should not cause any confusion since all part of the system (including the parser and display form mechanism) take into account the number of arguments. Warning: This commit probably broke lots of proofs. I plan to fix that after I have a chance to rewrite the squash theory a little better (for now I just copied the one from Itt_hide). Hopefully, I should have it done within a week.
I moved the bind operator from ITT to the Perv module. This makes sense because what we really mean by "bind" is a generic binding construction, not something ITT-specific. I've also replaced Perv!lambda with Perv!bind since it was now redundant and it was indeed used as "bind", not as "lambda" (there were no beta-reduction for Perv!lambda).
The itt_squiggle theory is added at last. Now a ~ b is a type as well as any other type. To substitute 'a for 'b in nth clause you can use sqSubstT <<a ~ b>> n or you can use Itt_subst2.substT tactic instead. (Note that Itt_subst.substT works only with an equality). The sqSubst tactic works exactly as the substT tactic. By default it replaces all occurrences of a with b, or one can give a bind term as an optional with-argument to specify the occurrences of a to be replaced. Example 1: H |- a+a=2*a by substT <<'a ~ 'b>> 0 1. ....rewrite.... H |- a <--> b 2. ....main.... H |- b+b=2*b Example 2: H |- a+a=2*a by withT <<bind{x.'x+'x=2*'a}>> (substT <<'a ~ 'b>> 0) 1. ....rewrite.... H |- a <--> b 2. ....main.... H |- b+b=2*a I'll document this theory later. Still to do: Figure out how to make conversion "a -> b" from "a~b". P.S. You probably need to run make clean in theories/itt before recompiling.
Now the letT tactic takes a term x=s in S as an argument (instead of s in S).
Spelling changes. For best results, upgrade to http://www.cs.cornell.edu/nogin/RPM/MetaPRL/noarch/words-2.1-1.noarch.html
1. I removed an invalid rule from itt_isect, derived some rule that was primitive, and added some new derivable rules on intersection (see theories.pdf). 2. Fix a bug in Itt_struct2. 3. Now Itt_isect and Itt_theory include Itt_struct2
I have added a new theory Itt_struct2 with some derived advanced versions of substitution rules and the cut rule. In particular, I have proved the let (cutEq) rule (that is the cut rule for the membership). Itt_struct2 redefines the substT tactic to use stronger substitution rules. There are also new tactics: letT, assetEqT and assertHideT. Itt_theory does not include Itt_struct2. If you whant to use these rules, you need to include Itt_struct2 explicitly.
This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.
ViewVC Help | |
Powered by ViewVC 1.1.26 |