The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

I don't understand the relation between these languages.
I give an example : (* let D the set of x in A such that x is not in f x*)
define  D  as (fun x:U => In U A x /\ ~(In U (f x) x)).
(* D is in (Power_set U A) *)
claim SousEns : (In (Ensemble U) (Power_set U A) D).
unfold In ;constructor.
thus thesis.
end claim.
And then the claim is proved.

But with : (* D is in (Power_set U A) *)
claim SousEns : (In (Ensemble U) (Power_set U A) D).
thus thesis using (unfold In;constructor) .
end claim.
And then claim is NOT proved.

The first proof mixes mathematical proof language and tactic language.
The second failed proof is only in the mathematical proof language.

-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy