The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

Hi,Daniel
   I'm very appreciate your reply. your solution is very helpful. but i am not familiar with Program Fixpoint. when i copy your codes to Coq, i got the error information. Any suggestion? Thanks a lot!

===========
Section bringToFrontOfList.
 Variable A:Type.
 Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.

 Lemma In_to_front: forall {A} (a:A) (l:list A),
  In a l -> exists l':list A, Permutation l (a::l').
 Proof.
   Admitted. (*needs to prove*)

Program Fixpoint bring_to_front  (a:A) (l:list A) :
  In a l -> { l':list A | Permutation l (a::l') } :=
match l with
| b :: l' => if (Aeq_dec a b) then l' else
                b :: bring_to_front a l' _
| nil => nil
end.
End bringToFrontOfList.
=================
Error:
In environment
A : Type
Aeq_dec : forall x y : A, {x = y} + {x <> y}
bring_to_front : Tactics.fix_proto
                   (forall (a : A) (l : list A),
                    In a l -> {l' : list A | Permutation l (a :: l')})
a : A
l : list A
b : A
l' : list A
Heq_l : b :: l' = l
H : a = b
The term "l'" has type "list A" while it is expected to have type
 "In a (b :: l') -> {l' : list A | Permutation (b :: l') (a :: l')}".




------------------ ԭʼÓʼþ ------------------
>From: Daniel Schepler <dschepler AT gmail.com>
>Reply-To: 
>To: ldou AT cs.ecnu.edu.cn
>Subject: Re: [Coq-Club] again, about ListSet , MSets or FSets
>Date: Wed, 16 Nov 2011 19:09:16 -0800
>
2011/11/15 <ldou AT cs.ecnu.edu.cn>

Hi,guys
   Sometimes we find the ListSet is hard to handle and is bringing some disadvantages in proof. We are suggested to use MSets or FSets. But few tutorials about that can be found . Could someone give us a detail example or  related documents?
   To be precise, we have the following premise :

exists e:string, set_In e sl.

in which sl : set string. In Coq, it is sl:list string actually. What we desire is that sl could be destructed as the form:

sl=e::sl'

so that we could simplify our function which is defined to match on sl.
But Coq could only destruct it as :¡¡a::sl'. Then we fall into the trap of discussing whether e=a or e is in sl', which
stucks our proofs.
We've tried to add an axiom to our development:

Axiom order_not_matter: forall sl:list string, exists e sl', set_In e sl -> l=e::sl'.

We know this is wrong, is there any better way around this ?  Thanks.

How about proving:

Require Import Permutation.

Lemma In_to_front: forall {A} (a:A) (l:list A),
  In a l -> exists l':list A, Permutation l (a::l').

And if A has decidable equality, as string does, then it should even be fairly easy to construct

Program Fixpoint bring_to_front {A} (a:A) (l:list A) :
  In a l -> { l':list A | Permutation l (a::l') } :=
match l with
| b :: l' => if (eq_dec a b) then l' else
                b :: bring_to_front a l' _
| nil => !
end.
--
Daniel Schepler