Как я могу подтвердить, что тип действителен в Agda?

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

Итак, допустим, у нас есть теорема f-equal

f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y
f-equal refl = refl

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

Π-equal : ∀ {A} {B : A → Set} {f : {a : A} → B a} {x y : A} →
            x ≡ y → f x ≡ f y

делает компилятор недовольным, потому что он не может понять, что f x и f y относятся к одному и тому же типу. Кажется, это проблема решаемая. Это?

Примечание; используемое отношение эквивалентности определяется следующим образом:

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

dependent-type theorem-proving proof agda type-theory
person gallabytes    schedule 09.09.2014    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Вы можете явно изменить тип f x:

Π-equal : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> P.subst B p (f x) ≡ f y
Π-equal refl = refl

Or

Π-equal'T : ∀ {α β} {A : Set α} {B : A -> Set β} -> ((x : A) -> B x) -> (x y : A) -> x ≡ y -> Set β
Π-equal'T f x y p with f x | f y
...| fx | fy rewrite p = fx ≡ fy

Π-equal' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
        -> (p : x ≡ y) -> Π-equal'T f x y p
Π-equal' refl = refl

Или вы можете использовать неоднородное равенство:

Π-equal'' : ∀ {α β} {A : Set α} {B : A -> Set β} {f : (x : A) -> B x} {x y : A}
          -> x ≡ y -> f x ≅ f y
Π-equal'' refl = refl

Также может быть полезна функция subst, вот ее тип (C-c C-d P.subst в Emacs):

{a p : .Agda.Primitive.Level} {A : Set a} (P : A → Set p)
      {x y : A} →
      x ≡ y → P x → P y

Используемый импорт:

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H

Кстати, ваш f-equal - это cong в стандартной библиотеке.

person user3237465    schedule 09.09.2014

arrow_upward
2
arrow_downward

Это может быть обработано гетерогенным равенством, которое может быть импортировано из Relation.Binary.HeterogeneousEquality:

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

Интуитивно понятно, хет. равенство свидетельствует о равенстве задействованных типов, а также о равенстве ценностей.

В модуле можно найти аналоги функций для стандартного равенства (subst, trans, cong и т. Д.). Также вы можете конвертировать туда и обратно стандартные и хет. равенство с использованием ≅-to-≡ и ≡-to-≅, но только тогда, когда типы по сторонам явно равны.

Обратите внимание, что синтаксис «перезаписать» нельзя использовать с het. равенство.

В качестве альтернативы мы можем использовать стандартное равенство с одной из сторон, приведенных к соответствующему типу:

Π-equal : 
  ∀ {A : Set} {B : A → Set}{f : ∀ a → B a}{x y : A} → (p : x ≡ y) → subst B p (f x) ≡ f y
Π-equal refl = refl

Этот подход фактически эквивалентен het. равенство, но я нахожу его. с равенством намного легче работать.

person András Kovács    schedule 09.09.2014