The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
I think this is due to the fact that you did not propagate the
"eq_refl trick" in the sub-patterns. You can see it when replace (F
(h2::t)) by (F l0) (l0 is syntactically a subterm of t).

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 l0).
(* This is certainly well-formed BUT you can't prove the l0 = h2::t,
because the eq_refl trick was not don for this intermediate. *)

Once you do the eq_refl trick at each level it works:

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
            | h1 :: h2l =>
              fun H => match h2l as l''
                             return  h2l = l'' ->
                                     map f (intersperse A c (h1::l'')) =
                                     intersperse B (f c) (map f (h1::l'')) 
with
                       | [] => fun H => eq_refl
                       | h2 :: t => fun H => _
                       end eq_refl
            end eq_refl).
  pose proof (F h2l).
  cbn.
  cbn in *. repeat f_equal. Guarded.

  (* At this point assumption H0 is same as goal [2] so apply H0
     should discharge the goal*)
  subst h2l.
  apply H1. Guarded.

Hope this helps,
Pierre
Le ven. 30 nov. 2018 à 06:14, Larry Lee 
<llee454 AT gmail.com>
 a écrit :
>
> 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