لم يتم تقييم السياق بشكل كافٍ داخل جملة `مع`

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

أنا أعمل مع الأعداد الطبيعية Γ المفسرة كسياقات، لا مؤشرات دي بروين، واستخدام عناصر 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

وهكذا دواليك.)

Answer 1

متداخلة with البنود بخير.المشكلة هي أنه في تعريف close-var, ، أنت لا تتطابق فقط على نتيجة compare (toℕ y) (toℕ z), ولكن أيضا على الحجج y و z أنفسهم.وبطبيعة الحال، لا يمكن لأجدا اختزال شيء ما دون التأكد من معادلة الدالة التي يجب استخدامها.

وفي الحفرة الثانية، 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 السجلات، ولكن من المحتمل أن تكون هذه الفكرة موجودة بالفعل).