ViewVC logotype

Log of /metaprl/theories/itt/itt_struct2.ml

Parent Directory Parent Directory | Revision Log Revision Log

Sticky Revision:
(Current path doesn't exist after revision 7950)

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 11989 byte(s)
Diff to previous 3312
- 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?).

Revision 3312 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 3 23:55:20 2001 UTC (19 years, 11 months ago) by kopylov
File length: 12002 byte(s)
Diff to previous 3307
- 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.

Revision 3307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 2 22:34:20 2001 UTC (19 years, 11 months ago) by kopylov
File length: 10558 byte(s)
Diff to previous 3298
- 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.

Revision 3298 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 25 01:34:52 2001 UTC (20 years ago) by kopylov
File length: 10418 byte(s)
Diff to previous 3262
- 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}

Revision 3262 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 14 20:46:42 2001 UTC (20 years ago) by kopylov
File length: 10416 byte(s)
Diff to previous 3257
- More record theorems are proved

- I restored eta-reduction rule, which is valid (with correct mechanism
  for conditional rewrites)

Revision 3257 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 13 19:32:30 2001 UTC (20 years ago) by kopylov
File length: 10360 byte(s)
Diff to previous 3235
1. I added new primitive rules:

   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)

Revision 3235 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 20 23:04:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 10092 byte(s)
Diff to previous 3232
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.

Revision 3232 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 17 22:06:20 2001 UTC (20 years, 1 month ago) by nogin
File length: 10088 byte(s)
Diff to previous 3139
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.

Revision 3139 - (view) (download) (annotate) - [select for diffs]
Modified Sun Feb 4 19:38:29 2001 UTC (20 years, 4 months ago) by nogin
File length: 10046 byte(s)
Diff to previous 3137
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
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).

Revision 3137 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 2 23:16:21 2001 UTC (20 years, 4 months ago) by kopylov
File length: 10038 byte(s)
Diff to previous 3131
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.

Revision 3131 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 1 19:22:00 2001 UTC (20 years, 4 months ago) by kopylov
File length: 9909 byte(s)
Diff to previous 3124
Now the letT tactic takes a term x=s in S as an argument (instead of s in S).

Revision 3124 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 31 22:44:31 2001 UTC (20 years, 4 months ago) by nogin
File length: 9900 byte(s)
Diff to previous 3121
Spelling changes.
For best results, upgrade to http://www.cs.cornell.edu/nogin/RPM/MetaPRL/noarch/words-2.1-1.noarch.html

Revision 3121 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 30 01:05:43 2001 UTC (20 years, 4 months ago) by kopylov
File length: 9900 byte(s)
Diff to previous 3115
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

Revision 3115 - (view) (download) (annotate) - [select for diffs]
Added Fri Jan 26 21:15:20 2001 UTC (20 years, 4 months ago) by kopylov
File length: 9814 byte(s)
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.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26