如何告诉Agda，财产始终存在于“ if”的分支？

Question

说我想拥有一个digit类型，该类型是char仅数字的细化：

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

然后，我可以构造digit for <代码>'0'喜欢这样（尽管我似乎需要通过的明显参数令人沮丧）：

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

但是，如果我想要一个任意char> char并返回也许Digit ，我似乎无法与然后在分支中交流Agda，iSdigit c始终保持。如何使Agda可见？

在某些语言中，这将是一种流量打字的形式，但是如果我正确理解，AGDA在构造函数上进行模式匹配时只有“流键入”。如果我在'0'，'1'，...'9'上完全匹配，它 do 编译，但这很乏味，似乎很不幸。

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)

（也欢迎改善我的建模方式数字>的建议。）

Answer 1

您可以使用记住匹配项（您需要将false添加到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

您还可以使用if_then_else _ aka 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)