[Coq-Club] Proof in functional style

[mukesh tiwari]

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

[mukesh tiwari]

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

Post by mukesh tiwari
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.
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

[Larry Lee]

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))))).

Post by mukesh tiwari
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
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

[Pierre Courtieu]

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

Post by Larry Lee
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)))
(*
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])
(*
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))))).
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