The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

The reason, I am trying to write proof in functional style, is to achieve the precisely the same effect which I am getting from functional induction scheme (three cases explicitly).

      Require Import FunInd.

      Fixpoint intersperse (A : Type) (c : A) (l : list A) : list A :=
        match l with
        | [] => []
        | [h] => [h]
        | h :: t => h :: c :: intersperse _ c t
        end.
    
     
      Functional Scheme intersperse_ind := Induction for intersperse Sort Prop.
     
      Compute (intersperse _ 0 []).
      Compute (intersperse _ 0 [1]).
      Compute (intersperse _ 0 [1; 2; 3]).
     
      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 l.
        functional induction (intersperse A c l).
        + cbn. exact eq_refl.
        + cbn. exact eq_refl.
        + cbn in *. repeat f_equal. assumption.
      Qed.

Best regards,

Mukesh Tiwari

On Fri, Nov 30, 2018 at 3:24 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> 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