Skip to content

Instantly share code, notes, and snippets.

@lunalunaa

lunalunaa/coq_filter.v

Forked from y-taka-23/coq_filter.v
Created March 25, 2018 12:25
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save lunalunaa/1dfbc5cfbdbc04e0c9075c0d4769f135 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save lunalunaa/1dfbc5cfbdbc04e0c9075c0d4769f135 to your computer and use it in GitHub Desktop.
Download ZIP
Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)
Raw
coq_filter.v
(******************************************************)
(** //// Validation of the "filter" Function //// *)
(******************************************************)
Require Import List Bool Lt.
Section Filter.
(*////////////////////////////////////////////////////*)
(** Validation of the Function *)
(*////////////////////////////////////////////////////*)
(* Assumption : test is a test function on the type X. *)
Variable X : Set.
Variable test : X -> bool.
(* Predicate : all P l <=> P holds for all elements in l. *)
Inductive all (P : X -> Prop) : list X -> Prop :=
| All_nil : all P nil
| All_cons : forall (x : X) (l' : list X),
P x -> all P l' -> all P (x :: l').
(* Predicate : merger l l1 l2 <=> l1 and l2 are merged into l. *)
Inductive merger : list X -> list X -> list X -> Prop :=
| Merger_nil_l : forall l : list X,
merger l nil l
| Merger_nil_r : forall l : list X,
merger l l nil
| Merger_cons_l : forall (x : X) (l l1 l2 : list X),
merger l l1 l2 ->
merger (x :: l) (x :: l1) l2
| Merger_cons_r : forall (x : X) (l l1 l2 : list X),
merger l l1 l2 ->
merger (x :: l) l1 (x :: l2).
(* Validity of filter (1) *)
Theorem filter_challenge : forall l l1 l2 : list X,
let T := fun x => test x = true in
let F := fun x => test x = false in
merger l l1 l2 -> all T l1 -> all F l2 ->
filter test l = l1.
Proof.
intros l l1 l2 T F H_m H_l1 H_l2.
induction H_m as [l | l |
x l' l1' l2 _ H_m' | x l' l1 l2' _ H_m'].
(* Case : l1 = nil, l2 = l *)
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
reflexivity.
(* Case : l = x :: l' *)
unfold filter.
fold (filter test).
inversion H_l2 as [| tmp1 tmp2 H_h H_t (tmp3, tmp4)].
clear tmp1 tmp2 tmp3 tmp4.
rewrite H_h.
apply H_l'.
apply H_t.
(* Case : l1 = l, l2 = nil *)
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
reflexivity.
(* Case : l = x :: l' *)
unfold filter.
fold (filter test).
inversion H_l1 as [| tmp1 tmp2 H_h H_t (tmp3, tmp4)].
clear tmp1 tmp2 tmp3 tmp4.
rewrite H_h.
rewrite (H_l' H_t).
reflexivity.
(* Case : l = x :: l', l1 = x :: l1' *)
unfold filter.
fold (filter test).
inversion H_l1 as [| tmp1 tmp2 H_h H_t (tmp3, tmp4)].
clear tmp1 tmp2 tmp3 tmp4.
rewrite H_h.
rewrite (H_m' H_t H_l2).
reflexivity.
(* Case : l= x :: l', l2 = x :: l2' *)
unfold filter.
fold (filter test).
inversion H_l2 as [| tmp1 tmp2 H_h H_t (tmp3, tmp4)].
clear tmp1 tmp2 tmp3 tmp4.
rewrite H_h.
rewrite (H_m' H_l1 H_t).
reflexivity.
Qed.
(* Predicate : sublist l1 l2 <=> l1 is a sublist of l2. *)
Inductive sublist : list X -> list X -> Prop :=
| Sublist_nil : forall l : list X,
sublist nil l
| Sublist_cons1 : forall (x : X) (l1 l2 : list X),
sublist l1 l2 ->
sublist l1 (x :: l2)
| Sublist_cons2 : forall (x : X) (l1 l2 : list X),
sublist l1 l2 ->
sublist (x :: l1) (x :: l2).
(* test x is true for all elements x of (filter test l). *)
Lemma filter_true : forall l : list X,
let T := fun x => test x = true in
all T (filter test l).
Proof.
intros l T.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply All_nil.
(* Case : l = x :: l' *)
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply All_cons.
(* Proof : T x *)
apply H_x.
(* Proof : all T (filter test l') *)
apply H_l'.
(* Case : test x = false *)
intro H_x.
apply H_l'.
Qed.
(* (filter test l) is a sublist of l. *)
Lemma filter_sublist : forall l : list X,
sublist (filter test l) l.
Proof.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply Sublist_nil.
(* Case : l = x :: l' *)
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply Sublist_cons2.
apply H_l'.
(* Case : test x = false *)
intro H_x.
apply Sublist_cons1.
apply H_l'.
Qed.
(* Maximality of filter *)
Lemma filter_max : forall l l0 : list X,
let T := fun x => test x = true in
all T l0 -> sublist l0 l ->
sublist l0 (filter test l).
Proof.
intros l l0 T H_l0 H_sub.
induction H_sub as [l | x l0 l' H_l' H_ind |
x l0' l' H_l' H_ind].
(* Case : l0 = nil *)
apply Sublist_nil.
(* Case : l = x :: l' *)
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply Sublist_cons1.
apply (H_ind H_l0).
(* Case : test x = false *)
intro H_x.
apply (H_ind H_l0).
(* Case : l = x :: l', l0 = x :: l0' *)
inversion H_l0 as [ | tmp1 tmp2 tmp3 H_t (tmp4, tmp5)].
clear tmp1 tmp2 tmp3 tmp4 tmp5.
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply Sublist_cons2.
apply (H_ind H_t).
(* Case : test x = false *)
intro H_x.
inversion H_l0 as [| tmp1 tmp2 H_h tmp3 (tmp4, tmp5)].
clear tmp1 tmp2 tmp3 tmp4 tmp5.
unfold T in H_h.
rewrite H_h in H_x.
discriminate.
Qed.
(* Sublists are shorter than or equal to the superlists. *)
Lemma sublist_length : forall l1 l2 : list X,
sublist l1 l2 ->
(l1 = l2 \/ length l1 < length l2).
Proof.
intros l1 l2 H_sub.
induction H_sub as [l2 | x l1 l2' H_l2' H_ind |
x l1' l2 H_l1' H_ind].
(* Case : l1 = nil *)
induction l2 as [| y l2' H_l2'].
(* Case : l2 = nil *)
left.
reflexivity.
(* Case : l2 = y :: l2' *)
right.
simpl.
apply lt_0_Sn.
(* Case : l2 = x :: l2' *)
right.
destruct H_ind as [H | H].
(* Case : l1 = l2' *)
rewrite H.
simpl.
apply lt_n_Sn.
(* Case : length l1 < length l2' *)
simpl.
apply (lt_trans (length l1) (length l2')
(S (length l2')) H).
apply lt_n_Sn.
(* Case : l1 = x :: l1', l2 = x :: l2' *)
destruct H_ind as [H | H].
(* Case : l1' = l2' *)
left.
rewrite H.
reflexivity.
(* Case : length l1' < length l2 *)
right.
simpl.
apply lt_n_S.
apply H.
Qed.
(* Validity of filter (2) *)
Theorem filter_challenge_2 : forall l : list X,
let T := fun x => test x = true in
all T (filter test l) /\
sublist (filter test l) l /\
(forall l0 : list X,
all T l0 -> sublist l0 l ->
(l0 = filter test l \/
length l0 < length (filter test l))).
Proof.
intros l T.
repeat split.
(* test x = true for all elements of (filter test l). *)
apply filter_true.
(* (filter test l) is a sublist of l. *)
apply filter_sublist.
(* (filter test l) has strictly maximal length. *)
intros l0 H_all H_sub.
apply sublist_length.
unfold T in H_all.
apply (filter_max l l0 H_all H_sub).
Qed.
(*////////////////////////////////////////////////////*)
(** Validation of the Specification (1) *)
(*////////////////////////////////////////////////////*)
Section Spec1.
(* Assumption : f1 satisfies the condtion of filter_challenge. *)
Variable f1 : list X -> list X.
Hypothesis f1_challenge : forall l l1 l2 : list X,
let T := fun x => test x = true in
let F := fun x => test x = false in
merger l l1 l2 -> all T l1 -> all F l2 ->
f1 l = l1.
(* Definition : Filter for negatation of test *)
Fixpoint antifilter (f : X -> bool) (l : list X) : list X :=
match l with
| nil => nil
| x :: l' => if f x
then antifilter f l'
else x :: antifilter f l'
end.
(* test x is false for all elements of (antifilter test l). *)
Lemma antifilter_false : forall l : list X,
let F := fun x => test x = false in
all F (antifilter test l).
Proof.
intros l F.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply All_nil.
(* Case : l = x :: l' *)
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply H_l'.
(* Case : antitest x = false *)
intro H_x.
apply All_cons.
(* Proof : F x *)
apply H_x.
(* Proof : all F (antifilter test l') *)
apply H_l'.
Qed.
(* [filter | antifilter] is a partition. *)
Lemma filter_merger : forall l : list X,
merger l (filter test l) (antifilter test l).
Proof.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply (Merger_nil_l nil).
(* Case : l = x :: l' *)
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply Merger_cons_l.
apply H_l'.
(* Case : test x = false *)
intro H_x.
apply Merger_cons_r.
apply H_l'.
Qed.
(* Valisity of filter_challenge *)
Theorem spec1_valid : forall l : list X, f1 l = filter test l.
Proof.
induction l as [| x l' H_l'].
(* Case : l = nil *)
simpl.
apply (f1_challenge nil nil nil).
(* Proof : merger nil nil nil *)
apply Merger_nil_l.
(* Proof : all T nil *)
apply All_nil.
(* Proof : all F nil *)
apply All_nil.
(* Case : l = x :: l' *)
simpl.
case_eq (test x).
(* Case : test x = true *)
intro H_x.
apply (f1_challenge (x :: l') (x :: filter test l')
(antifilter test l')).
(* Proof : merger (x :: l') (x :: filter test l')
(antifilter test l') *)
apply Merger_cons_l.
apply filter_merger.
(* Proof : all T (x :: filter test l') *)
apply All_cons.
(* Proof : T x *)
apply H_x.
(* Proof : all T (filter test l') *)
apply filter_true.
(* Proof : all F (antifilter test l') *)
apply antifilter_false.
(* Case : test x = false *)
intro H_x.
apply (f1_challenge (x :: l') (filter test l')
(x :: antifilter test l')).
(* Proof : merger (x :: l') (filter test l')
(x :: antifilter test l') *)
apply Merger_cons_r.
apply filter_merger.
(* Proof : all T (filter test l') *)
apply filter_true.
(* Proof : arr F (x :: antifilter test l') *)
apply All_cons.
(* Proof : F x *)
apply H_x.
(* Proof : all F (antifilter test l') *)
apply antifilter_false.
Qed.
End Spec1.
(*////////////////////////////////////////////////////*)
(** Validation of the Specification (2) *)
(*////////////////////////////////////////////////////*)
Section Spec2.
(* Assumption : f2 satisfies the condtion of filter_challenge_2. *)
Variable f2 : list X -> list X.
Hypothesis f2_challenge : forall l : list X,
let T := fun x => test x = true in
all T (f2 l) /\ sublist (f2 l) l /\
(forall l0 : list X,
all T l0 -> sublist l0 l ->
(l0 = f2 l \/
length l0 < length (f2 l))).
(* Validity of filter_challenge_2 *)
Theorem spec2_valid : forall l : list X, f2 l = filter test l.
Proof.
intro l.
assert (filter test l = f2 l \/
length (filter test l) < length (f2 l)) as H_1.
(* Proof of the assertion *)
apply f2_challenge.
(* Proof : all T (filter test l) *)
apply filter_true.
(* Proof : sublist (filter test l) l *)
apply filter_sublist.
assert (f2 l = filter test l \/
length (f2 l) < length (filter test l)) as H_2.
(* Proof of the assertion *)
apply filter_challenge_2.
(* Proof : all T (f2 l) *)
apply f2_challenge.
(* Proof : sublist (f2 l) l *)
apply f2_challenge.
destruct H_1 as [H_1 | H_1].
(* Cawe : filter test l = f2 l *)
symmetry.
apply H_1.
(* Case : length (filter test l) < length (f2 l) *)
destruct H_2 as [H_2 | H_2].
(* Case : f2 l = filter test l *)
apply H_2.
(* Case : length (f2 l) < length (filter test l) *)
apply lt_asym in H_2.
contradiction.
Qed.
End Spec2.
End Filter.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment