Распределительность `subst`

Question

Предположим, что у меня есть транзитивное отношение ~ с двумя эндомапами f и g. Предполагая f и g согласны везде и f a ~ f b ~ f c то есть два способа, чтобы показать g a ~ g c: трансформируют каждый f в g по данному равенству затем применить транзитивность, или применять транзитивность то преобразование по равенству. Являются ли полученные доказательства одинаковыми? Видимо поэтому,

open import Relation.Binary.PropositionalEquality 

postulate A : Set 
postulate _~_ : A → A → Set 
postulate _⟨~~⟩_ : ∀{a b c} → a ~ b → b ~ c → a ~ c 
postulate f g : A → A 

subst-dist : ∀{a b c}{ef : f a ~ f b}{psf : f b ~ f c} → (eq : ∀ {z} → f z ≡ g z) 
    → 
     subst₂ _~_ eq eq ef ⟨~~⟩ subst₂ _~_ eq eq psf 
     ≡ subst₂ _~_ eq eq (ef ⟨~~⟩ psf) 

subst-dist {a} {b} {c} {ef} {psf} eq rewrite eq {a} | eq {b} | eq {c} = refl 

Я только недавно узнал о rewrite ключевом слове и думал, что это может помочь; видимо, это так. Однако, честно говоря, я не понимаю, что здесь происходит. Я использовал rewrite другие времена, с пониманием. Однако все эти subst s меня смущают.

Я хотел бы знать,

• , если есть ли способ проще получить subst-dist? Может быть, что-то подобное в библиотеках?
• , что происходит с этим специфическим использованием rewrite
• альтернативного доказательство subst-dist без использования рерайт (самого важного)
• есть другой способ, чтобы получить g a ~ g c без использования subst?
• Каковы некоторые из недостатков использования гетерогенного равенства, похоже, что большинство людей не любят его. (также важно)

Любая помощь приветствуется.

Answer 1

rewrite - это всего лишь сахаристый with, который является просто оформленным совпадением «верхнего уровня». См. В Agda’s documentation.

Каковы некоторые из недостатков использования гетерогенного равенства, это не похоже, что большинство людей его любят. (Важно)

Это нормально

types-equal : ∀ {α} {A B : Set α} {x : A} {y : B} -> x ≅ y -> A ≡ B 
types-equal refl = refl 

это нормально, а также

A-is-Bool : {A : Set} {x : A} -> x ≅ true -> A ≡ Bool 
A-is-Bool refl = refl 

Это ошибка

fail : ∀ {n m} {i : Fin n} {j : Fin m} -> i ≅ j -> n ≡ m 
fail refl = {!!} 

-- n != m of type ℕ 
-- when checking that the pattern refl has type i ≅ j 

потому Fin n ≡ Fin m не сразу следует n ≡ m (вы можете ke это так, включив --injective-type-constructors, но что makes Agda anti-classical) (Fin n ≡ Fin m -> n ≡ m - provable).

Первоначально Agda допускается сопоставление с образцом на x ≅ y когда x и y имеют не-unifiable типов, но это позволяет писать странные вещи, как (цитата из this нити)

P : Set -> Set 
    P S = Σ S (\s → s ≅ true) 

    pbool : P Bool 
    pbool = true , refl 

    ¬pfin : ¬ P (Fin 2) 
    ¬pfin (zero ,()) 
    ¬pfin (suc zero ,()) 
    ¬pfin (suc (suc()) ,()) 

    tada : ¬ (Bool ≡ Fin 2) 
    tada eq = ⊥-elim (¬pfin (subst (\ S → P S) eq pbool)) 

Saizan или, может быть, это просто игнорируя типы и сравнивая имена конструкторов?

pigworker Saizan: это именно то, что я думаю, что происходит

Andread Авеля:

• Если я slighly изменить код, я могу доказать, Bool неравной Bool2, где true2, false2: Bool2 (см файл ..22.agda)
• Однако, если я переименую конструкторы в true, false: Bool2, то вдруг я не могу доказать, что Bool больше не равен Bool2 (см. другой файл). Итак, на данный момент Agda2 сравнивает яблоки и апельсины в определенных ситуациях. ;-)

Так что для того, чтобы соответствовать узор на i ≅ j, где i : Fin n, j : Fin m, в первую очередь необходимо унифицировать n с m

OK : ∀ {n m} {i : Fin n} {j : Fin m} -> n ≡ m -> i ≅ j -> ... 
OK refl refl = ... 

Это главный недостаток heteregeneous равенства: необходимо предоставить доказательств равенства индексов всюду. Обычные cong и subst не индексируются, поэтому вам также необходимо предоставить индексированные версии (или использовать еще более раздражающие cong₂ и subst₂).

