Her biri bir veya iki örtük değişkene A B: Type bağlı olabilecek bir dizi işlevim olduğunu varsayalım. Bunu nasıl belirleyebilirim? Yani bu değişkenleri değişken listesine ekleyin ve bunları örtük olarak ayarlayın.Coq: örtük değişkenler ekleniyor
En belirgin yöntem, tanımlarına {A B: Type} eklemektir. Bununla birlikte, gerçek hayatta ve orta derecede karmaşık gelişmelerde, dolaylı olarak paylaşılmış bu türden çıkarımlar, 6-10 giriş uzunluğunda olabilir ve karmaşık tipler içerebilir, böylece okunması zor olan fonksiyon tanımlamaları ve benzerliklerini anlamak ya da belirtilen türlerde değişiklik yapmak daha da zorlaşır. Böylece bu çözüm geçerli değildir.
Tüm işlevleri bir bölüme veya modüle ekleyebilirim ve Variables (A B: Type) etc'u en başa yazabilirim, ancak bu, değişkenleri örtük hale getirmez ve bölümün sonundaki tüm işlevler için bağımsız değişkenleri el ile ayarlamak zorunda kalırdım. Daha da kötüsü, tüm değişkenleri paylaşırdı. Yani Ben
Section sect.
Variable A B: Type.
Definition f (t: A -> Type) := (..).
Definition g (t: A -> Type) (s: B -> Type) := G (f t) (f s).
End sect.
ilan etmeleri halinde sA -> Type olmadığı için esasen f sadece keyfi bir tip ailesini gerektirir rağmen, daha sonra g kabul olmaz (G yaklaşık iki değişkenli fonksiyonudur).
Bir bölüm oluşturabilir ve Context {A B: Type} bildirebilirim. Bu, bu değişkenlerin tüm işlevler için örtülü olmasını sağlar, ancak önceki durumda olduğu gibi paylaşım sorunu hala devam eder. Bu yüzden, işlevlerimi örtük argümanlarının farklı değerleri ile Sect.1'den çağırabilmem için işlevlerimi çeşitli bölümlere ayırmam gerekirdi. Bu işe yarıyor ama çirkin ve her bölümün düzgün bir şekilde çağırabilmem için 2-3 bölüm uzunluğunda olması gereken bir durumu kolayca hayal edebiliyorum.
Daha iyi bir çözüm var mı?
Generalizable All Variables.
Definition g `(t: A -> Type) `(s: B -> Type) := G (f t) (f s).
Paylaşım sorununu anladığımdan emin değilim. 'Bağlam {A: Tür}' kullanma ve 'f' ve' g' için 'A -> Type' parametresini almanın ne gibi problemleri vardır? –
Üzgünüm, ama hala kafam karıştı. “G” nin tanımını değiştiremediniz, bu da “B” yerine “A” üzerinde parametrelendirilmiş tipler almasını sağladı mı? –
Sanırım şimdi düzgün çalışması gerekiyor. –