Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)
(******************************************************)
(** //// 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.
@prashantpawar

This comment has been minimized.

Copy link

@prashantpawar prashantpawar commented May 21, 2018

I don't think you need 4 branches for the merger inductive type.

Wouldn't this do the job too?

Inductive merger {X:Type} : list X -> list X -> list X -> Prop :=
  | Merger_nil : merger [] [] []
  | Merger_l1 : forall (n : X) (l1 l2 l : list X),
      merger l1 l2 l -> merger (n :: l1) l2 (n :: l)
  | Merger_l2 : forall (n : X) (l1 l2 l : list X),
      merger l1 l2 l -> merger l1 (n :: l2) (n :: l).

Sorry just found your gist while searching for some hints on this exercise.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment