Re: [isabelle] HOLCF equality
On 07/09/2012 10:04 PM, Brian Huffman wrote:
Btw, the above strictness rules came from observing how ghci handled
equalities involving "undefined". For the case of (==) this is
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 ;).
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:
"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
-- 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.
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and