在上下文中使用等价来强制归约

Question

此问题的设置与此 earlier question 中的“排序列表合并”示例相同。

{-# OPTIONS --sized-types #-}

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P hiding (trans)

module ListMerge
   {???? ℓ}
   (A : Set ????)
   {_<_ : Rel A ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

   open import Data.Product
   open import Data.Unit
   open import Level
   open import Size

   data SortedList (l u : A) : {ι : Size} → Set (???? ⊔ ℓ) where
      [] : {ι : _} → .(l < u) → SortedList l u {↑ ι}
      _∷[_]_ : {ι : _} (x : A) → .(l < x) → (xs : SortedList x u {ι}) →
               SortedList l u {↑ ι}

和以前一样，我使用了调整大小的类型，以便 Agda 可以确定以下 merge 函数终止：

   open IsStrictTotalOrder isStrictTotalOrder

   merge : ∀ {l u} → {ι : _} → SortedList l u {ι} →
                      {ι′ : _} → SortedList l u {ι′} → SortedList l u
   merge xs ([] _) = xs
   merge ([] _) ys = ys
   merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
   ... | tri< _ _ _ = x ∷[ l<x ] (merge xs (y ∷[ _ ] ys))
   merge (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ =
      x ∷[ l<x ] (merge xs ys)
   ... | tri> _ _ _ = y ∷[ l<y ] (merge (x ∷[ _ ] xs) ys)

我要做的是证明以下结合性定理：

   assoc : ∀ {l u} → {ι₁ : _} → (x : SortedList l u {ι₁}) →
                     {ι₂ : _} → (y : SortedList l u {ι₂}) →
                     {ι₃ : _} → (z : SortedList l u {ι₃}) →
           merge (merge x y) z ≡ merge x (merge y z)

根据定义，至少有一个列表是[] 的情况很容易理解，但为了完整起见，我将它们包括在内。

   assoc ([] _) ([] _) ([] _) = P.refl
   assoc ([] _) ([] _) (_ ∷[ _ ] _) = P.refl
   assoc ([] _) (_ ∷[ _ ] _) ([] _) = P.refl
   assoc (_ ∷[ _ ] _) ([] _) ([] _) = P.refl
   assoc ([] _) (y ∷[ _ ] _) (z ∷[ _ ] _) with compare y z
   assoc ([] _) (y ∷[ _ ] ys) (.y ∷[ _ ] zs) | tri≈ _ P.refl _ = P.refl
   ... | tri< _ _ _ = P.refl
   ... | tri> _ _ _ = P.refl
   assoc (x ∷[ _ ] _) ([] _) (z ∷[ _ ] _) with compare x z
   assoc (x ∷[ _ ] xs) ([] _) (.x ∷[ _ ] zs) | tri≈ _ P.refl _ = P.refl
   ... | tri< _ _ _ = P.refl
   ... | tri> _ _ _ = P.refl
   assoc (x ∷[ _ ] _) (y ∷[ _ ] _) ([] _) with compare x y
   assoc (x ∷[ _ ] xs) (.x ∷[ _ ] ys) ([] _) | tri≈ _ P.refl _ = P.refl
   ... | tri< _ _ _ = P.refl
   ... | tri> _ _ _ = P.refl

但是，我在尝试证明剩余案例时遇到了困难，该案例有很多子案例。特别是，我不知道如何在顶层下方的证明上下文中“重用”诸如compare x y ≡ tri< .a .¬b .¬c 之类的事实（例如，不引入辅助引理）。

我知道inspect（类固醇）成语提到here，并且已经取得了一些成功，但我的问题似乎是我想“重用”相关事实的上下文当我使用rewrite 来简化我使用inspect 保存的等式时，尚未建立。

因此，例如在以下子案例中，我可以使用以下 inspect 调用来捕获 compare x y 和 compare y z 的值：

   assoc (x ∷[ _ ] _) (y ∷[ _ ] _) (z ∷[ _ ] _)
         with compare x y | compare y z
         | P.inspect (hide (compare x) y) unit
         | P.inspect (hide (compare y) z) unit

然后rewrite 简化：

   assoc {l} {u} (x ∷[ l<x ] xs) (y ∷[ _ ] ys) (.y ∷[ _ ] zs)
         | tri< _ _ _ | tri≈ _ P.refl _ | P.[ eq ] | P.[ eq′ ] rewrite eq | eq′ =

但我认为rewrite 只会影响当时处于活动状态的目标。特别是，如果在证明的主体中我使用cong 转换到允许更多减少的嵌套上下文，我可能会暴露那些不会被重写的比较的新出现。 （请参阅下面的{!!} 了解我的意思。）我对减少的确切方式的理解有点模糊，因此我欢迎对此进行任何更正或澄清。

      begin
         x ∷[ _ ] merge (merge xs (y ∷[ _ ] ys)) (y ∷[ _ ] zs)
      ≡⟨ P.cong (λ xs → x ∷[ l<x ] xs) (assoc xs (y ∷[ _ ] ys) (y ∷[ _ ] zs)) ⟩
         x ∷[ _ ] merge xs (merge (y ∷[ _ ] ys) (y ∷[ _ ] zs))
      ≡⟨ P.cong (λ xs′ → x ∷[ _ ] merge xs xs′)
                {merge (y ∷[ _ ] ys) (y ∷[ _ ] zs)} {y ∷[ _ ] merge ys zs} {!!} ⟩
         x ∷[ _ ] merge xs (y ∷[ _ ] merge ys zs)
      ∎ where open import Relation.Binary.EqReasoning (P.setoid (SortedList l u))

（cong 的隐含参数需要在这里明确说明。）

当我把光标放在洞里时，我可以看到目标（有点意译）是

merge (y ∷[ _ ] ys) (y ∷[ _ ] zs) | compare y y ≡ y ∷[ _ ] merge ys zs

尽管之前有rewrite eq′。此外，在我的上下文中，我有

eq′  : compare y y ≡ tri≈ .¬a refl .¬c

这似乎正是我需要允许减少以取得进展以便refl 将完成证明案例。

这是剩余子案例的占位符。

   assoc (x ∷[ _ ] _) (_ ∷[ _ ] _) (z ∷[ _ ] _) | _ | _ | _ | _ = {!!}

我在这里有点不自信；我不知道我是否在类固醇上滥用inspect，完全以错误的方式进行证明，或者只是愚蠢。

有没有办法使用上下文中的eq′ 等价来允许继续进行缩减？

Answer 1

是的，根据Vitus' 的评论，需要再次对比较结果进行模式匹配。我最终定义了 3 个辅助引理，一个用于三分法的每个分支，然后在最终证明中使用每个引理两次。

merge≡ : ∀ {x l u} (l<x : l < x) {ι₁ : _} (xs : SortedList x u {ι₁}) {ι₂ : _} (ys : SortedList x u {ι₂}) →
         merge (x ∷[ l<x ] xs) (x ∷[ l<x ] ys) ≡ x ∷[ l<x ] merge xs ys
merge≡ {x} _ _ _ with compare x x
merge≡ _ _ _ | tri< _ x≢x _ = ⊥-elim (x≢x refl)
merge≡ _ _ _ | tri≈ _ refl _ = refl
merge≡ _ _ _ | tri> _ x≢x _ = ⊥-elim (x≢x refl)

merge< : ∀ {x y l u} (l<x : l < x) (l<y : l < y) (x<y : x < y)
         {ι₁ : _} (xs : SortedList x u {ι₁}) {ι₂ : _} (ys : SortedList y u {ι₂}) →
         merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) ≡ x ∷[ l<x ] merge xs (y ∷[ x<y ] ys)
merge< {x} {y} _ _ _ _ _ with compare x y
merge< _ _ _ _ _ | tri< _ _ _ = refl
merge< _ _ x<y _ _ | tri≈ x≮y _ _ = ⊥-elim (x≮y x<y)
merge< _ _ x<y _ _ | tri> x≮y _ _ = ⊥-elim (x≮y x<y)

merge> : ∀ {x y l u} (l<x : l < x) (l<y : l < y) (y<x : y < x)
         {ι₁ : _} (xs : SortedList x u {ι₁}) {ι₂ : _} (ys : SortedList y u {ι₂}) →
         merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) ≡ y ∷[ l<y ] merge (x ∷[ y<x ] xs) ys
merge> {x} {y} _ _ _ _ _ with compare x y
merge> _ _ y<x _ _ | tri< _ _ y≮x = ⊥-elim (y≮x y<x)
merge> _ _ y<x _ _ | tri≈ _ _ y≮x = ⊥-elim (y≮x y<x)
merge> _ _ _ _ _ | tri> _ _ _ = refl

尽管如此，样板的数量还是不能令人满意；我猜（几乎没有第一手经验）Coq 会更好。