pattern-matching - Agda:模拟 Coq 的重写策略

Question

我有一些使用 Coq 的经验，现在正在学习 Agda。我正在研究插入排序的正确性证明，并且已经达到了我想要执行类似于 Coq 重写策略的程度。目前，我有:

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Sum

data list : Set where
  nil : list
  cons : ℕ -> list -> list

data sorted (n : ℕ) : list -> Set where
  nilSorted : sorted n nil
  consSorted : ∀ hd tl -> hd ≥ n -> sorted hd tl -> sorted n (cons hd tl)

leMin : ∀ x y -> x ≤ y -> (x ⊓ y) ≡ x
leMin zero zero p = refl
leMin zero (suc y) p = refl
leMin (suc x) zero ()
leMin (suc x) (suc y) (s≤s p) = cong suc (leMin x y p)

insert : ℕ → list → list
insert x l = {!!}

intDec : ∀ x y → x ≤ y ⊎ x > y
intDec x y = {!!}

insertCorrect : ∀ {n} -> ∀ x l -> sorted n l -> sorted (n ⊓ x) (insert x l)
insertCorrect {n} x nil p with intDec n x
insertCorrect {n} x nil p | inj₁ x₁ with (leMin n x x₁) 
... | c = {c }0

我的证明上下文如下所示:

Goal: sorted (n ⊓ x) (cons x nil)
————————————————————————————————————————————————————————————
p  : sorted n nil
c  : n ⊓ x ≡ n
x₁ : n ≤ x
x  : ℕ
n  : ℕ

我尝试分解 c，希望用 n 替换出现的 (n ⊓ x)，但是，我得到出现以下错误:

I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
n₁ ⊓ x₂ ≟ n₁
when checking that the expression ? has type
sorted (n ⊓ x) (cons x nil)

基本上，我希望能够执行重写，以便达到以下目的:

Goal: sorted n (cons x nil)
————————————————————————————————————————————————————————————
p  : sorted n nil
x₁ : n ≤ x
x  : ℕ
n  : ℕ

关于如何进行的任何想法？

Answer 1

您可以使用 Agda 关键字rewrite 对您的目标应用命题等价:

insertCorrect : ∀ {n} -> ∀ x l -> sorted n l -> sorted (n ⊓ x) (insert x l)
insertCorrect {n} x nil p with intDec n x
insertCorrect {n} x nil p | inj₁ x₁ rewrite leMin n x x₁ = ?

这里，? 中的目标正如您所希望的那样:

Goal: sorted n (cons x nil)
————————————————————————————————————————————————————————————
p  : sorted n nil
x₁ : n ≤ x
x  : ℕ
n  : ℕ