Блог

Я пытаюсь доказать разрешимое равенство типа данных в Agda, используя Agda stdlib. У меня есть следующий код, но я не уверен, чем заполнить дыру. Цель кажется разумной, но на самом деле ее достижение является сложной задачей.

Возможно ли это в Agda и есть ли какие-либо идеи о том, как это решить?

 open import Data.String as String hiding (_≟_)  open import Relation.Nullary open import Relation.Binary open import Relation.Binary.PropositionalEquality  module Problem1 where  data Test : Set where  test : String → Test   infix 4 _≟_  _≟_ : Decidable {A = Test} _≡_ test x ≟ test x₁ with x String.≟ x₁ ... | yes refl = yes refl ... | no ¬a = no {!!}  

Дыра:

 Goal: ¬ test x ≡ test x₁ ———————————————————————————————————————————————————————————— ¬a : ¬ x ≡ x₁ x₁ : ℕ x : ℕ  

На самом деле это один лайнер, основанный на разбиении случая на доказательство равенства внутри анонимной функции, как показано ниже:

 ... | no ¬a = no λ {refl → ¬a refl}