एग्डा में क्लॉज के साथ/पुनः लिखने वाले प्रकार, या, पदार्थ के बजाय पुनर्लेखन का उपयोग कैसे करें?

Question

पहले कुछ उबाऊ आयात:

import Relation.Binary.PropositionalEquality as PE 
import Relation.Binary.HeterogeneousEquality as HE 
import Algebra 
import Data.Nat 
import Data.Nat.Properties 
open PE 
open HE using (_≅_) 
open CommutativeSemiring commutativeSemiring using (+-commutativeMonoid) 
open CommutativeMonoid +-commutativeMonoid using() renaming (comm to +-comm) 

अब मान लीजिए कि मैं एक प्रकार से, कहते हैं, प्राकृतिक की सूचीबद्ध करा सकते हैं।

postulate Foo : ℕ -> Set 

और मैं इस प्रकार के Foo पर काम कार्यों के बारे में कुछ समानताओं को साबित करना चाहते हैं। चूंकि एग्डा बहुत स्मार्ट नहीं है, ये विषम समानताएं होंगी। एक साधारण उदाहरण

foo : (m n : ℕ) -> Foo (m + n) -> Foo (n + m) 
foo m n x rewrite +-comm n m = x 

bar : (m n : ℕ) (x : Foo (m + n)) -> foo m n x ≅ x 
bar m n x = {! ?0 !} 

पट्टी में लक्ष्य

Goal: (foo m n x | n + m | .Data.Nat.Properties.+-comm n m) ≅ x 
———————————————————————————————————————————————————————————— 
x : Foo (m + n) 
n : ℕ 
m : ℕ 

है होगा क्या इन | के गोल में कर रहे हैं? और मैं इस प्रकार की अवधि का निर्माण कैसे शुरू करूं?

इस मामले में, मैं subst के साथ मैन्युअल रूप से प्रतिस्थापन करके समस्या के आसपास काम कर सकता हूं, लेकिन यह बड़े प्रकार और समीकरणों के लिए वास्तव में बदसूरत और थकाऊ हो जाता है।

foo' : (m n : ℕ) -> Foo (m + n) -> Foo (n + m) 
foo' m n x = PE.subst Foo (+-comm m n) x 

bar' : (m n : ℕ) (x : Foo (m + n)) -> foo' m n x ≅ x 
bar' m n x = HE.≡-subst-removable Foo (+-comm m n) x 

Answer 1

उन पाइप संकेत मिलता है कि कमी सवाल में भाव का परिणाम लंबित निलंबित कर दिया है, और यह आम तौर पर तथ्य यह है कि आप एक with ब्लॉक जिसका परिणाम आप आगे बढ़ने के लिए पता करने की जरूरत थी निर्भर करता है। ऐसा इसलिए है क्योंकि rewrite निर्माण किसी भी सहायक मूल्यों के साथ-साथ refl पर एक मैच के बाद प्रश्न में अभिव्यक्ति के with तक फैलता है।

इस मामले में, यह सिर्फ है कि आप refl पर एक with ब्लॉक और पैटर्न मैच में +-comm n m लागू करने के लिए (और आप शायद दायरे में भी n + m लाने के लिए, के रूप में यह पता चलता है की आवश्यकता होगी की जरूरत का मतलब है, इसलिए समानता कुछ है के बारे में बात करने के लिए)। आगाडा मूल्यांकन मॉडल काफी सरल है, और यदि आप पैटर्न पर कुछ मिलान करते हैं (रिकॉर्ड्स पर गलत पैटर्न मैचों को छोड़कर), तब तक यह कम नहीं होगा जब तक कि आप उसी चीज़ पर पैटर्न मिलान न करें। आप अपने सबूत में एक ही अभिव्यक्ति द्वारा पुनः लिखने में भी सक्षम हो सकते हैं, क्योंकि यह केवल आपके लिए उल्लिखित करता है।

दरअसल, अगर आप को परिभाषित:

f : ... 
f with a | b | c 
... | someDataConstructor | boundButNonConstructorVariable | someRecordConstructor = ... 

और फिर आप अभिव्यक्ति के रूप में f को देखें, तो आप क्योंकि यह, someDataConstructor पर से मेल खाता है, पाइप आप केवल अभिव्यक्ति a के लिए मनाया मिल जाएगा बहुत से तो कम से कम f प्राप्त करने के लिए आपको a पेश करने की आवश्यकता होगी और फिर someDataConstructor से मिलान करें। दूसरी तरफ, b और c, हालांकि उन्हें ब्लॉक के साथ पेश किया गया था, कोई रोकथाम मूल्यांकन नहीं किया गया है, क्योंकि b पैटर्न मिलान नहीं करता है, और c का someRecordConstructor एकमात्र संभावित कन्स्ट्रक्टर होने के लिए स्थिर रूप से जाना जाता है क्योंकि यह एक रिकॉर्ड है ईटा के साथ टाइप करें।