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

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