问题[agda](coding)

我对 Agda 还不熟悉，正在尝试构建 Interval 的格子。到目前为止，我已经将 Lattice 数据类型定义如下：

data 𝕀 : Set where
  ⊤ : 𝕀
  ⊥ : 𝕀
  -∞ : ℤ → 𝕀
  _+∞ : ℤ → 𝕀
  I : (l : ℤ) → (u : ℤ) → {l ≤ u} → 𝕀

并且_⊔𝕀_运算符为：

_⊔𝕀_ : Op₂ 𝕀
⊤ ⊔𝕀 y = ⊤
⊥ ⊔𝕀 y = y
-∞ x ⊔𝕀 ⊤ = ⊤
-∞ x ⊔𝕀 ⊥ = -∞ x
-∞ x ⊔𝕀 -∞ y = -∞ (x ⊔ y)
-∞ x ⊔𝕀 (y +∞) = ⊤
-∞ x ⊔𝕀 I l u = -∞ (x ⊔ u)
(x +∞) ⊔𝕀 ⊤ = ⊤
(x +∞) ⊔𝕀 ⊥ = x +∞
(x +∞) ⊔𝕀 -∞ y = ⊤
(x +∞) ⊔𝕀 (y +∞) = (x ⊓ y) +∞
(x +∞) ⊔𝕀 I l u = (x ⊓ l) +∞
I l u ⊔𝕀 ⊤ = ⊤
I l u {l≤u} ⊔𝕀 ⊥ = I l u {l≤u}
I l u ⊔𝕀 -∞ x = -∞ (u ⊔ x)
I l u ⊔𝕀 (x +∞) = (l ⊓ x) +∞
I l₁ u₁ {l₁≤u₁} ⊔𝕀 I l₂ u₂ {l₂≤u₂} = I (l₁ ⊓ l₂) (u₁ ⊔ u₂) {≤-trans (≤-trans (i⊓j≤i l₁ l₂) l₁≤u₁) ((i≤i⊔j u₁ u₂))}

但在试图证明以下情况下运算符的交换性时

⊔𝕀-comm (I l₁ u₁ {l₁≤u₁}) (I l₂ u₂ {l₂≤u₂}) = {!cong₂ I (⊓-comm l₁ l₂) (⊔-comm u₁ u₂)!}

我得到了错误

Cannot instantiate the metavariable _C_171 to solution
({_ : l ≤ u} → 𝕀) since it contains the variable l
which is not in scope of the metavariable
when checking that the expression I has type ℤ → ℤ → _C_171

如果我理解正确的话，这与I构造函数具有隐式参数有关，但我不知道如何解决这个问题。

我正在尝试构建具有如下定义的数据类型的区间格：

data 𝕀 : Set where
  ⊤   : 𝕀
  ⊥   : 𝕀
  -∞  : ℤ → 𝕀
  _+∞ : ℤ → 𝕀
  I   : (l : ℤ) → (u : ℤ) → {l ≤ u} → 𝕀

为了在某​​些情况下在区间上定义 ⊓𝕀 (glb) 运算符，我必须进行模式匹配i ≤ᵇ j以定义运算符的适当值，尽管我不确定如何在案例定义中重用模式匹配提供的信息。

特别是在

-∞ x ⊓𝕀 (y +∞) with (y ≤ᵇ x) | inspect (y ≤ᵇ_) x
... | false | [ y≤x≡ff ] = ⊥
... | true | [ y≤x≡tt ] = I y x {≤ᵇ⇒≤ {!!}}

我有一个证人，(y ≤ᵇ x) ≡ true但我不知道如何使用它来结合它，≤ᵇ⇒≤以产生证人y ≤ x

我只是个普通人，并不真正了解 Cubical Agda 的所有细节。我曾尝试阅读其文档和 HoTT，但很快就不再关注发生了什么。

我特别希望的是一个如何为更高归纳类型编写简单操作的示例，理想情况下不需要外部库Cubical.Core.Everything。

举一个具体的例子，我们将整数视为自然数对的商：

data N : Set where
  0N : N
  suc : N -> N

