The Coq mailing list

[Larry Lee <llee454 AT gmail.com>]

Hi mukesh,

I hope this helps you identify the problem in your proof.

- Larry

Require Import List.

Import ListNotations.

Open Scope list_scope.

Fixpoint intersperse (A : Type) (c : A) (l : list A) : list A :=

      match l with

      | [] => []

      | [h] => [h]

      | h :: t => h :: c :: intersperse _ c t

      end.

Lemma map_intersperse_not_working :  forall (A B : Type) (f : A -> B) (c : A) (l : list A),

          map f (intersperse _ c l) = intersperse _ (f c) (map f l).

Proof.

  exact (

    fun (A B : Type) (f : A -> B) (c : A)

      => list_ind

           (fun l => map f (intersperse _ c l) = intersperse _ (f c) (map f l))

           (eq_refl [])

           (fun x0

             => list_ind

                  (fun xs => map f (intersperse _ c xs) = intersperse _ (f c) (map f xs) -> map f (intersperse _ c (x0 :: xs)) = intersperse _ (f c) (map f (x0 :: xs)))

                  (*

                     goal:

                     map f (intersperse _ c (x0 :: [])) = intersperse _ (f c) (map f (x0 :: []))

                     map f [x0] = intersperse _ (f c) [f x0]

                     [f x0] = [f x0]

                  *)

                  (fun _ => eq_refl [f x0])

                  (* 

                     goal:

                     map f (intersperse _ c (x0 :: y0 :: ys)) = intersperse _ (f c) (map f (x0 :: y0 :: ys))

                     map f (x0 :: c :: intersperse _ c (y0 :: ys)) = intersperse _ (f c) (f x0 :: f y0 :: (map f ys))

                     (f x0 :: f c :: map f (intersperse _ c (y0 :: ys)) = (f x0 :: f c :: intersperse _ (f c) (f y0 :: map f xs))

                  *)

                  (fun y0 ys _ (H : map f (intersperse _ c (y0 :: ys)) = intersperse _ (f c) (map f (y0 :: ys)))

                    => ((eq_ind

                         (map f (intersperse _ c (y0 :: ys)))

                         (fun zs => (f x0 :: f c :: map f (intersperse _ c (y0 :: ys))) = (f x0 :: f c :: zs))

                         (eq_refl (f x0 :: f c :: map f (intersperse _ c (y0 :: ys))))

                         (intersperse _ (f c) (map f (y0 :: ys)))

                         H))))).

On Fri, 2018-11-30 at 15:24 +1100, mukesh tiwari wrote:

Hi Everyone, I have written a function (basically Haskell intersperse function)

  Fixpoint intersperse (A : Type) (c : A) (l : list A) : list A :=
        match l with
        | [] => []
        | [h] => [h]
        | h :: t => h :: c :: intersperse _ c t
        end.

     
      Compute (intersperse _ 0 []).
      Compute (intersperse _ 0 [1]).
      Compute (intersperse _ 0 [1; 2; 3]).

and proof about it's correctness      

      Lemma map_intersperse : forall (A B : Type) (f : A -> B) (c : A) (l : list A),
          map f (intersperse _ c l) = intersperse _ (f c) (map f l).
      Proof.
        intros A B f c.
        induction l.
        + cbn; auto.
        + destruct l.
          ++ cbn; auto.
          ++ cbn in *. repeat f_equal.
               (* At this point, the induction hypothesis is [1], and assumption is able to discharge
                   the proof *)
                assumption.
      Qed.

Now I rewrote the same proof in function style using refine tactic.

Lemma map_intersperse_not_working :  forall (A B : Type) (f : A -> B) (c : A) (l : list A),
          map f (intersperse _ c l) = intersperse _ (f c) (map f l).
        refine (fun A B f c =>
                  fix F l :=
                  match  l as l'
                         return  l = l' ->
                                 map f (intersperse A c l') =
                                 intersperse B (f c) (map f l') with
                                     
                  | [] => fun H => eq_refl
                  | [h] => fun H => eq_refl
                  | h1 :: h2 :: t => fun H => _      
                  end eq_refl).
        pose proof (F (h2 :: t)).
        cbn in *. repeat f_equal. Guarded.
        (* At this point assumption H0 is same as goal [2] so apply H0 should discharge the goal*)

        apply H0. Guarded. 

       (* I am getting Recursive definition of F is ill-formed. *)

Could some one point me why it's saying F is ill-formed ? I am calling it smaller argument (At least that is my understanding). 

I got working solution with help of Li-yao [3], but I am wondering why destruct t is making a difference in this solution which I am doing explicitly in previous one (matching on one element list [h])

  Lemma map_intersperse_not_working :  forall (A B : Type) (f : A -> B) (c : A) (l : list A),
          map f (intersperse _ c l) = intersperse _ (f c) (map f l).
        refine (fun A B f c =>
                  fix F l :=
                  match  l as l'
                         return  l = l' ->
                                 map f (intersperse A c l') =
                                 intersperse B (f c) (map f l') with
                                      
                  | [] => fun H => eq_refl
                  | h :: t => fun H => _     
                  end eq_refl).
        pose proof (F t).
        destruct t.
        + cbn. exact eq_refl.
        + cbn in *. repeat f_equal. apply H0. Guarded.
      Qed.

Best regards,

Mukesh Tiwari

[1] https://gist.github.com/mukeshtiwari/3effe799a8c76a9aaf1c9de27d4a89f0#file-function-v-L6
[2] https://gist.github.com/mukeshtiwari/3effe799a8c76a9aaf1c9de27d4a89f0#file-function-v-L36

[3] https://gist.github.com/Lysxia/13109240eff4082a9c17634c6e2f6c5f