The Coq mailing list

[herman geuvers <H.Geuvers AT cs.ru.nl>]

Dear all,

I noticed that Coq's unification sometimes introduces too many 
abstractions, causing the apply tactic to take the "wrong branch", 
leading to proof failure.

Here is an example, part of my exercise file for students where they 
prove an instance of the Knaster-Tarski fixed-point theorem.

Did anyone else ever come accross this?
Is this a failure of Coq's unification?

Best Regards

Herman Geuvers

--------------------------------------------------------------------------
Variable A:Set.

Definition subs := fun S T :A->Prop => forall x :A, S x -> T x.
Infix "<<" := subs (no associativity, at level 75).

Variable F : (A->Prop) -> (A->Prop).

Definition closed := fun P:A->Prop => F P << P.

(* Higher order definition of the "smallest closed subset of A", sm_clos *)
Definition sm_clos(x:A) := forall P:A->Prop, F P << P -> P x.

(* We want to prove that sm_clos is a subset of every closed subset P *)

Lemma prop1 : forall P:A->Prop, closed P -> sm_clos << P.
intros P hc.
intros x hsc.
unfold sm_clos in hsc.

(* Now the following is natural, but doesn't work *)
apply hsc.
intros z H.
apply hc.
 (* exact H ?? No way! Coq is intensional, so
     F (fun x0 : A => P x0)
can't be equated to
     F P *)

(* The only way to complete the proof is as follows:
apply (hsc P).
apply hc.
Qed. *)