Impossible d'écrire un objet de preuve implicite dans coq

Question

J'essaie d'utiliser coq comme langage de programmation avec un type dépendant. J'ai créé le petit programme suivant:

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. 

I défini un type de liste non vide et crée une fonction qui obtient le premier élément d'une telle liste fournie il y a une preuve que ce n'est pas vide. Je gère bien le cas où les articles de tête se composent de deux éléments, mais je ne peux pas gérer le cas impossible de la liste vide. Comment puis-je faire ça en coq?

Answer 1

Une façon de le faire qui est plus simple que votre essai est:

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

Voici une façon de le faire de la manière que vous vouliez faire. Vous remarquerez qu'il est très verbeux de prouver que "Good nil" n'existe pas, inline.

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. 

Vous pouvez sûrement en définir une partie à l'extérieur et la réutiliser. Je ne suis pas au courant des meilleures pratiques cependant. Peut-être que quelqu'un peut venir avec une façon plus courte de faire la même chose.

---

EDIT:

Par ailleurs, vous pouvez obtenir à peu près le même résultat, d'une manière beaucoup plus facile, en mode démonstration:

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

Vous pouvez alors:

Print get_first'. 

Pour voir comment Coq le définit. Cependant, pour des choses plus impliqués, vous pourriez être mieux suivre ce qui gdsfhl du canal IRC#coq proposé comme solution:

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

Vous pouvez voir qu'il utilise la tactique refine pour fournir une partie du squelette du terme pour écrire, et différer les preuves manquantes.