유도의 재귀 적 단계에서 Fixpoint를 '펼치기'사용하기

Question

나는 coq에서 뭔가를 증명하려고 노력하고 있으며 같은 문제가 계속 발생합니다. 유도의 재귀 적 (nil이 아닌) 단계에서 Fixpoint의 정의를 펼치고 싶습니다.

목록 역 (REV)을 전개하기 전에 정의 :

n : nat 
    l' : natlist 
    IHl' : rev (rev l') = l' 
    ============================ 
    rev (rev (n :: l')) = n :: l' 

후 : 지금까지

n : nat 
    l' : natlist 
    IHl' : rev (rev l') = l' 
    ============================ 
    (fix rev (l : natlist) : natlist := match l with 
             | [ ] => [ ] 
             | h :: t => rev t ++ [h] 
             end) 
    ((fix rev (l : natlist) : natlist := match l with 
             | [ ] => [ ] 
             | h :: t => rev t ++ [h] 
             end) l' ++ [n]) = n :: l' 

좋지 예상대로 작품을 펼쳐, 여기에 예입니다. 이제는 simpl이 무응답이 아닌 경우입니다. n :: l'은 결코이 될 수 없으므로 일치하지 않는 경우 ([ ] => [ ])가 아닌 nil의 경우 만 단순화합니다. 정의.

불행히도 그것은 암묵적으로 그렇게하지 않습니다. 재귀 고정 점 정의의 unfold을 유도로 잘 재생하려면 어떻게해야합니까? 나는 어떻게합니까 :

n : nat 
    l' : natlist 
    IHl' : rev (rev l') = l' 
    ============================ 
    rev (rev l' ++ [n]) = n :: l' 

내부 rev에 대한 rev 정의에 따르면.

참고 : 목록 사용은 여기에 관계가 없으며 동일한 기술을 유도 식 정의 유형에 사용할 수 있습니다.

편집 : rev의 정의와 의 후속 상태의 증명.

Fixpoint rev (l:natlist) : natlist := 
    match l with 
    | nil => nil 
    | h :: t => rev t ++ [h] 
    end. 

Theorem rev_involutive : forall l : natlist, 
    rev (rev l) = l. 
Proof. 
    intros l. induction l as [| n l']. 
    - reflexivity. 
    - unfold rev. 

Answer 1

귀하의 After:은 기본적으로 rev (rev l' ++ [n]) 감소 당신이 일어나고보고 싶은 것을 의미합니다 (펼쳐진 rev로)이 이미 일어난 것입니다. 이제 rev (xs ++ ys) = rev ys ++ rev xs과 유사한 보조 정리를 증명하려고합니다.