Работа в рамках решимости Agda - PullRequest
Новая
       57

Работа в рамках решимости Agda

1 голос
/ 14 апреля 2020

У меня проблемы с возможностью использования строки. Во-первых, я запутался, почему в Agda так сложно работать с решаемостью, когда в Coq он выглядит гладким, как масло. Когда я пытаюсь доказать эту простую теорему о строках, Агда раскрывает этот беспорядок определения, с которым практически невозможно работать, если вы не знаете точно, что вы пытаетесь сделать. Как я могу работать с возможностью выбора строки с помощью сопоставления с шаблоном, который сохраняет определение в такте?

Использую функцию сохранения Пня вместо проверки Агды. 

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 = {!!}

Вот вывод Агды: 

-- 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 был значительно чище, а затем просто применить Основы c правил для получения окончательного доказательства. 

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)

Последняя строка является законченным доказательством. Любые предложения будут полезны!

1 Ответ

1 голос
/ 20 апреля 2020

Импортируя Relation.Nullary там, где определено понятие разрешимости, вы получите доступ к шаблонам yes и no , и Agda с радостью повторно наберет (.true Relation.Nullary.because Relation.Nullary.ofʸ refl) как yes refl и другие один как no ¬p.

Относительно типа цели, это вытекает из того факта, что равенство для строк получается поточечным равенством в списках символов, а равенство для символов получается равенством их базового представления. как числа. Это многословно, но это дает нам определение, признанное Agda как безопасное и довольно эффективное.

...