Работа над аксиомами Пеано в Агде и наткнулся на камень преткновения

PA6 : ∀{m n} -> m ≡ n -> n ≡ m

это аксиома, которую я пытаюсь решить и поддержать, я пытался использовать конг (из основной библиотеки), но у меня проблемы с конструктором конг

PA6 = cong

ни к чему меня не приводит, я знаю, что для cong я должен предоставить refl для равенства и типа, но я не уверен, какой тип я должен предоставить. Идеи?

Это для небольшого задания в университете, поэтому я бы предпочел, чтобы кто-нибудь продемонстрировал то, что я пропустил, а не написал реальный ответ, но я был бы признателен за любую степень поддержки.


haskell axiom agda
person Schroedinger    schedule 05.04.2010    source источник

Ответы (2)


arrow_upward
6
arrow_downward

Ваш PA6 говорит, что ≡ симметричен.

Это можно найти в стандартной библиотеке из модуля Relation.Binary.PropositionalEquality.

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

(Этот вопрос довольно старый, но я пишу для будущих читателей, которые наткнутся на него.)

person glguy    schedule 07.11.2010

arrow_upward
3
arrow_downward

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

Таким образом, чтобы удовлетворить мою типовую сигнатуру, принятая agda: PA6 refl = refl

надеюсь, это поможет

person Schroedinger    schedule 05.04.2010
comment
Пожалуйста, опубликуйте немного больше о решении, чтобы оно могло помочь другим, у которых есть аналогичная проблема (по крайней мере, ваше определение ℕ и ≡ или версия lib и имя модуля, если они из библиотеки). Голосование последует :) - person fishlips; 05.04.2010