pattern-matching - 在上下文中使用等价物来强制减少

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 保存的相等性.

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

   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为了转移到允许更多缩减的嵌套上下文，我可能会公开那些不会被重写的比较的新出现。 (有关我指的位置，请参阅下面的 {!!}。)我对减少 yield 的确切方式的理解有点模糊，所以我欢迎对此进行任何更正或澄清。

      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 会更好。