Agda에서 언어의 연결 증명이 연관되어 있습니다.

Question

저는 Agda 언어가 처음이고 Agda를 사용하여 공식 언어를 연구 중입니다.

언어의 연결이 연관성이 있음을 증명할 때 몇 가지 문제가 있습니다.

LangAssoc : ∀{Σ}{l1 l2 l3 : Language Σ}{w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w 
LangAssoc {l1 = l1} (conc x (conc y z)) = conc (conc (subst l1 (++Assoc _ _ _) x) y) z 

은 "++ 연합회는"목록의 연결의 연관성의 증거 : 증거는 AGDA 다음 코드에서 "++ 연합회"에 대한 단어를 찾을 수 없습니다로 노란색이 강조 될 것입니다 .

는

Language : ℕ → Set₁ 
Language a = Word a → Set 

data LangConc {Σ} (l1 l2 : Language Σ) : Language Σ where 
    conc : ∀{w1 w2} → l1 w1 → l2 w2 → (LangConc l1 l2) (w1 ++ w2) 

그래서 나는 누군가가 내가이 상황에서 잘못하고있는 무슨에 설명하고 나에게 문제를 해결하는 방법에 대한 몇 가지 힌트를 줄 수 있는지 묻고 싶다 :

언어와 연결은 다음과 같이 정의된다 .

편집 1 : 나는 연결 외부 SUBST를 사용하여 다른 방법을 시도했습니다,하지만 난이 상황에 갇혀있어 :

LangAssoc : ∀{Σ} {l1 l2 l3 : Language Σ} {w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w 
LangAssoc {Σ} {l1 = l1} {l2 = l2} {l3 = l3} (conc x (conc y z)) = subst {!!} (++Assoc {Σ} _ _ _) (conc {Σ} (conc {Σ} x y) z) 

편집 2 : 난 그냥 다음 코드와 결과와 시도했습니다 오류 메시지.

---

LangAssoc : ∀{Σ} {l1 l2 l3 : Language Σ} {w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w 
LangAssoc {l1 = l1} {w = w} (conc x (conc y z)) = ? 

w1 ++ w2 != w of type List (Fin Σ) 
when checking that the pattern conc x (conc y z) has type 
LangConc l1 (LangConc l2 l3) w 

---

편집 3 : 그냥 제안 세 조각으로 승 단어를 위반하여 다른 시도를했다.

LangAssoc : ∀{Σ : ℕ}{l1 l2 l3 : Language Σ}{w1 w2 w3 : Word Σ} 
      → (LangConc l1 (LangConc l2 l3)) (w1 ++ w2 ++ w3) 
      → (LangConc (LangConc l1 l2) l3) ((w1 ++ w2) ++ w3) 
LangAssoc (conc {w1} x (conc {w2} {w3} y z)) 
    = subst (LangConc (LangConc _ _) _) (++Assoc w1 w2 w3) (conc (conc x y) z) 

---

오류 메시지 :

목록 (핀 Σ)는 말씀 Σ의 정의입니다

w4 != w1 of type List (Fin Σ) 
when checking that the pattern conc {w1} x (conc {w2} {w3} y z) has 
type LangConc l1 (LangConc l2 l3) (w1 ++ w2 ++ w3) 

.

Answer 1

++은 주입식이 아니기 때문에 (심지어 Agda가 알지도 못함) x ++ (y ++ z) ?= _1 ++ (_2 ++ _3)을 해결하려고 할 때 Agda가 선택할 수있는 가장 일반적인 해결책은 없습니다.

예를 들어 _1 = [], _2 = x, _3 = y ++ z을 말합니다.

편집 : 그것은 정말 이해가 LangConc l1 (LangConc l2 l3) w에 일치하는 패턴을 가진 후 w을 소개 할 수 않습니다 w이 3 개 부분 (l1, l2 및 l3에 correponding 사람)에 헤어 졌되었습니다. 이 부분들을 소개하는 것이 훨씬 더 흥미 롭습니다 :

LangAssoc (conc {w1} x (conc {w2} {w3} y z)) = 
    subst (LangConc (LangConc _ _) _) (++Assoc w1 w2 w3) (conc (conc x y) z)