mukesh tiwari

2018-11-30 04:24:23 UTC

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

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