An Implementation of the uniq Command Certified by Coq

coq_uniq.v

Parameter A : Type.
Parameter beq_A : A -> A -> bool.

Section Uniq.

Require Import Arith List.

Hypothesis beq_A_true : forall x y : A,
                        beq_A x y = true -> x = y.
Hypothesis beq_A_false : forall x y : A,
                         beq_A x y = false -> x <> y.

Fixpoint uniq (l : list A) : list A :=
    match l with
    | nil => nil
    | x :: nil => x :: nil
    | x :: ((y :: _) as xs) => if (beq_A x y)
                                   then uniq xs
                                   else x :: uniq xs
    end.
Functional Scheme uniq_ind := Induction for uniq Sort Prop.

Inductive no_stutter : list A -> Prop :=
    | NoStut_nil    : no_stutter nil
    | NoStut_single : forall x : A,
                      no_stutter (x :: nil)
    | NoStut_cons   : forall (x y : A) (ys : list A),
                      x <> y -> no_stutter (y :: ys) ->
                      no_stutter (x :: y :: ys).

Lemma no_stutter_cons : forall (x : A) (xs : list A),
                        no_stutter (x :: xs) -> no_stutter xs.
Proof.
    intros x xs H.
    inversion H as [| | t1 y ys t2 H_xs t4 ]; subst; clear H.
    
        (* Case : xs = nil *)
        apply NoStut_nil.
    
        (* Case : xs = y :: ys *)
        apply H_xs.
Qed.

Lemma uniq_head : forall l : list A,
                  hd_error (uniq l) = hd_error l.
Proof.
    intro l.
    functional induction (uniq l)
        as [| _ x _ _ _ | _ x xs _ y ys H_xs H_eq H |
              _ x xs _ y ys H_xs H_eq H].
    
        (* Case : l = nil *)
        reflexivity.
    
        (* Case : l = x :: nil *)
        reflexivity.
    
        (* Case : l = x :: y :: ys, x = y *)
        rewrite H.
        simpl.
        apply beq_A_true in H_eq.
        subst.
        reflexivity.
    
        (* Case : l = x :: y :: ys, x <> y *)
        simpl.
        reflexivity.
Qed.

Lemma uniq_no_stutter : forall l : list A,
                        no_stutter (uniq l).
Proof.
    intro l.
    functional induction (uniq l)
        as [| _ x _ _ _ | _ _ xs _ _ _ _ _ H |
              _ x xs _ y ys H_xs H_eq H].
    
        (* Case : l = nil *)
        apply NoStut_nil.
    
        (* Case : l = x :: nil *)
        apply NoStut_single.
    
        (* Case : l = x :: y :: ys, x = y *)
        apply H.
    
        (* Case : l = x :: y :: ys, x <> y *)
        remember (uniq (y :: ys)) as xs.
        destruct xs as [| z zs].
        
            (* Case : xs = nil *)
            apply NoStut_single.
        
            (* Case : xs = z :: zs *)
            apply NoStut_cons.
            
                (* Proof : x <> z *)
                assert (hd_error (z :: zs) =
                        hd_error (uniq (y :: ys))) as H_z.
                
                    (* Proof of the assertion *)
                    apply f_equal.
                    assumption.
                
                rewrite uniq_head in H_z.
                simpl in H_z.
                inversion H_z; subst.
                apply beq_A_false in H_eq.
                apply H_eq.
            
                (* Proof : no_stutter (z :: zs) *)
                apply H.
Qed.

Inductive subseq : list A -> list A -> Prop := 
    | SubSeq_nil   : forall l : list A,
                     subseq nil l
    | SubSeq_cons1 : forall (x : A) (l1 l2 : list A),
                     subseq l1 l2 ->
                     subseq l1 (x :: l2)
    | SubSeq_cons2 : forall (x : A) (l1 l2 : list A),
                     subseq l1 l2 ->
                     subseq (x :: l1) (x :: l2).

Lemma uniq_subseq : forall l : list A,
                    subseq (uniq l) l.
Proof.
    intro l.
    functional induction (uniq l)
        as [| _ x _ _ _ | _ x xs _ y ys H_xs _ H | 
              _ x xs _ y ys H_xs _ H].
    
        (* Case : l = nil *)
        apply SubSeq_nil.
    
        (* Case : l = x :: nil *)
        apply SubSeq_cons2.
        apply SubSeq_nil.
    
        (* Case : l = x :: y :: nil, x = y *)
        apply SubSeq_cons1.
        apply H.
    
        (* Case : l = x :: y :: nil, x <> y *)
        apply SubSeq_cons2.
        apply H.
Qed.

Lemma subseq_length : forall l1 l2 : list A,
                      subseq l1 l2 ->
                      l1 = l2 \/ length l1 < length l2.
