# Re: [isabelle] HOLCF equality

```On 07/09/2012 10:04 PM, Brian Huffman wrote:
```
```On Mon, Jul 9, 2012 at 11:14 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
```
```I am currently using

class eq =
fixes eq :: "'a::pcpo → 'a → tr"
assumes equals_strict [simp]:
"eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
and eq_iff [iff]:
"eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
"eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
"eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).
```
Btw, the above strictness rules came from observing how ghci handled equalities involving "undefined". For the case of (==) this is relatively simple.
```
```
On a related note, in the the ghc sources there are often several versions of a function (usually one due to the Haskell report and an optimized one). Furthermore there are rewrite rules that can be used by the compiler. In both cases the strictness-behaviour (I don't know the correct technical term) is sometimes different, i.e., optimized functions behave different (I think I experienced this with the two versions of "any", but am not a 100% sure) from report versions and sometimes rewrite rules have not been correct when considering strictness, e.g., consider the following excerpt from the sources:
```
{-# RULES
```
"filter" [~1] forall p xs. filter p xs = build (\c n -> foldr (filterFB c p) n xs)
```"filterList"   forall p.     foldr (filterFB (:) p) [] = filter p
```
"filterFB" forall c p q. filterFB (filterFB c p) q = filterFB c (\x -> q x && p x)
``` #-}

```
-- Note the filterFB rule, which has p and q the "wrong way round" in the RHS.
```--     filterFB (filterFB c p) q a b
--   = if q a then filterFB c p a b else b
--   = if q a then (if p a then c a b else b) else b
--   = if q a && p a then c a b else b
--   = filterFB c (\x -> q x && p x) a b
-- I originally wrote (\x -> p x && q x), which is wrong, and actually
-- gave rise to a live bug report.  SLPJ.

```
For verification this is of course important. It seems that HOLCF provides a nice way to verify such compiler rewrite rules in a reliable way.
```
chris

```
```
I think your eq_iff rules need to be weakened like this:

"eq⋅x⋅y = TT ==> x = y"
"eq⋅x⋅y = FF ==> x ≠ y"

Otherwise instances for lazy lists or other lazy datatypes are not
possible. (Your class "eq" is provably a subclass of "flat".)

Alternatively, a subclass "eq_flat" with the strong eq_iff rules might
be useful alongside a weakened "eq" class.

```
```Maybe something like a theory for standard Haskell functions could be placed
where everybody can browse and contribute? (I am currently mainly defining
very basic list functions and proving basic properties about them.)
```
```
This sounds like a good idea. The question is where to put it. We
could add a theory file under HOLCF in the distribution, or we could
add an AFP entry for this purpose. (Maybe using the distribution is
better; as an "archive", the AFP seems not to be intended so much for
dynamic, growing works with open authorship.)

- Brian

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.