Правила вывода для заказа подпоследовательности

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, которые избегают этой ошибки объединения, но затем другие доказательства имеют, казалось бы, абсурдные узоры.

Мне нужна помощь с версией порядка подпоследовательности (с доказательствами надежности и полноты, что было бы неплохо).

Существуют ли какие-либо общие эвристики, которые нужно попробовать при преобразовании предложения в формульной форме в форму вывода/данных?

Спасибо!

Answer 1

Мы получаем ошибки унификации при совмещении рисунка на, казалось бы, невозможных q.

Это обычная проблема с «зеленой слизью». По словам Конор МакБрайд:

Присутствие «зеленой слизью» - определенной функции в типах возвращаемых конструкторов - это знак опасности.

См. 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)