Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)

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.

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.