Недостаточно оцененный контекст внутри предложения `with`

Я застрял на следующем доказательстве.

module Temp where

   open import Data.Empty
   open import Data.Fin hiding (compare)
   open import Data.Nat hiding (compare); open import Data.Nat.Properties
   open import Function
   open import Level
   open import Relation.Binary
   open import Relation.Binary.PropositionalEquality

Я работаю с натуральными числами Γ, истолковываемыми как контексты, индексами а-ля де Брейна и использую элементы Fin Γ в качестве идентификаторов. (Для целей моего вопроса не нужно понимать их как контексты и идентификаторы, но это может помочь с интуицией.)

Переименование — это контекстный морфизм:

   Ren : Rel ℕ Level.zero
   Ren Γ Γ′ = Fin Γ → Fin Γ′

Теперь я определяю следующие две очень простые операции. Первый, close-var, дает переименование, которое удаляет имя из контекста, сопоставляя его с существующим именем в оставшемся контексте. Второй, open-var, дает переименование, которое делает обратное, вставляя новое имя в контекст в определенном месте. Чтобы найти точку вставки или удаления в контексте, я сравниваю toℕ, так как еще не понял, как использовать Data.Fin.compare.

   open StrictTotalOrder strictTotalOrder
   open DecTotalOrder decTotalOrder renaming (refl to ≤-refl; trans to ≤-trans)
   open import Data.Fin.Props using (bounded)

   close-var : ∀ {Γ} → Fin Γ → Fin (suc Γ) → Fin (suc Γ) → Fin Γ
   close-var _ y z with compare (toℕ y) (toℕ z)
   close-var _ _ zero | tri< () _ _
   close-var _ _ (suc z) | tri< _ _ _ = z
   close-var x _ _ | tri≈ _ _ _ = x
   close-var _ zero _ | tri> _ _ ()
   close-var _ (suc y) z | tri> _ _ z<suc-y = 
      fromℕ≤ (≤-trans z<suc-y (bounded y))

   open-var : ∀ {Γ} → Fin (suc Γ) → Fin Γ → Fin (suc Γ)
   open-var y z with compare (toℕ y) (toℕ z)
   ... | tri< _ _ _ = suc z
   ... | tri≈ _ _ _ = suc z
   ... | tri> _ _ _ = inject₁ z

Единственная нетривиальная часть этих определений — это последний случай close-var, который должен приводить от большего контекста к меньшему.

Для фиксированных аргументов переименования, полученные из close-var и open-var, образуют изоморфизм (я вполне уверен). Однако я застрял в понимании следующих целей:

   close∘open≡id : ∀ {Γ} (x : Fin Γ) (y : Fin (suc Γ)) (z : Fin Γ) → 
                   (close-var x y ∘ open-var y) z ≡ z
   close∘open≡id _ y z with compare (toℕ y) (toℕ z)
   close∘open≡id _ y z | tri< _ _ _ with compare (toℕ y) (suc (toℕ z))
   close∘open≡id _ _ _ | tri< _ _ _ | tri< _ _ _ = refl
   close∘open≡id _ _ _ | tri< y<z _ _ | tri≈ y≮suc-z _ _ = 
      ⊥-elim (y≮suc-z (≤-step y<z))
   close∘open≡id _ _ _ | tri< y<z _ _ | tri> y≮suc-z _ _ = 
      ⊥-elim (y≮suc-z (≤-step y<z))
   close∘open≡id _ y z | tri≈ _ _ _ with compare (toℕ y) (suc (toℕ z))
   close∘open≡id _ _ _ | tri≈ _ _ _ | tri< _ _ _ = refl
   close∘open≡id _ _ _ | tri≈ _ y≡z _ | tri≈ y≮suc-z _ _ rewrite y≡z = 
      ⊥-elim (y≮suc-z ≤-refl)
   close∘open≡id _ _ _ | tri≈ _ y≡z _ | tri> y≮suc-z _ _ = {!!}
   close∘open≡id _ y z | tri> _ _ _ with compare (toℕ y) (toℕ (inject₁ z))
   close∘open≡id _ _ _ | tri> _ _ _ | tri< _ _ _ = {!!}
   close∘open≡id _ _ _ | tri> _ _ _ | tri≈ _ _ _ = {!!}
   close∘open≡id _ _ _ | tri> _ _ _ | tri> _ _ _ = {!!}

Первый случай должен быть невозможен, но я, кажется, не могу использовать y≡z и y≮suc-z для вывода противоречия, как я сделал в непосредственно предыдущем случае. Я думаю, это потому, что сама схема абсурдна, но я не знаю, как убедить в этом Агду.

Вторая и, возможно, связанная с этим проблема заключается в том, что не похоже, что произошло достаточное сокращение по четырем оставшимся целям. Все они содержат with шаблонов, таких как tri< .a .¬b .¬c. Но я ожидал, что вложенные предложения with позволят выполнить достаточно, чтобы устранить их. Что я делаю неправильно?

(В качестве проверки работоспособности это легко проверить:

   sub : ∀ {Γ} (x : Fin Γ) (y : Fin (suc Γ)) → Ren Γ Γ
   sub x y = close-var x y ∘ open-var y

   Γ : ℕ
   Γ = 5

   ρ : Ren Γ Γ
   ρ = sub (suc (zero)) (suc (suc (suc zero)))

   ex₁ : ρ zero ≡ zero
   ex₁ = refl

   ex₂ : ρ (suc zero) ≡ suc zero
   ex₂ = refl

   ex₃ : ρ (suc (suc (zero))) ≡ suc (suc zero)
   ex₃ = refl

   ex₄ : ρ (suc (suc (suc (zero)))) ≡ suc (suc (suc zero))
   ex₄ = refl

и так далее.)


pattern-matching proof agda
person Roly    schedule 25.02.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вложенные предложения with в порядке. Проблема в том, что в определении close-var вы сопоставляете не только результат compare (toℕ y) (toℕ z), но и сами аргументы y и z. И, конечно же, Agda не может что-то уменьшить, не зная, какое уравнение функции использовать.

Во втором отверстии close-var должно совпасть с inject₁ z, но вы этого не сделаете (и не сможете). Вы также должны абстрагироваться от этого, а затем достаточно сопоставить шаблон, чтобы убедить Agda в том, что он может безопасно выбрать одно уравнение.

close∘open≡id x y z | tri> _ _ _
  with inject₁ z | compare (toℕ y) (toℕ (inject₁ z))
... | tri> _ _ _ | Fin.zero  | tri< () _ _
... | tri> _ _ _ | Fin.suc r | tri< _  _ _ = {!!}  -- goal is r ≡ z

Что касается первой дыры - если код выше не помогает, просто докажите простую лемму:

≡→≤ : {x y : ℕ} → x ≡ y → x ≤ y
≡→≤ refl = ≤-refl

И тогда вы можете получить противоречие через:

y≮suc-z (s≤s (≡→≤ y≡z))

(Я не смотрел записи StrictTotalOrder, но есть вероятность, что эта лемма уже там).

person Vitus    schedule 25.02.2014
comment
Хорошо, это имеет смысл, и это помогает. Еще раз спасибо :) - person Roly; 26.02.2014