Parent Directory | Revision Log
Links to HEAD: | (view) (download) (annotate) |
Sticky Revision: |
Removed the introduction rule for "equiv" since it made proofs awkard and could be easily substitued with a rewrite rule; Reproved related rules.
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.
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.
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}}.)
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.
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.
ViewVC Help | |
Powered by ViewVC 1.1.26 |