`iLawfulOrdDouble` is refuted by NaN and gives a proof of `⊥`

Open
  • Is something wrong?
#488 1 comment 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
45/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Domain
backend

Research direction

Read lib/base/Haskell/Law/Ord/Def.agda around iLawfulOrdDouble and compare it with the change in issue #290 that removed iLawfulEqDouble. Reproduce the provided DoubleFalse.agda example with Agda 2.8.0.2 and the stated command. Done means importing Haskell.Law no longer lets the supplied proofs derive ⊥, while any replacement instance has valid equality and ordering laws.

Written by the indexing model from the issue text.

Description

bug library

The postulated instance iLawfulOrdDouble : IsLawfulOrd Double asserts reflexivity of <= and, through its IsLawfulEq superclass, lawful == for every Double. Agda reduces both nan <= nan and nan == nan to False, so importing Haskell.Law is enough to prove ⊥:

module DoubleFalse where

open import Haskell.Prelude
open import Haskell.Law          -- the umbrella module users import

nan : Double
nan = primFloatDiv 0.0 0.0

nan≠nan : (nan == nan) ≡ False
nan≠nan = refl

nan≰nan : (nan <= nan) ≡ False
nan≰nan = refl

bot₁ : ⊥
bot₁ with () ← trans (sym (reflexivity nan)) nan≰nan

bot₂ : ⊥
bot₂ = IsLawfulEq.nequality (IsLawfulOrd.super iLawfulOrdDouble) nan nan refl refl

Save as DoubleFalse.agda, then run with Agda 2.8.0.2:

git clone https://github.com/agda/agda2hs.git agda2hs
git -C agda2hs checkout 1accbe6aedc2660781c83d9ab7eaf87a75e8c76c
agda --no-libraries --erasure --no-projection-like -i . -i agda2hs/lib/base DoubleFalse.agda

Agda exits successfully without the witness adding postulates. GHC 9.10.3 also gives False for both comparisons on NaN. Tested on Linux x86-64.

#290 removed the iLawfulEqDouble postulate because floating-point equality is not lawful, but iLawfulOrdDouble still provides the order laws and, through super, a lawful Eq. Removing this instance too would block these proofs. A replacement instance for a restricted representation should have its equality and ordering laws proved.

Dominant language
Agda
Stars
211
Forks
51
Avg merge
1d 11h
Merged PRs (30d)
9

Getting set up

This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from agda/agda2hs

All issues in agda/agda2hs

Similar issues

More Backend & API Design issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.