The Coq mailing list

[lisa <ldou AT cs.ecnu.edu.cn>]

Pierre-Marie Pédrot <pierre-marie.pedrot <at> inria.fr> writes:

> 
> On 26/01/2012 09:28, ldou <at> cs.ecnu.edu.cn wrote:
> > (*4.the properties of "simulation" .
> > we get stuck in this lemma. We think it is true:
> > when "simulation st a b" exists and the function of "sel" in c
> > is used to construct the interleave of two traces(a and z) , the
> > function of "sel"
> > in c' should construct the interleave of b and z in the same way as the
> > previous one.
> > We have no idea about how to construct such c' in Coq,
> > any suggestions are appreciated.
> > *)
> 
> What your proof scheme suggests me is that you're actually using some
> form of classical reasoning, because you cannot give the choice
> operation c' a priori without knowledge of « simulation st a b ».
> 
> Looks a lot like independence of general premises, which is is slightly
> classical. See the ClassicalFacts module for more information.
> 
> PMP
> 
> 

Do you mean that we could use "choice_axiom" to handle the "exists" so that 
the  
proof can go on? If we take (trace->trace) for A and trace for B, how can we 
construct R?
Axiom choice_axiom:forall (A B : Type) (R : A->B->Prop),
   (forall x : A, exists y : B, R x y) ->
    exists f : A->B, (forall x : A, R x (f x)).
Thank you very much!