The Coq mailing list

[Jasper Stein <J.Stein AT cs.ru.nl>]

Op dinsdag 20 september 2005 08:50, schreef u:
> Hello all.
>
> I am trying to play with CoQ a bit. I've written the following theorem
> about convexity but have no idea how to prove it. Either I don't
> understand something or it's really non-trivial thing. Please help.
>
> Thanks a lot.

Hello Nickolay...!

You failed to say which contribution you're using - the file 
Linear_Algebra_by_Friedberg_Insel_Spence.v is not in the standard Coq 
library. That's why it's been so silent until now. Fortunately I recognised 
the LinAlg package, which I authored :-) Glad to see someone actually using 
my work!

To the solution.
I assume you got stuck on proving something like
   exists s3 : min_set X, (some proposition)
which requires exhibiting an element of a particular subset of V; that is, 
you'd have to pick some v in V which is also, informally, an element of 
(min_set X). So, in your context, you must provide v and a proof of that fact 
(ie. of Pred_fun (min_set X) v), and pack them, on-the-fly. 

This is relatively hard to do by hand, since - in my opinion - writing proofs 
non-interactively, just by giving the proof term, is awkward and not very 
intuitive, and the proof terms are fairly large at times - but working with 
subsets in the setoid formalism unavoidably results in this kind of proof 
requirements.

The easiest thing you can do is first to provide a (local) function that 
produces terms of the desired subset:
===
Let to_minset (X:part_set V) : X->(min_set X).
intros X x.
simpl.
assert (in_part (min (subtype_elt x)) (min_set X)).
red.
simpl.
exists x.
apply Refl.
red in H.
apply (Build_subtype H).
Defined.
===
This takes an x:X and outputs (min x), represented as an element of (min_set 
X). With it you can finish your proof more easily:
===
Lemma min_is_convex :
    forall X : part_set V, is_convex X -> is_convex (min_set X).
intros.
red in H.
red.
intros.
destruct s1 as [ms1 [s1 Hs1]].
destruct s2 as [ms2 [s2 Hs2]].
simpl.
destruct (H s1 s2) as [ms3 Hms3].
exists (to_minset X ms3).
simpl.
apply Trans with ((min (subtype_elt s1))+' min (subtype_elt s2));auto with 
algebra.
apply Trans with (min ((subtype_elt ms3)+'(subtype_elt ms3)));info auto with 
algebra.
apply Trans with (min ((subtype_elt s1)+'(subtype_elt s2)));auto with algebra.
apply Trans with ((min (subtype_elt s2))+' min (subtype_elt s1));auto with 
algebra.
Qed.
===

Hope this helps. If you still have any questions - feel free to email me (via 
Coq-club or privately).


Jasper
-- 
The problem with having an open mind is that people toss in garbage