gpt4 book ai didi

equality - `subst`的分布率

转载 作者:行者123 更新时间:2023-12-02 04:14:13 27 4
gpt4 key购买 nike

假设我与两个内图fg有传递关系~。假设 fg 处处一致且 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
  • 使用异构平等有哪些缺点,大多数人似乎并不喜欢它。 (也很重要)

感谢任何帮助。

最佳答案

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 ≡ mprovable )。

最初,当 xy 具有不可统一的类型时,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,您首先需要统一 nm

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

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

“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 时,您就可以对 pj 将与 i 统一,因此不需要额外携带 n ≡ m 的证明。

异质平等,正如 Agda 中所呈现的那样,也是 inconsistent with the univalence axiom .

编辑

x : A, y : B, x ≅ y 上的模式匹配等于 A ≡ B 上的模式匹配,然后更改每个 yx 的上下文中。所以当你写

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 iA j 统一,而是显式地携带 [_]_≅_< 类型的索引,这使得它们可以统一。当索引统一时,两种类型都变成相同的 A i 并且可以像命题相等一样进行。

编辑

异构平等的另一个问题是它不是完全异构的:在 x : A, y : B, x ≅ y AB 中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))

关于equality - `subst`的分布率,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34845986/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com