The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday, November 18, 2011 11:23:56 PM 
ldou AT cs.ecnu.edu.cn
 wrote:
> 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')}".

Sorry, I guess I forgot to consume the "In a l" argument.  This version 
compiles for me:

Require Export List.
Require Export Permutation.
Require Import Program.

Section bringToFrontOfList.

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

Lemma In_to_front: forall (a:A) (l:list A),
  In a l -> exists l':list A, Permutation l (a::l').
Proof.
intros.
induction l; simpl in H.
  contradiction.

  destruct H as [[]|].
    exists l; apply Permutation_refl.

    destruct (IHl H) as [l'].
    exists (a0 :: l').
    apply Permutation_trans with (a0 :: a :: l');
      constructor; trivial.
Qed.

Program Fixpoint bring_to_front (a:A) (l:list A) :
  In a l -> { l':list A | Permutation l (a::l') } :=
fun _ =>
match l with
| b :: l' => if (A_eq_dec a b) then l' else
             b :: bring_to_front a l' _
| [] => !
end.
Next Obligation. Proof.
destruct H; congruence || assumption.
Qed.
Next Obligation. Proof.
apply Permutation_trans with (b :: a :: x);
  constructor; trivial.
Defined.

End bringToFrontOfList.

(*
Require Import ExtrOcamlBasic.
Extraction bring_to_front.
*)
-- 
Daniel Schepler