Problèmes avec types dépendants en assistant à la preuve Coq

Question

Tenir compte de la langue d'expression simple suivante:

Inductive Exp : Set := 
| EConst : nat -> Exp 
| EVar : nat -> Exp 
| EFun : nat -> list Exp -> Exp. 

et son prédicat wellformedness:

Definition Env := list nat. 

Inductive WF (env : Env) : Exp -> Prop := 
| WFConst : forall n, WF env (EConst n) 
| WFVar : forall n, In n env -> WF env (EVar n) 
| WFFun : forall n es, In n env -> 
         Forall (WF env) es -> 
         WF env (EFun n es). 

qui stipule essentiellement que tous les symboles variables et fonctions doivent être définies dans l'environnement. Maintenant, je veux définir une fonction qui indique la décidabilité de WF prédicat:

Definition WFDec (env : Env) : forall e, {WF env e} + {~ WF env e}. 
    refine (fix wfdec e : {WF env e} + {~ WF env e} := 
      match e as e' return e = e' -> {WF env e'} + {~ WF env e'} with 
      | EConst n => fun _ => left _ _ 
      | EVar n => fun _ => 
         match in_dec eq_nat_dec n env with 
         | left _ _ => left _ _ 
         | right _ _ => right _ _      
         end 
      | EFun n es => fun _ => 
         match in_dec eq_nat_dec n env with 
         | left _ _ => _ 
         | right _ _ => right _ _      
         end 
      end (eq_refl e)) ; clear wfdec ; subst ; eauto. 

Le problème est de savoir comment affirmer que WF prédicat détient ou non pour une liste d'expressions dans le cas EFun. Je pense évidente était:

 ... 

    match Forall_dec (WF env) wfdec es with 

    ... 

Mais Coq refuse, en faisant valoir que l'appel récursif wfdec est mal formé. Ma question est la suivante: est-il possible de définir la décidabilité d'un tel prédicat de bonne forme sans modifier la représentation de l'expression?

Le code de travail complet est le suivant: gist.

Answer 1

Le problème est que Forall_dec est défini comme étant opaque dans la bibliothèque standard (à savoir, avec Qed au lieu de Defined). Pour cette raison, Coq ne sait pas que l'utilisation de wfdec est valide.

La solution immédiate à votre problème est de redéfinir Forall_dec afin qu'il soit transparent. Vous pouvez le faire en imprimant le terme de preuve que Coq génère et en le collant dans votre fichier source. J'ai ajouté un gist ici avec une solution complète. Inutile de dire que cette approche se prête à un gonflement, difficile à lire, et difficile à maintenir le code. Comme ejgallego soulignait dans sa réponse, votre meilleur pari dans ce cas est probablement de définir une fonction booléenne qui décide WF, et l'utiliser au lieu de WFDec. Le seul problème avec son approche, comme il l'a dit, est que vous aurez besoin d'écrire votre propre principe d'induction à Exp afin de prouver que la version booléenne décide en effet de la définition inductive. Le CPDT d'Adam Chlipala a un chapter sur les types inductifs qui donne un exemple d'un tel principe d'induction; il suffit de chercher "types inductifs imbriqués".

Answer 2

Pour contourner ce problème, vous pouvez définir le temps wf comme:

Definition wf (env : Env) := fix wf (e : Exp) : bool := 
    match e with 
    | EConst _ => true 
    | EVar v => v \in env 
    | EFun v l => [&& v \in env & all wf l] 
    end. 

qui consiste à utiliser habituellement de façon plus pratique. Cependant, cette définition sera plutôt inutile en raison de Coq générant le mauvais principe d'induction pour exp, car il ne détecte pas la liste. Ce que je fais habituellement est de fixer le principe d'induction manuellement, mais c'est coûteux. Exemple:

From Coq Require Import List. 
From mathcomp Require Import all_ssreflect. 

Set Implicit Arguments. 
Unset Printing Implicit Defensive. 
Import Prenex Implicits. 

Section ReflectMorph. 

Lemma and_MR P Q b c : reflect P b -> reflect Q c -> reflect (P /\ Q) (b && c). 
Proof. by move=> h1 h2; apply: (iffP andP) => -[/h1 ? /h2 ?]. Qed. 

Lemma or_MR P Q b c : reflect P b -> reflect Q c -> reflect (P \/ Q) (b || c). 
Proof. by move=> h1 h2; apply: (iffP orP) => -[/h1|/h2]; auto. Qed. 

End ReflectMorph. 

Section IN. 
Variables (X : eqType). 

Lemma InP (x : X) l : reflect (In x l) (x \in l). 
Proof. 
elim: l => [|y l ihl]; first by constructor 2. 
by apply: or_MR; rewrite // eq_sym; exact: eqP. 
Qed. 

End IN. 

Section FORALL. 

Variables (X : Type) (P : X -> Prop). 
Variables (p : X -> bool). 

Lemma Forall_inv x l : Forall P (x :: l) -> P x /\ Forall P l. 
Proof. by move=> U; inversion U. Qed. 

Lemma ForallP l : (forall x, In x l -> reflect (P x) (p x)) -> reflect (Forall P l) (all p l). 
Proof. 
elim: l => [|x l hp ihl /= ]; first by constructor. 
have/hp {hp}hp : forall x : X, In x l -> reflect (P x) (p x). 
    by move=> y y_in; apply: ihl; right. 
have {ihl} ihl := ihl _ (or_introl erefl). 
by apply: (iffP andP) => [|/Forall_inv] [] /ihl hx /hp hall; constructor. 
Qed. 

End FORALL. 

Inductive Exp : Type := 
| EConst : nat -> Exp 
| EVar : nat -> Exp 
| EFun : nat -> list Exp -> Exp. 

Lemma Exp_rect_list (P : Exp -> Type) : 
    (forall n : nat, P (EConst n)) -> 
    (forall n : nat, P (EVar n)) -> 
    (forall (n : nat) (l : seq Exp), (forall x, In x l -> P x) -> P (EFun n l)) -> 
    forall e : Exp, P e. 
Admitted. 

Definition Env := list nat. 

Definition wf (env : Env) := fix wf (e : Exp) : bool := 
    match e with 
    | EConst _ => true 
    | EVar v => v \in env 
    | EFun v l => [&& v \in env & all wf l] 
    end. 

Inductive WF (env : Env) : Exp -> Prop := 
| WFConst : forall n, WF env (EConst n) 
| WFVar : forall n, In n env -> WF env (EVar n) 
| WFFun : forall n es, In n env -> 
         Forall (WF env) es -> 
         WF env (EFun n es). 

Lemma WF_inv env e (wf : WF env e) : 
    match e with 
    | EConst n => True 
    | EVar n => In n env 
    | EFun n es => In n env /\ Forall (WF env) es 
    end. 
Proof. by case: e wf => // [n|n l] H; inversion H. Qed. 

Lemma wfP env e : reflect (WF env e) (wf env e). 
Proof. 
elim/Exp_rect_list: e => [n|n|n l ihe] /=; try repeat constructor. 
    by apply: (iffP idP) => [/InP|/WF_inv/InP //]; constructor. 
apply: (iffP andP) => [[/InP ? /ForallP H]|/WF_inv[/InP ? /ForallP]]. 
    by constructor => //; exact: H. 
by auto. 
Qed.