Consider the following simple expression language:
Inductive Exp : Set :=
| EConst : nat -> Exp
| EVar : nat -> Exp
| EFun : nat -> list Exp -> Exp.
and its wellformedness predicate:
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).
which basically states that every variable and function symbols must be defined in the environment. Now, I want to define a function that states the decidability of WF
predicate:
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.
The trouble is how to state that WF
predicate holds or not for a list of expressions in the EFun
case. My obvious guess was:
...
match Forall_dec (WF env) wfdec es with
...
But Coq refuses it, arguing that the recursive call wfdec
is ill-formed. My question is: Is it possible to define decidability of such wellformedness predicate without changing the expression representation?
The complete working code is at the following gist.
The problem is that Forall_dec
is defined as opaque in the standard library (that is, with Qed
instead of Defined
). Because of that, Coq does not know that the use of wfdec
is valid.
The immediate solution to your problem is to redefine Forall_dec
so that it is transparent. You can do this by printing the proof term that Coq generates and pasting it in your source file. I've added a gist here with a complete solution.
Needless to say, this approach lends itself to bloated, hard to read, and hard to maintain code. As ejgallego was pointing out in his answer, your best bet in this case is probably to define a Boolean function that decides WF
, and use that instead of WFDec
. The only problem with his approach, as he said, is that you will need to write your own induction principle to Exp
in order to prove that the Boolean version indeed decides the inductive definition. Adam Chlipala's CPDT has a chapter on inductive types that gives an example of such an induction principle; just look for "nested inductive types".
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With