"subst"的分布

Question

假设我有一个传递关系~有两个endomaps f和g.假设f并且g在任何地方f a ~ f b ~ f c 都同意然后有两种方式可以显示g a ~ g c:通过给定的等式将每个f转换为a 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不使用重写的替代证明(最重要)
• 是否有另一种g a ~ g c不使用的方式获得subst？
• 使用异构平等有什么缺点,似乎大多数人都不喜欢它.(也很重要)

任何帮助表示赞赏.

Answer 1

rewrite只是一个含糖的with,这只是加糖的"顶级"模式匹配.请参阅Agda的文档.

使用异构平等有什么缺点,似乎大多数人都不喜欢它.(也很重要)

还行吧

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,但这使得Agda反经典)(虽然Fin n ? Fin m -> n ? m可以证明).

最初Agda允许在x ? y何时进行模式匹配x并y具有非统一类型,但这允许编写奇怪的东西,如(引用此线程)

  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 Abel:

• 如果我轻轻地修改代码,我可以证明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 = ...

这是异质平等的主要缺点:你需要提供各地索引相等的证据.平时cong和subst在非索引,所以还必须为他们提供的索引版本(或使用更讨厌cong?和subst?).

"heterindexed"(我不知道它是否有一个正确的名称)平等没有这样的问题

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中呈现的异构平等也与单一性公理不一致.

编辑

模式匹配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,并且可以像命题平等一样进行.

编辑

异构平等的另一个问题是它不是完全异构的:in x : A, y : B, x ? y A并且B必须在同一个Universe中.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 ?)

因为阿格达不认为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))