У меня есть некоторый опыт использования 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 ⊓ x)
на n
, однако получаю следующую ошибку:
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 : ℕ
Есть идеи, как действовать?