coq에 암시 적 증명 객체를 쓰는 데있어 불가능한 패턴

Question

종속 유형이있는 프로그래밍 언어로 coq를 사용하려고합니다. 비어 있지 있다는 증거가있다 제공

Inductive Good : list nat -> Set := 
    | GoodNonEmpty : forall h t, Good (h :: t). 

Definition get_first(l : list nat)(good : Good l) : nat := 
    match l with 
    | h :: t => h 
    | nil => 
     match good with 
     end 
    end. 

내가 비어 있지 않은 목록의 유형을 정의하고 이러한 목록의 첫 번째 요소를 가져 오는 함수를 만들 : 나는 다음과 같은 작은 프로그램을 만들었습니다. 헤드 항목이 두 항목으로 구성된 경우를 잘 처리하지만 빈 목록의 불가능한 경우는 처리 할 수 ​​없습니다. 내가 coq에서 이것을 어떻게 할 수 있습니까? 당신의 시도보다 간단하다 그것을 할 수

Answer 1

한 가지 방법은 다음과 같습니다 여기

Definition get_first (l : list nat) (good : Good l) : nat := 
    match good with 
    | GoodNonEmpty h _ => h 
    end. 

당신이 그것을하고 싶었던 방법으로 그것을 할 수있는 방법입니다. "Good nil"이 존재하지 않고 인라인되어 있음을 증명하는 것은 매우 장황합니다.

Definition get_first (l : list nat) (good : Good l) : nat := 
    (
    match l as l' return (Good l' -> nat) with 
    | nil => 
     fun (goodnil : Good nil) => 
     (
      match goodnil in (Good l'') return (nil = l'' -> nat) with 
      | GoodNonEmpty h t => 
      fun H => False_rect _ (nil_cons H) 
      end 
     ) 
     (@eq_refl _ nil) 
    | h :: _ => fun _ => h 
    end 
) good. 

분명히 외부의 일부를 정의하고 다시 사용할 수 있습니다. 나는 최선의 관행을 알지 못한다. 어쩌면 누군가 똑같은 일을하는 더 짧은 길을 택할 수도 있습니다.

---

편집 : 그런 다음 수

Definition get_first' (l : list nat) (good : Good l) : nat. 
Proof. 
    destruct l. inversion good. exact n. 
Defined. 

: 그런데

, 당신은 증거 모드에서 훨씬 쉬운 방법으로, 거의 같은 결과에 얻을 수

Print get_first'. 

Coq가 어떻게 정의하는지 확인하십시오. 그러나, 더 복잡 것을 위해, 당신은 솔루션으로 제안 무엇 #coq의 IRC 채널에서 gdsfhl 다음 더 나을 수 있습니다

http://paste.in.ua/4782/

당신은 그 골격의 일부를 제공하기 위해 refine 전술을 사용하고 있음을 알 수 있습니다 쓰고, 누락 된 증명을 연기하기위한 용어.