Skip to content

Instantly share code, notes, and snippets.

@y-taka-23
Created September 12, 2015 06:31
Show Gist options
  • Save y-taka-23/2799b9bf06fb9971b8c9 to your computer and use it in GitHub Desktop.
Save y-taka-23/2799b9bf06fb9971b8c9 to your computer and use it in GitHub Desktop.
An Implementation of the uniq Command Certified by Coq
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment