`with`句の中のコンテキストが不十分

Question

私は以下の証明に立ち往生しています。

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

.

私は、コンテキストとして解釈された自然数γ、 A a de Bruijnインデックス、および識別子としてFin Γの要素を使用しています。 （私の質問の目的のために、これらはコンテキストや識別子として理解する必要はありませんが、それは直感に役立つかもしれません。）

名前の変更は文脈の形態学です：

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

.

私は次の2つの非常に単純な操作を定義します。最初のclose-varは、コンテキストから名前を削除し、残りのコンテキスト内の既存の名前にマッピングする名前を変更します。 2番目の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から得られた名前の変更は、同素体を形成します（私はかなり確実です）。しかし、私は以下の目標を意味しています：

   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> _ _ _ = {!!}

.

最初のケースは不可能であるべきですが、私は直前のケースで行ったように、矛盾を引き出すためにopen-varとy≡zを使用することができないようです。私はこれがパターン自体がばかげているからですが、私はこれのagdaを納得させる方法がわからない。

第2回、そしておそらく関連する問題は、残りの4つの目標の下で十分な削減が起こったのように見えないということです。それらはすべてy≮suc-zなどのwithパターンを含みます。しかし、私はこれらを排除するのに十分な実行を可能にするために、ネストされたtri< .a .¬b .¬c句を期待していました。私は何を間違っていますか？

（健全性チェックとして、確認が簡単です。

   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

.

など）

Answer 1

ネストされたwith句は大丈夫です。問題は、close-varの定義では、compare (toℕ y) (toℕ z)の結果だけでなく、引数yとzでも一致することです。もちろん、AGDAはどの関数式を使用するかを確かになさずに何かを減らすことはできません。

2番目の穴では、close-varはinject₁ zにパターンを合わせる必要がありますが、（そしてできません）。あなたはそれを抽象化しなければならず、そしてそれはそれが安全に1つの式を選ぶことができるように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

.

---

最初の穴の場合 - 上記のコードが役に立たない場合は、単純なleemmaを証明してください：

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

.

それから、あなたは矛盾を伴うことができます：

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

.

（StrictTotalOrderレコードを調べませんでしたが、この補題はすでにそこにあることがあります）。