子序列顺序的推理规则

Question

我正在用子序列顺序做一些练习，

record _⊑₀_ {X : Set} (xs ys : List X) : Set where
 field
  indices : Fin (length xs) → Fin (length ys)
  embed   : ∀ {a b : Fin (length xs)} → a < b → indices a < indices b
  eq      : ∀ {i : Fin (length xs)} → xs ‼ i ≡ ys ‼ (indices i)

哪里

_‼_ : ∀ {X : Set} → (xs : List X) → Fin (length xs) → X
[] ‼ ()
(x ∷ xs) ‼ fzero = x
(x ∷ xs) ‼ fsuc i = xs ‼ i

是通常的安全查找。

虽然记录版本很好，但我想改用推理规则，因为这可能比每次构建嵌入并证明它们的属性更容易。

所以我尝试以下操作，

infix 3 _⊑₁_
data _⊑₁_ {X : Set} : (xs ys : List X) → Set where
 nil   : ∀ {ys} → [] ⊑₁ ys
 embed : ∀ {x y} → x ≡ y → x ∷ [] ⊑₁ y ∷ []
 cons  : ∀ {xs₁ ys₁ xs₂ ys₂} → xs₁ ⊑₁ ys₁ → xs₂ ⊑₁ ys₂ → xs₁ ++ xs₂ ⊑₁ ys₁ ++ ys₂

这看起来很有希望。虽然我很难证明它是录音版本的声音和完整反映。

总之，后序顺序是可传递的，这就有点麻烦了：

⊑₁-trans : ∀ {X : Set} (xs ys zs : List X) → xs ⊑₁ ys → ys ⊑₁ zs → xs ⊑₁ zs
⊑₁-trans .[] ys zs nil q = nil
⊑₁-trans ._ ._ [] (embed x₁) q = {! q is absurd !}
⊑₁-trans ._ ._ (x ∷ zs) (embed x₂) q = {!!}
⊑₁-trans ._ ._ zs (cons p p₁) q = {!!}

在看似不可能的模式上进行模式匹配时，我们会遇到统一错误 q。因此，我尝试了其他 data 版本的命令来避免这种统一错误，但其他证明具有看似荒谬的模式。

我需要一些有关 data 版本的子序列顺序的帮助（具有可靠性和完整性证明，这很好）。

将公式形式的命题转换为 inference/data 形式时，是否有任何通用的启发式方法可以尝试？

谢谢！

Answer 1

We get unification errors when pattern matching on a seemingly impossible pattern q.

这是常见的 "green slime" 问题。用 Conor McBride 的话来说：

The presence of ‘green slime’ — defined functions in the return types of constructors — is a danger sign.

请参阅 here 了解一些打败绿色史莱姆的技巧。

对于 _⊑_ 使用 order preserving embeddings:

infix 3 _⊑_

data _⊑_ {α} {A : Set α} : List A -> List A -> Set α where
  stop : [] ⊑ []
  skip : ∀ {xs ys y} -> xs ⊑ ys -> xs     ⊑ y ∷ ys
  keep : ∀ {xs ys x} -> xs ⊑ ys -> x ∷ xs ⊑ x ∷ ys

⊑-trans : ∀ {α} {A : Set α} {xs ys zs : List A} -> xs ⊑ ys -> ys ⊑ zs -> xs ⊑ zs
⊑-trans  p        stop    = p
⊑-trans  p       (skip q) = skip (⊑-trans p q)
⊑-trans (skip p) (keep q) = skip (⊑-trans p q)
⊑-trans (keep p) (keep q) = keep (⊑-trans p q)

子序列顺序的推理规则

Inference rules for subsequence order

list

sequence

agda