<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Sep 8, 2015 at 1:06 PM, Tim Peters <span dir="ltr"><<a href="mailto:tim.peters@gmail.com" target="_blank">tim.peters@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div id=":2bh" class="" style="overflow:hidden">But I can never decide whether something really "fixes the hash<br>
problem" without a lot more thought.<br></div></blockquote><div><br></div><div>Let me try to outline a formal proof.</div><div><br></div><div>Definitions:  An aware datetime value t is called "regular" if t.utcoffset() does not depend on the value of the fold attribute.  All other values are called "special".  A binary relation "==" is defined by the following rules: (a) two special values s1 and s2 satisfy the "==" relation if they are the same (all component are equal) or they differ only by the value of fold; (b) for any special value s and regular value r, both r == s and s == r are False; and (c) for two regular values r1 and r2, r1 == r2 is equivalent to r1 - r1.utcoffset() and r2 - r2.utcoffset() having the same components.  (Recall that according to PEP 495, dt - delta always has fold=0.)  It will also be useful to define a "naive" equivalence: t1 ~ t2 if t1.tzinfo is t2.tzinfo and all their components except fold (year through microseconds) are equal.  We will assume that ~ being an equivalence relation is well known.</div><div><br></div><div>Lemma: The "==" relation defined above is an equivalence relation.</div><div><br></div><div>Proof:  We need to prove reflexivity (t == t for any t), symmetry (t1 == t2 => t2 == t1) and transitivity (t1 == t2 and t2 == t3 implies t1 == t3).  Note that because of rule (b) it is enough to prove that == is equivalence separately for regular and special values.  The complete proof is a rather tedious analysis of six propositions: three properties for each regular/special case.  I'll present the two least trivial ones.</div><div><br></div><div>1. Let's show that == is transitive on the regular datetimes.  Indeed, let r1, r2 and r3 are regular datetimes and o1, o2, and o3 are their utcoffset() values.  Then r1 == r2 and r2 == r3 implies that r1 - o1 ~ r2 - o2 and r2 - o2 ~ r3 - o3, which in turn implies that r1 - o1 ~ r3 - o3 by transitivity of ~, which in turn implies r1 == r3 by transitivity of ~.  QED.</div><div><br></div><div>2. Let's show that == is transitive on the special datetimes.  This case is even simpler because s1 == s2 implies s1 ~ s2 (s1 and s2 differ only by fold), s2 == s3 implies s2 ~ s3 and thus s1 ~ s3 by transitivity of ~ and s1 == s3 by rule (a).</div><div><br></div><div>Lemma: A function that is constant on equivalence classes satisfies the hash invariant.</div><div><br></div><div>Proof:  This is a tautology.  </div><div><br></div><div>Proposition: newhash(t) = oldhash(t.replace(fold=0)) satisfies the hash invariant.</div><div><br></div><div>Proof: If t is special, its equivalence class consists of itself and a value with the complement value of fold.  Since we force fold=0 before computing the hash values, it is trivially the same for both values in the same class.  If t is regular, since oldhash is defined as a hash of t - t.utcoffset() components, the hash values of r1 and r2 are equal if  r1 - r1.utcoffset() ~ r2 - r2.utcoffset() which follows from r1 == r2 by rule (c).</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div id=":2bh" class="" style="overflow:hidden">
<br>
So far, so good :-)</div></blockquote></div><br>Except for headache. :-)</div></div>