I'm trying to work with a datatype that represents expressions in a sort of universal algebra context. The usual way to express this in (pen and paper) maths is that you have a set of function symbols, F, together with an arity function. An expression is a tree where each node is labelled with a function symbol and it has as many children as its arity. In this particular example, I've also got a set of atomic variables that get injected explicitly as terms.
It's pretty clear how to write this down with Coq (I've got a snippet of code at the bottom), but I'd like to prove some sort of decidability result. I've managed to prove decidability for vectors ("If I have decidability on A, then I can get decidability on VectorDef.t A n"), but I can't work out how to do the same for my tree type.
I tried doing an explicit recursion over the structure of a tree, but I ended up needing to call out to my "decidable vector" function, which doesn't get past the termination checker. This is reasonable, since the vector function expects to be given a discriminator for arbitrary elements of its underlying type and this obviously doesn't bottom out!
I can't work out how to tell Coq that (by induction) I have decidability for some terms, and these are the only terms that appear in the vectors in question. Is there a standard trick for doing this sort of thing?
Below, the data types in question:
Require Vectors.VectorDef.
Definition vec := VectorDef.t.
Section VTree.
(* If it helps, I have a definition for this function *)
Variable dec_vec : forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (n : nat) (v v' : vec A n), {v = v'} + {v <> v'}.
Variable V : Set.
Variable F : Set.
Variable a : F -> nat.
Inductive VTree : Type :=
| varTerm : V -> VTree
| funTerm (f : F) (ts : vec VTree (a f)) : VTree.
Section DecVTree.
Hypothesis decV : forall x y : V, {x = y} + {x <> y}.
Hypothesis decF : forall x y : F, {x = y} + {x <> y}.
Definition decVTree : forall x y : VTree, {x = y} + {x <> y}.
(* ??? *)
While Li-yao made some useful points, the dependent types aren't that bad! It turns out that the reason my previous script didn't work is that I'd used Qed rather than Defined to finish my decidability proof for vectors.
Here's a complete working proof:
Require Vectors.VectorDef.
Require Import Logic.Eqdep_dec.
Require Import PeanoNat.
Definition vec := VectorDef.t.
Section dec_vec.
Variable A : Type.
Hypothesis decA : forall x y : A, {x = y} + {x <> y}.
Definition dec_vec {n} (v v' : vec A n) : {v = v'} + {v <> v'}.
refine (VectorDef.rect2 (fun _ x y => {x = y} + {x <> y})
(left (eq_refl))
(fun n v v' veq a a' => _)
v v').
- destruct (decA a a') as [ eqaH | neaH ].
+ rewrite <- eqaH; clear eqaH a'.
destruct veq as [ eqvH | nevH ].
* rewrite <- eqvH. apply left. exact eq_refl.
* apply right. intro consH. inversion consH.
exact (nevH (inj_pair2_eq_dec nat Nat.eq_dec (vec A) n v v' H0)).
+ apply right.
intro consH. inversion consH. contradiction.
Defined.
End dec_vec.
Section VTree.
Variable V : Set.
Variable F : Set.
Variable a : F -> nat.
Inductive VTree : Type :=
| varTerm : V -> VTree
| funTerm (f : F) (ts : vec VTree (a f)) : VTree.
Section DecVTree.
Hypothesis decV : forall x y : V, {x = y} + {x <> y}.
Hypothesis decF : forall x y : F, {x = y} + {x <> y}.
Lemma varTerm_ne_funTerm v f ts : varTerm v <> funTerm f ts.
Proof.
intros eqH. inversion eqH.
Qed.
Fixpoint decVTree (x y : VTree) : {x = y} + {x <> y}.
refine (match x, y with
| varTerm v, varTerm v' => _
| varTerm v, funTerm f ts => _
| funTerm f ts, varTerm v => _
| funTerm f ts, funTerm f' ts' => _
end
).
- destruct (decV v v') as [ eqH | neH ].
+ exact (left (f_equal varTerm eqH)).
+ enough (H: varTerm v <> varTerm v');
try (exact (right H)).
injection; tauto.
- exact (right (varTerm_ne_funTerm v f ts)).
- exact (right (not_eq_sym (varTerm_ne_funTerm v f ts))).
- destruct (decF f f') as [ feqH | fneH ].
+ revert ts'. rewrite <- feqH. clear feqH; intro ts'.
destruct (dec_vec VTree decVTree ts ts') as [ tseqH | tsneH ].
* apply left. apply f_equal. exact tseqH.
* apply right. intro funH. inversion funH.
exact (tsneH (inj_pair2_eq_dec
F decF (fun f => vec VTree (a f)) f ts ts' H0)).
+ enough (H: funTerm f ts <> funTerm f' ts');
try (exact (right H)).
injection; tauto.
Qed.
End DecVTree.
End VTree.