I am currently solving Software Foundations and am in the IndProp chapter doing the excercise "filter_challenge". I have run into the following Problem in the merge_filter Theorem. Coq errors when I try to unfold the All fixpoint and says that it is opaque. I do not know why it is opaque. I have tried to use cbv to compute the Fixpoint once but it did not work (and I am unsure on how to use it or if it even is the right tool for the job).
Here is my definition of merge:
Inductive merge {X:Type} : list X -> list X -> list X -> Prop :=
(* FILL IN HERE *)
| merge_nil : merge [] [] []
| merge_head l1 l2 l (x: X) (H: merge l1 l2 l) : merge (x::l1) l2 (x::l)
| merge_comm l1 l2 l (H: merge l1 l2 l) : merge l2 l1 l
.
My definition of All from Logic.v earlier in the book:
Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop
:= match l with
| [] => True
| x::l' => P x /\ All P l'
end.
The Theorem in question:
Theorem merge_filter : forall (X : Set) (test: X->bool) (l l1 l2 : list X),
merge l1 l2 l ->
All (fun n => test n = true) l1 ->
All (fun n => test n = false) l2 ->
filter test l = l1.
Proof.
intros.
induction H.
- reflexivity.
- simpl. unfold All in H0.
Admitted.
I want to unfold H0 to get a hypothesis regarding the head of the list.
This was a problem with the build process. Rebuilding the project fixed it.