在 agda 的可决策性框架内工作
Working within agda's decideability framework
我在使用字符串可判定性时遇到问题。首先,我很困惑为什么在 Agda 中处理可决定性如此困难,而在 Coq 中它看起来像黄油一样光滑。当我试图证明这个关于字符串的简单定理时,Agda 展开了这个定义的混乱,除非你确切地知道你正在尝试做什么,否则几乎不可能使用它。我如何通过模式匹配来处理字符串的可判定性以保持定义的完整性?
我正在使用 Stump 的 keep 函数而不是 Agda 的 inspect。
keep : ∀{ℓ}{A : Set ℓ} → (x : A) → Σ A (λ y → x ≡ y)
keep x = ( x , refl )
--first roadblock
eqbStringrefl' : forall (b : String) → true ≡ (b == b)
eqbStringrefl' b with keep (b ≟ b)
eqbStringrefl' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd = {!!}
eqbStringrefl' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = {!!}
这是 Agda 的输出:
-- Goal: true ≡
-- Relation.Nullary.Decidable.Core.isYes
-- (Relation.Nullary.Decidable.Core.map′
-- (λ x →
-- Agda.Builtin.String.Properties.primStringToListInjective b b
-- (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
-- (Data.List.Relation.Binary.Pointwise.map
-- (λ {z} {z = z₁} →
-- Agda.Builtin.Char.Properties.primCharToNatInjective z z₁)
-- x)))
-- (λ x →
-- Data.List.Relation.Binary.Pointwise.map
-- (cong Agda.Builtin.Char.primCharToNat)
-- (Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
-- (cong Data.String.toList x)))
-- (Data.List.Relation.Binary.Pointwise.decidable
-- (λ x y →
-- Relation.Nullary.Decidable.Core.map′
-- (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Bool.Properties.T?
-- (Agda.Builtin.Char.primCharToNat x Data.Nat.≡ᵇ
-- Agda.Builtin.Char.primCharToNat y)))
-- (Data.String.toList b) (Data.String.toList b)))
-- ————————————————————————————————————————————————————————————
-- snd : Relation.Nullary.Decidable.Core.map′
-- (λ x →
-- Agda.Builtin.String.Properties.primStringToListInjective b b
-- (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
-- (Data.List.Relation.Binary.Pointwise.map
-- (λ {z} {z = z₁} →
-- Agda.Builtin.Char.Properties.primCharToNatInjective z z₁)
-- x)))
-- (λ x →
-- Data.List.Relation.Binary.Pointwise.map
-- (cong Agda.Builtin.Char.primCharToNat)
-- (Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
-- (cong Data.String.toList x)))
-- (Data.List.Relation.Binary.Pointwise.decidable
-- (λ x y →
-- Relation.Nullary.Decidable.Core.map′
-- (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Bool.Properties.T?
-- (Agda.Builtin.Char.primCharToNat x Data.Nat.≡ᵇ
-- Agda.Builtin.Char.primCharToNat y)))
-- (Data.String.toList b) (Data.String.toList b))
-- ≡ Relation.Nullary.yes refl
-- b : String
如果我现在应用重写,目标会得到简化,但假设列表中仍然一团糟。
当我尝试 ctrl-a 时,我收到以下错误,尽管目标似乎可以推断:
Goal: true ≡ true
Not implemented: The Agda synthesizer (Agsy) does not support
copatterns yet
尽管如此,我还是能够继续进行,就好像 snd 项明显更清晰一样,然后只需应用基本规则即可得出最终证明。
eqbStringrefl'' : forall (b : String) → true ≡ (b == b)
eqbStringrefl'' b with keep (b ≟ b)
eqbStringrefl'' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd rewrite snd = {!!}
eqbStringrefl'' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = {!!}
-- eqbStringrefl'' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd rewrite snd = refl
-- eqbStringrefl'' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = ⊥-elim (¬p refl)
最后一行是完成的证明。任何建议都会有所帮助!
通过导入定义了可判定性概念的 Relation.Nullary
,您
将可以访问 yes
and no
patterns 并且 Agda 将很乐意重新加糖
(.true Relation.Nullary.because Relation.Nullary.ofʸ refl)
作为 yes refl
另一个是 no ¬p
.
关于目标的类型,它来自这样一个事实,即字符串的相等性是通过字符列表上的逐点相等性获得的,而字符的相等性是通过它们作为数字的底层表示的相等性获得的。它很冗长,但这给了我们一个被 Agda 认为安全且相当有效的定义。
我在使用字符串可判定性时遇到问题。首先,我很困惑为什么在 Agda 中处理可决定性如此困难,而在 Coq 中它看起来像黄油一样光滑。当我试图证明这个关于字符串的简单定理时,Agda 展开了这个定义的混乱,除非你确切地知道你正在尝试做什么,否则几乎不可能使用它。我如何通过模式匹配来处理字符串的可判定性以保持定义的完整性?
我正在使用 Stump 的 keep 函数而不是 Agda 的 inspect。
keep : ∀{ℓ}{A : Set ℓ} → (x : A) → Σ A (λ y → x ≡ y)
keep x = ( x , refl )
--first roadblock
eqbStringrefl' : forall (b : String) → true ≡ (b == b)
eqbStringrefl' b with keep (b ≟ b)
eqbStringrefl' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd = {!!}
eqbStringrefl' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = {!!}
这是 Agda 的输出:
-- Goal: true ≡
-- Relation.Nullary.Decidable.Core.isYes
-- (Relation.Nullary.Decidable.Core.map′
-- (λ x →
-- Agda.Builtin.String.Properties.primStringToListInjective b b
-- (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
-- (Data.List.Relation.Binary.Pointwise.map
-- (λ {z} {z = z₁} →
-- Agda.Builtin.Char.Properties.primCharToNatInjective z z₁)
-- x)))
-- (λ x →
-- Data.List.Relation.Binary.Pointwise.map
-- (cong Agda.Builtin.Char.primCharToNat)
-- (Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
-- (cong Data.String.toList x)))
-- (Data.List.Relation.Binary.Pointwise.decidable
-- (λ x y →
-- Relation.Nullary.Decidable.Core.map′
-- (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Bool.Properties.T?
-- (Agda.Builtin.Char.primCharToNat x Data.Nat.≡ᵇ
-- Agda.Builtin.Char.primCharToNat y)))
-- (Data.String.toList b) (Data.String.toList b)))
-- ————————————————————————————————————————————————————————————
-- snd : Relation.Nullary.Decidable.Core.map′
-- (λ x →
-- Agda.Builtin.String.Properties.primStringToListInjective b b
-- (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
-- (Data.List.Relation.Binary.Pointwise.map
-- (λ {z} {z = z₁} →
-- Agda.Builtin.Char.Properties.primCharToNatInjective z z₁)
-- x)))
-- (λ x →
-- Data.List.Relation.Binary.Pointwise.map
-- (cong Agda.Builtin.Char.primCharToNat)
-- (Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
-- (cong Data.String.toList x)))
-- (Data.List.Relation.Binary.Pointwise.decidable
-- (λ x y →
-- Relation.Nullary.Decidable.Core.map′
-- (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
-- (Agda.Builtin.Char.primCharToNat y))
-- (Data.Bool.Properties.T?
-- (Agda.Builtin.Char.primCharToNat x Data.Nat.≡ᵇ
-- Agda.Builtin.Char.primCharToNat y)))
-- (Data.String.toList b) (Data.String.toList b))
-- ≡ Relation.Nullary.yes refl
-- b : String
如果我现在应用重写,目标会得到简化,但假设列表中仍然一团糟。 当我尝试 ctrl-a 时,我收到以下错误,尽管目标似乎可以推断:
Goal: true ≡ true
Not implemented: The Agda synthesizer (Agsy) does not support
copatterns yet
尽管如此,我还是能够继续进行,就好像 snd 项明显更清晰一样,然后只需应用基本规则即可得出最终证明。
eqbStringrefl'' : forall (b : String) → true ≡ (b == b)
eqbStringrefl'' b with keep (b ≟ b)
eqbStringrefl'' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd rewrite snd = {!!}
eqbStringrefl'' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = {!!}
-- eqbStringrefl'' b | (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) , snd rewrite snd = refl
-- eqbStringrefl'' b | (.false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p) , snd = ⊥-elim (¬p refl)
最后一行是完成的证明。任何建议都会有所帮助!
通过导入定义了可判定性概念的 Relation.Nullary
,您
将可以访问 yes
and no
patterns 并且 Agda 将很乐意重新加糖
(.true Relation.Nullary.because Relation.Nullary.ofʸ refl)
作为 yes refl
另一个是 no ¬p
.
关于目标的类型,它来自这样一个事实,即字符串的相等性是通过字符列表上的逐点相等性获得的,而字符的相等性是通过它们作为数字的底层表示的相等性获得的。它很冗长,但这给了我们一个被 Agda 认为安全且相当有效的定义。