Harita bul id = id idris?

Question

Genelde idris ve teorem ispatlarıyla oynamaya başladım. İnternetteki temel bilgilerin ispatlarının örneklerinin çoğunu takip edebilirim, bu yüzden kendi başıma keyfi bir şey denemek istedim. Yani, haritanın aşağıdaki temel özellik için kanıt terim yazmak istiyorum:

map : (a -> b) -> List a -> List b 
prf : map id = id 

Sezgisel, ben kanıtı çalışması gerektiğini nasıl tahmin edebilirsiniz: keyfi bir liste l alın ve harita kimliği l olasılıklarını analiz edin. L boş olduğunda, belli ki; l boş olmadığında, işlev uygulamasının eşitliği koruduğu kavramı temel alır.

prf' : (l : List a) -> map id l = id l 

Tüm açıklamada için gibi: Yani, böyle bir şey yapabilirsiniz. İlgili fonksiyonların eşitliğinin bir kanıtı haline nasıl dönüştürebilirim?

Answer 1

Yapamazsınız. İdris'in tip teorisi (Coq's ve Agda gibi) genel genişlemeyi desteklemez. f ve g iki işlevi göz önüne alındığında, "aynı davranın", asla Not (f = g) olduğunu kanıtlayamayacaksınız, ancak f ve g yalnızca alfa ve eta eşdeğeri kadar tanımlanmışsa f = g olduğunu kanıtlayabileceksiniz. Ne yazık ki, yüksek mertebeden fonksiyonları dikkate aldığınızda işler daha da kötüleşir; Coq standart kitaplığında böyle bir teorem var, ancak şu anda onu bulamıyorum veya hatırlamıyorum.