Proof.
    intros l1 l2 H.
    induction H as [l2 | x l1 ys H_ss H | x xs ys H_ss H].
    
        (* Case : l1 = nil *)
        destruct l2 as [| y ys].
        
            (* Case : l2 = nil *)
            left.
            reflexivity.
        
            (* Case : l2 = y :: ys *)
            right.
            simpl.
            apply lt_0_Sn.
    
        (* Case : l2 = x :: ys, subseq l1 ys *)
        right.
        destruct H as [H | H].
        
            (* Case : l1 = ys *)
            subst.
            simpl.
            apply lt_n_Sn.
        
            (* Case : length l1 < length ys *)
            simpl.
            apply lt_trans with (length ys).
            
                (* Proof : length l1 < length ys *)
                apply H.
            
                (* Proof : length ys < S (length ys) *)
                apply lt_n_Sn.
    
        (* Case : l1 = x :: xs, l2 = x :: ys, subseq xs ys *)
        destruct H as [H | H].
        
            (* Case : xs = ys *)
            left.
            subst.
            reflexivity.
        
            (* Case : length xs < length ys *)
            right.
            simpl.
            apply lt_n_S.
            apply H.
Qed.

Lemma uniq_max : forall l l0 : list A,
                 no_stutter l0 -> subseq l0 l ->
                 subseq l0 (uniq l).
Proof.
    intros l.
    functional induction (uniq l)
        as [| _ x _ _ _ | _ x xs _ y ys H_xs H_eq H |
              _ x xs _ y ys H_xs _ H ].
    
        (* Case : l = nil *)
        intros l0 H_ns H_ss.
        inversion H_ss; subst.
        apply SubSeq_nil.
    
        (* Case : l = x :: nil *)
        intros l0 H_ns H_ss.
        apply H_ss.
    
        (* Case : l = x :: y :: ys, x = y *)
        intros l0 H_ns H_ss.
        apply beq_A_true in H_eq.
        subst.
        apply (H _ H_ns).
        inversion H_ss as [| t1 t2 t3 H_ind t4 t5 |
                             t1 l1 t2 H_ind t3 t4 ];
        subst; clear H_ss.
        
            (* Case : l0 = nil *)
            apply SubSeq_nil.
        
            (* Case : subseq l0 (y :: ys) *)
            apply H_ind.
        
            (* Case : l0 = x :: l1, subseq l1 (y :: ys) *)
            apply SubSeq_cons2.
            inversion H_ind as [| t1 t2 t3 H_ind' t4 t5 |
                                  t1 l2 t2 H_ind' t3 t4 ];
            subst; clear H_ind.
            
                (* Case : l1 = nil *)
                apply SubSeq_nil.
            
                (* Case : l1 = subseq ys *)
                apply H_ind'.
            
                (* Case : l1 = y :: l2, subseq l2 ys *)
                inversion H_ns as [| | t1 t2 t3 H_F H_ns' t4];
                subst.
                contradict H_F.
                reflexivity.
    
        (* Case : l = x :: y :: ys, x <> y *)
        intros l0 H_ns H_ss.
        inversion H_ss as [| t1 t2 t3 H_ind t4 t5 |
                             t1 l1 t2 H_ind t3 t4 ];
        subst; clear H_ss.
        
            (* Case : l0 = nil *)
            apply SubSeq_nil.
        
            (* Case : subseq l0 (y :: ys) *)
            apply SubSeq_cons1.
            apply (H _ H_ns).
            apply H_ind.
        
            (* Case : l0 = x :: l1, subseq l1 (y :: ys) *)
            apply SubSeq_cons2.
            apply H.
            
                (* Proof : no_stutter l1 *)
                apply (no_stutter_cons _ _ H_ns).
            
                (* Proof : subseq l1 (y :: ys) *)
                apply H_ind.
Qed.

Theorem uniq_valid : forall l : list A,
                     no_stutter (uniq l) /\ subseq (uniq l) l /\
                     (forall l0 : list A,
                      no_stutter l0 /\ subseq l0 l ->
                      l0 = uniq l \/ length l0 < length (uniq l)).
Proof.
    intro l.
    repeat split.
    
        (* Proof : no_stutter (uniq l) *)
        apply uniq_no_stutter.
    
        (* Proof : subseq (uniq l) l *)
        apply uniq_subseq.
    
        (* Proof : Maximality *)
        intros l0 H.
        destruct H as [H1 H2].
        apply subseq_length.
        apply (uniq_max _ _ H1 H2).
Qed.

End Uniq.


Extraction Language Haskell.

Extract Inductive bool =>
    "Prelude.Bool" ["Prelude.True" "Prelude.False"].
Extract Inductive list => "[]" ["[]" "(:)"].

Extract Constant A => "Prelude.String".
Extract Constant beq_A => "(Prelude.==)".

Extraction "CertiUniq.hs" uniq.