Там нет таких проблем с «heteroindexed» (я не знаю, если он имеет имя собственное) равенство

data [_]_≅_ {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : ∀ {j} -> A j -> Set where 
    refl : [ A ] x ≅ x 

например

OK : ∀ {n m} {i : Fin n} {j : Fin m} -> [ Fin ] i ≅ j -> n ≡ m 
OK refl = refl 

В более общем плане, когда у вас есть x : A i, y : A j, p : [ A ] x ≅ y, вы можете матч узор на p и j будут объединены с i, так что вам не нужно носить с собой дополнительное доказательство n ≡ m.

Неоднородное равенство, представленное в Агда, также является inconsistent with the univalence axiom.

РЕДАКТИРОВАТЬ

шаблона согласования на x : A, y : B, x ≅ y равно шаблон на A ≡ B, а затем меняются каждый y в контексте x.Поэтому, когда вы пишете

fail : ∀ {n m} {i : Fin n} {j : Fin m} -> i ≅ j -> n ≡ m 
fail refl = {!!} 

это то же самое, как

fail' : ∀ {n m} {i : Fin n} {j : Fin m} -> Fin n ≡ Fin m -> i ≅ j -> n ≡ m 
fail' refl refl = {!!} 

, но вы не можете шаблон матч на Fin n ≡ Fin m

fail-coerce : ∀ {n m} -> Fin n ≡ Fin m -> Fin n -> Fin m 
fail-coerce refl = {!!} 

-- n != m of type ℕ 
-- when checking that the pattern refl has type Fin n ≡ Fin m 

, как вы не можете шаблон матча на

fail'' : ∀ {n m} -> Nat.pred n ≡ Nat.pred m -> n ≡ m 
fail'' refl = {!!} 

-- n != m of type ℕ 
-- when checking that the pattern refl has type Nat.pred n ≡ Nat.pred m 

Всего

f-inj : ∀ {n m} -> f n ≡ f m -> ... 
f-inj refl = ... 

работает только в том случае, если f явно инъективен. То есть если f представляет собой серию конструкторов (например, suc (suc n) ≡ suc (suc m)) или вычисляет к ней (например, 2 + n ≡ 2 + m). Конструкторы типов (которые Fin) не являются инъективными, потому что это сделало бы Agda антиклассическим, поэтому вы не можете нарисовать на Fin n ≡ Fin m, если вы не включите --injective-type-constructors.

Индексы унифицировать для

data [_]_≅_ {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : ∀ {j} -> A j -> Set where 
    refl : [ A ] x ≅ x 

, потому что вы не пытаетесь объединить A i с A j, но вместо того, чтобы явно нести индексы в типе [_]_≅_, что делает их доступными для объединения. Когда индексы унифицированы, оба типа становятся одинаковыми A i, и можно продолжить, как с пропозициональным равенством.

EDIT

Одна другая проблема с гетерогенной равенства является то, что она не полностью гетерогенная: в x : A, y : B, x ≅ yA и B должны находиться в одной и той же вселенной. Лечение уровней вселенной в data определений изменилось в последнее время, и теперь мы можем определить полностью гетерогенной равенство:

data _≅_ {α} {A : Set α} (x : A) : ∀ {β} {B : Set β} -> B -> Set where 
    refl : x ≅ x 

Но это не работает

levels-equal : ∀ {α β} -> Set α ≅ Set β -> α ≅ β 
levels-equal refl = refl 

-- Refuse to solve heterogeneous constraint Set α : Set (suc α) =?= 
-- Set β : Set (suc β) 

потому что Agda не думает suc инъективна

suc-inj : {α β : Level} -> suc α ≅ suc β -> α ≅ β 
suc-inj refl = refl 

-- α != β of type Level 
-- when checking that the pattern refl has type suc α ≅ suc β 

Если мы допускаем это, то мы можем доказать levels-equal:

hcong : ∀ {α β δ} {A : Set α} {B : Set β} {D : Set δ} {x : A} {y : B} 
     -> (f : ∀ {γ} {C : Set γ} -> C -> D) -> x ≅ y -> f x ≅ f y 
hcong f refl = refl 

levelOf : ∀ {α} {A : Set α} -> A -> Level 
levelOf {α} _ = α 

postulate 
    suc-inj : {α β : Level} -> suc α ≅ suc β -> α ≅ β 

levels-equal : ∀ {α β} -> Set α ≅ Set β -> α ≅ β 
levels-equal p = suc-inj (suc-inj (hcong levelOf p))