pattern-matching - コンテキスト内で同等性を使用して削減を強制する

Answer 1

はい、Vitusのコメントによると、比較の結果で再度パターン マッチする必要があります。最終的に、3 つのヘルパー レンマを定義し、3 分法の各ブランチに 1 つずつ定義し、最終的な証明で各レンマを 2 回使用しました。

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の方がうまくいくと思います。