_+N_ : N -> N -> N
0N +N n = n
suc m +N n = suc (m +N n)

data Z : Set where
  zpair : N -> N -> N
  zeq : (a b c d : N) -> (a +N d) === (b +N c) -> zpair a b === zpair c d

_+Z_ : Z -> Z -> Z
zpair a b + zpair c d = zpair (a +N c) (b +N d)
zeq a b c d ad=bc i + zeq e f g h eh=fg j = ???

zpair + zeq我可以并且已经通过例如和反之亦然的方式工作，其中有一个i : I和我可以构建一条适当的路径并将其应用于i。我不明白当我有i j : I和我将路径上的点组合在一起时该怎么做，特别是看起来我不能将它们楔在一起，也没有看到明显的组合或将I其应用于的值。

令人满意的答案将填写???，假设上有任何必要的方便引理_+N_，并根据需要使用方程推理 API。

我查看了 Agda 中将整数定义为商的定义，但我找不到这种运算的定义位置。

我想证明

¬Any≃All¬ : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs

我已经定义

to [] t = []
to (x :: xs) v = (v ∘ here) ∷ to xs (v ∘ there)

from [] [] ()
from (x :: xs´) (¬Px ∷ ¬Pxs´) = λ { (here Px) → ¬Px Px ; (there Pxs´) → (from xs´ ¬Pxs´) Pxs´}

问题来自于试图定义

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v 

我的想法是写类似这样的内容：

FromTo [] t = extensionality (λ {()})
FromTo (x :: xs´) v =
  begin
    ((from (x :: xs´)) ∘ (to (x :: xs´))) v 
  ≡⟨⟩
    (from (x :: xs´))(to (x :: xs´) v)
  ≡⟨⟩
    (from (x :: xs´))((v ∘ here) ∷ (to xs´ (v ∘ there)))
  ≡⟨⟩
    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩ -- PARSE ERROR
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨ FromTo xs´ (λ u → v (there u)) ⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (v ∘ there) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → v (there Pxs´) }
  ≡⟨⟩
    v
  ∎

我遇到的问题是我有一个奇怪的解析错误：

 Parse error
≡⟨⟩<ERROR>
        λ { (here Px´) → v (h...

位于此处：

    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }

我尝试了各种方法，想看看是不是缺少了空格，制表符是否错误，还是其他什么原因，但都无济于事。当两个 lambda 被 ≡⟨⟩ 分隔时，就会出现问题。

我正在用 PLFA 在 Agda 中做一个代码练习，以实现“一个列表的反转附加到另一个列表上，就是第二个列表的反转附加到第一个列表的反转上”的证明。

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

我能够毫无问题地完成前两种归纳情况：

reverse-++-distrib {A} [] ys

reverse-++-distrib xs []

但是第三步出现“终止检查失败”错误，我猜这意味着归纳步骤没有正确完成。

reverse-++-distrib {A} (x :: xs) ys =
  begin
    reverse ((x :: xs) ++ ys)
  ≡⟨⟩
    reverse (x :: (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨ cong ((reverse ys) ++_) (cong ((reverse xs) ++_) (sym (reverse-++-fixed-point {A} x))) ⟩
    (reverse ys) ++ (reverse xs ++ (reverse [ x ]))
  **≡⟨ cong ((reverse ys) ++_) (sym (reverse-++-distrib {A} (x :: []) xs)) ⟩**
    (reverse ys) ++ (reverse ([ x ] ++ xs))
  ≡⟨⟩
    (reverse ys) ++ (reverse (x :: ([] ++ xs)))
  ≡⟨ cong ((reverse ys) ++_) (cong reverse (cong (x ::_) (++-identityˡ xs))) ⟩
    (reverse ys) ++ (reverse (x :: xs))
  ∎

有问题的调用显然是这样的：

反向-++-分布 {A} (x :: []) xs

对我来说这看起来不错，因为第一个参数的长度是 1，小于或等于 x :: xs 的长度。并且只有当 xs 是空列表时才相等，在这种情况下它应该进入第二个模式匹配。那么为什么 agda 对此定义有问题呢？