equality - `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 都让我感到困惑。

我想知道

• 是否有更简单的方法来获取subst-dist？也许图书馆里有类似的东西？
• rewrite 的这种特殊用法是怎么回事
• 不使用重写的 subst-dist 的替代证明(最重要)
• 有没有另一种方法可以在不使用subst的情况下获得g a ~ g c？
• 使用异构平等有哪些缺点，大多数人似乎并不喜欢它。 (也很重要)

感谢任何帮助。

Answer 1

rewrite 只是一个加糖的 with，它只是加糖的“顶级”模式匹配。参见Agda’s documentation .

what are some of the downsides of using heterogeneous equality, it doesn't seem like most people are fond of it. (also important)

这样就可以了

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 (您可以通过启用 --injective-type-constructors，但 makes Agda anti-classical )(Fin n ≡ Fin m -> n ≡ m 是 provable )。

最初，当 x 和 y 具有不可统一的类型时，Agda 允许在 x ≅ y 上进行模式匹配，但这允许编写奇怪的代码类似的事情(引用自 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 or maybe it's just ignoring the types and comparing the constructor names?

pigworker Saizan: that's exactly what I think is happening

Andread Abel:

• If I slighly modify the code, I can prove Bool unequal Bool2, where true2, false2 : Bool2 (see file ..22.agda)
• However, if I rename the constructors to true, false : Bool2, then suddenly I cannot prove that Bool is unequal to Bool2 anymore (see other file). So, at the moment Agda2 compares apples and oranges in certain situations. ;-)

因此，为了对 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 = ...

这是异质相等的主要缺点:您需要提供到处索引相等的证明。通常的 cong 和 subst 是非索引的，因此您还必须提供它们的索引版本(或者使用更烦人的 cong2 和 subst2)。

“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 的证明。

异质平等，正如 Agda 中所呈现的那样，也是 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明显单射时才有效。 IE。如果 f 是一系列构造函数(例如 suc (suc n) ≡ suc (suc m))或对其进行计算(例如 2 + n ≡ 2 +米)。类型构造函数(Fin 是)不是单射的，因为这会使 Agda 反经典，因此除非启用 - -单射类型构造函数。

指数统一

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 并且可以像命题相等一样进行。

编辑

异构平等的另一个问题是它不是完全异构的:在 x : A, y : B, x ≅ y A 和 B 中code> 必须位于同一个宇宙中。 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 β

如果我们假设它，那么我们就可以证明级别相等:

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))