The Coq mailing list

[Alan Pogrebinschi <alanpog AT gmail.com>]

Victor,
The following declarative proof works for you Lemma:
proof. thus thesis using apply corr_propcc.end proof. Qed.
There seemed to be 2 problems with your original proof (I've just
started learning Coq, so my explanation below may not be totally
accurate):
- you used "have" instead of "thus" or "hence". "have" is only for
intermediate steps, according to the refman section 11.3.7 .- you used
specialize and no apply. Note that in your imperative proof you had to
use "eauto" after specialize to complete the proof,
 and there was no equivalent step in the declarative version.
Regards,
Alan
On Tue, Nov 15, 2011 at 7:01 PM, Victor Porton 
<porton AT narod.ru>
 wrote:
> [[[[
> Variable s: Set.
> Variable mygraph: Set.
>
> Variable sub: Set->Set->Prop.
> Variable product: Set->Set->Set.
> Variable is_graph: Set->Prop.
> Variable domain: Set->Set.
> Variable range: Set->Set.
>
> Axiom corr_propcc: forall s t g,
>  sub g (product s t) = (is_graph g /\ sub (domain g) s /\ sub (range g) t).
>
> Lemma TwoInside: sub mygraph (product s s) = (is_graph mygraph /\ sub 
> (domain mygraph) s /\ sub (range mygraph) s).
> (*
> Proof.
>  specialize corr_propcc.
>  eauto.
> Qed.
> *)
> proof.
>  have thesis using specialize corr_propcc.
> end proof. Qed.
> ]]]]
>
> It does not work. When I uncomment the Proof...Qed and comment declarative 
> proof, it works.
>
> It does not work with declarative proofs. Please help me to rewrite it in 
> declarative proof style.
>
> --
> Victor Porton - http://portonvictor.org
>