/[mojave]/metaprl/theories/czf/czf_itt_equiv.prla
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_equiv.prla

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3552 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 07:28:45 2002 UTC (19 years, 2 months ago) by xiny
File length: 258337 byte(s)
Diff to previous 3549
Removed the introduction rule for "equiv" since it made proofs awkard
and could be easily substitued with a rewrite rule;
Reproved related rules.


Revision 3549 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 24 11:01:50 2002 UTC (19 years, 3 months ago) by xiny
File length: 237878 byte(s)
Diff to previous 3543
1. The original equivTransT was wrong. Changed the original equivTrans1T
   and equivSym1T into equivTransT and equivSymT; Changed the original
   equivSymT to equivSym1T and removed equivTrans1T.
2. Added the "fold" form for "equiv".
3. Reproved rules in the file.


Revision 3543 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 24 07:22:12 2002 UTC (19 years, 3 months ago) by xiny
File length: 321592 byte(s)
Diff to previous 3534
  Added and proved the rule for the property "if a is equivalent to b
  under any equivalence relation, then a is equal to b". It is proved
  by the use of "set builder" defined in Czf_itt_set_bvd.


Revision 3534 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 09:57:12 2002 UTC (19 years, 3 months ago) by xiny
File length: 287711 byte(s)
Diff to previous 3526
1. Minor changes in the introduction rule for equivalence relations;
2. Added tactics "equivSym1T" and "equivTrans1T" for the symmetry and
   transitivity of equivalence relations which are supposed to be
   applied to goals while "equivSymT" and "equivTransT" in the previous
   versions are supposed to be applied to hypotheses;
3. Added the property that if 'a = 'b then 'a is equivalent to 'b under
   any equivalence relation;
4. Added in comments the property that if 'a is equivalent to 'b under
   any equivalence relation then 'a = 'b. (This is not proved since I
   don't know how to express the set
   {(a, b): mem{'a; 's}, mem{'b; 's}, equal{'a; 'b}}.)


Revision 3526 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 4 02:19:09 2002 UTC (19 years, 3 months ago) by xiny
File length: 267112 byte(s)
Diff to previous 3515
1. Defined functionality in the sense of equivalence relations,
   which is distinct from the functionality for equality.
2. Added and proved properties of equivalence functionality.
3. Added and proved functionality properties of equivalence relations
   (both equivalence functionality and equality functionality).
4. Updated the substitution rules and tactics.

Tactics for equivalence relations:
  equivFunSetT, equivFunMemT, equivRefT, equivSymT,
  equivTransT, equivSubstT

TODO:
  1. Might need to define terms for functionality judgments on
     dependent types (i.e., equiv_dfun_prop).
  2. Implement equivalence class later.


Revision 3515 - (view) (download) (annotate) - [select for diffs]
Added Mon Feb 25 02:21:06 2002 UTC (19 years, 3 months ago) by xiny
File length: 139738 byte(s)
Added definition for equivalence relations, which are more general
than "equal" and are necessary in the context of groups.

TODO:
   1. Might need to define functionality for equivalence relations
      and update the substitution rules.
   2. Implement equivalence class.


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