CODEWITHSUNDEEP
agda
Camelid
Camelid

Reputation: 1575

How to tell Agda that property always holds in branch of `if`?

Say I want to have a Digit type that is a refinement of Char to only digits:

open import Data.Bool using (Bool; true; if_then_else_)
open import Data.Char using (Char; isDigit)
open import Data.Maybe using (Maybe; just; nothing)

data IsTrue : Bool → Set where
  is-true : IsTrue true

data IsDigit (c : Char) : Set where
  is-digit : {p : IsTrue (isDigit c)} → IsDigit c

data Digit : Set where
  digit : (c : Char) → {p : IsDigit c} → Digit

I can then construct, e.g., the Digit for '0' like so (although the obvious parameters that I seem to need to pass are frustrating):

0-digit : Digit
0-digit = digit '0' {is-digit {_} {is-true}}

However, if I want a function that takes an arbitrary Char and returns Maybe Digit, I can't seem to communicate to Agda that in the then branch, isDigit c always holds. How do I make this visible to Agda?

In some languages, this would be a form of flow typing, but if I understand correctly, Agda only has "flow typing" when pattern-matching on constructors. It does compile if I exhaustively match on '0', '1', ... '9', but that's tedious and seems unfortunate.

maybeFromChar : Char → Maybe Digit
maybeFromChar c =
  if isDigit c
    then just (digit c {is-digit {c} {is-true}})
    else nothing

.../Foo.agda:20,39-46
true != isDigit c of type Bool
when checking that the expression is-true has type
IsTrue (isDigit c)

(Suggestions for improvements to the way I'm modeling Digit are welcome as well.)

Upvotes: 0

Views: 54

Answers (1)

effectfully
effectfully

Reputation: 12715

You can use the inspect idiom to remember the match (you'll need to add false to the import list of Data.Bool):

open import Relation.Binary.PropositionalEquality

maybeFromChar : Char → Maybe Digit
maybeFromChar c with isDigit c | inspect isDigit c
... | true  | [ eq ] = just (digit c {is-digit {c} {subst IsTrue (sym eq) is-true}})
... | _     | _      = nothing

You can also use the dependent version of if_then_else_ a.k.a. the eliminator of Bool:

open import Function
open import Data.Maybe as Maybe

elimBool : ∀ {π} → (P : Bool → Set π) → P true → P false → ∀ b → P b
elimBool P t f true  = t
elimBool P t f false = f

maybeFromChar' : Char → Maybe Digit
maybeFromChar' c =
  Maybe.map (λ p -> digit c {is-digit {_} {p}}) $
    elimBool (Maybe ∘ IsTrue) (just is-true) nothing (isDigit c)

Upvotes: 2

Related Questions