[Coq-Club] Compute a general recursive function on dependent types.

[Shengyi Wang]

Dear Coq users,

Recently I defined a map of "sig" type from positive to positive. The map
should satisfy a property: it always maps a value v to a value which is not
greater than v. Formally the definition is:

Definition pos_map_prop (t: PM.tree positive) : Prop :=
forall i j, PM.find i t = Some j -> j <= i.

Definition PosMap := {pm : PM.tree positive | pos_map_prop pm}.

Such a map can be viewed as a forest: each key in the map is a node. Each
node points to a smaller value or itself.

Then I successfully defined a general recursive function "pm_trace_root"
which traces back such a node along the pointers until to a self-pointing
"root". The property of the map ensures the termination.

So far everything seems fine until I try to run the function in Coq. I
defined a test_map which is essentially {1 -> 1, 2 -> 2}. I tested:

Compute (PM.find 2 (proj1_sig test_map)).
===> Some 1

Compute (PM.find 1 (proj1_sig test_map)).
===> Some 1

The function pm_trace_root works for 1:

Compute (pm_trace_root 1 test_map).
===> Some 1

But for 2, "Compute (pm_trace_root 2 test_map)." generates an output of 912
lines.

I doubt it is caused by the similar problem mentioned in Xavier Leroy's
blog: http://gallium.inria.fr/blog/coq-eval/

But I'm not sure. Even it is for the same reason, I can not figure out
which proof term caused this problem. I attached the code. Could anyone
tell me how to debug this kind of things?

Thank you very much,

Shengyi Wang

Cell: [phone]

[Jason -Zhong Sheng- Hu]

Hi Shengyi,


are you referring to the opaque term issue? Yes, it causes that. Specifically, in your proof of accessibility:


Lemma Pos_lt_wf': forall x y : positive, x < y -> Acc Pos.lt x.
Proof.
intros. rewrite Pos2Nat.inj_lt in H.
remember (Pos.to_nat y) as n. clear y Heqn. revert x H. induction n; intros.
- pose proof (Pos2Nat.is_pos x). exfalso; intuition.
- apply lt_n_Sm_le, le_lt_or_eq in H. destruct H; auto.
constructor. intros. rewrite Pos2Nat.inj_lt, H in H0. apply IHn. assumption.
Defined.

all highlighted terms are opaque. I use emacs + company-coq, so for me `(company-coq-term-doc TERM)` will tell me if the term is opaque. Effectively, you want to make the entire well-formedness proof transparent, so probably all of them are the problem.


I got a question related to this: I am not sure if Pos2Nat.is_pos being opaque matters here as the branch is discharged by falsehood. In this case, we should not get into that branch. Is it correct to say that we would never have to care about reducibility of lemmas concluding falsehood?


Sincerely Yours,

Jason Hu
________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of Shengyi Wang <***@gmail.com>
Sent: August 18, 2018 12:34:57 PM
To: coq-***@inria.fr
Subject: [Coq-Club] Compute a general recursive function on dependent types.

Dear Coq users,

Recently I defined a map of "sig" type from positive to positive. The map should satisfy a property: it always maps a value v to a value which is not greater than v. Formally the definition is:

Definition pos_map_prop (t: PM.tree positive) : Prop :=
forall i j, PM.find i t = Some j -> j <= i.

Definition PosMap := {pm : PM.tree positive | pos_map_prop pm}.

Such a map can be viewed as a forest: each key in the map is a node. Each node points to a smaller value or itself.

Then I successfully defined a general recursive function "pm_trace_root" which traces back such a node along the pointers until to a self-pointing "root". The property of the map ensures the termination.

So far everything seems fine until I try to run the function in Coq. I defined a test_map which is essentially {1 -> 1, 2 -> 2}. I tested:

Compute (PM.find 2 (proj1_sig test_map)).
===> Some 1

Compute (PM.find 1 (proj1_sig test_map)).
===> Some 1

The function pm_trace_root works for 1:

Compute (pm_trace_root 1 test_map).
===> Some 1

But for 2, "Compute (pm_trace_root 2 test_map)." generates an output of 912 lines.

I doubt it is caused by the similar problem mentioned in Xavier Leroy's blog: http://gallium.inria.fr/blog/coq-eval/

But I'm not sure. Even it is for the same reason, I can not figure out which proof term caused this problem. I attached the code. Could anyone tell me how to debug this kind of things?

Thank you very much,

Shengyi Wang

Cell: [phone]

[Shengyi Wang]

Hi Jason,

Thank you very much for telling me the trick about determining opaque
terns. I tried to use "Print Opaque Dependencies Pos_lt_wf'." before but it
generates hundreds of dependencies which is then useless.

After some thought, I think my question is "How to preserve the "phase
distinction" in proofs used in a function?". I'm not sure opaque terns in
Pos_lt_wf' are the only causes. How about other lemmas involved in the
function definition such as "ptr_ok"?

Thank you,

Shengyi Wang

Cell: [phone]

Post by Jason -Zhong Sheng- Hu
Hi Shengyi,
are you referring to the opaque term issue? Yes, it causes that.
Lemma Pos_lt_wf': forall x y : positive, x < y -> Acc Pos.lt x.
Proof.
intros. rewrite Pos2Nat.inj_lt in H.
remember (Pos.to_nat y) as n. clear y Heqn. revert x H. induction n; intros.
- pose proof (Pos2Nat.is_pos x). exfalso; intuition.
- apply lt_n_Sm_le, le_lt_or_eq in H. destruct H; auto.
constructor. intros. rewrite Pos2Nat.inj_lt, H in H0. apply IHn. assumption.
Defined.
all highlighted terms are opaque. I use emacs + company-coq, so for me `(company-coq-term-doc
TERM)` will tell me if the term is opaque. Effectively, you want to make
the entire well-formedness proof transparent, so probably all of them are
the problem.
I got a question related to this: I am not sure if Pos2Nat.is_pos being
opaque matters here as the branch is discharged by falsehood. In this case,
we should not get into that branch. Is it correct to say that we would
never have to care about reducibility of lemmas concluding falsehood?
*Sincerely Yours, *
* Jason Hu*
------------------------------
*Sent:* August 18, 2018 12:34:57 PM
*Subject:* [Coq-Club] Compute a general recursive function on dependent
types.
Dear Coq users,
Recently I defined a map of "sig" type from positive to positive. The map
should satisfy a property: it always maps a value v to a value which is not
Definition pos_map_prop (t: PM.tree positive) : Prop :=
forall i j, PM.find i t = Some j -> j <= i.
Definition PosMap := {pm : PM.tree positive | pos_map_prop pm}.
Such a map can be viewed as a forest: each key in the map is a node. Each
node points to a smaller value or itself.
Then I successfully defined a general recursive function "pm_trace_root"
which traces back such a node along the pointers until to a self-pointing
"root". The property of the map ensures the termination.
So far everything seems fine until I try to run the function in Coq. I
Compute (PM.find 2 (proj1_sig test_map)).
===> Some 1
Compute (PM.find 1 (proj1_sig test_map)).
===> Some 1
Compute (pm_trace_root 1 test_map).
===> Some 1
But for 2, "Compute (pm_trace_root 2 test_map)." generates an output of 912 lines.
I doubt it is caused by the similar problem mentioned in Xavier Leroy's
blog: http://gallium.inria.fr/blog/coq-eval/
But I'm not sure. Even it is for the same reason, I can not figure out
which proof term caused this problem. I attached the code. Could anyone
tell me how to debug this kind of things?
Thank you very much,
Shengyi Wang
Cell: [phone]

[Xavier Leroy]

After some thought, I think my question is "How to preserve the "phase distinction" in proofs used in a function?". I'm not sure opaque terns in Pos_lt_wf' are the only causes. How about other lemmas involved in the function definition such as "ptr_ok"?

I don't think there is a general answer to your question beyond "try to evaluate and see what happens".

My personal experience with { x : A | P x } types and other instances of mild uses of dependent types is that they compute well most of the time.

For proofs of well-foundedness / accessibility, there exists a neat trick to turn an opaque proof (or a proof that computes very inefficiently) into a transparent, computationally-cheap proof that lets you evaluate general recursive definitions efficiently:

https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00034.html

I wish this trick was made available in the Coq stdlib.

- Xavier Leroy

Thank you,
Shengyi Wang
Cell: [phone]
Hi Shengyi,
Lemma Pos_lt_wf': forall x y : positive, x < y -> Acc Pos.lt x.
Proof.
intros. rewrite Pos2Nat.inj_lt in H.
remember (Pos.to_nat y) as n. clear y Heqn. revert x H. induction n; intros.
- pose proof (Pos2Nat.is_pos x). exfalso; intuition.
- apply lt_n_Sm_le, le_lt_or_eq in H. destruct H; auto.
constructor. intros. rewrite Pos2Nat.inj_lt, H in H0. apply IHn. assumption.
Defined.
all highlighted terms are opaque. I use emacs + company-coq, so for me `(company-coq-term-doc TERM)` will tell me if the term is opaque. Effectively, you want to make the entire well-formedness proof transparent, so probably all of them are the problem.
I got a question related to this: I am not sure if Pos2Nat.is_pos being opaque matters here as the branch is discharged by falsehood. In this case, we should not get into that branch. Is it correct to say that we would never have to care about reducibility of lemmas concluding falsehood?
*Sincerely Yours,
*
*
Jason Hu*
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
*Sent:* August 18, 2018 12:34:57 PM
*Subject:* [Coq-Club] Compute a general recursive function on dependent types.
Dear Coq users,
Definition pos_map_prop (t: PM.tree positive) : Prop :=
forall i j, PM.find i t = Some j -> j <= i.
Definition PosMap := {pm : PM.tree positive | pos_map_prop pm}.
Such a map can be viewed as a forest: each key in the map is a node. Each node points to a smaller value or itself.
Then I successfully defined a general recursive function "pm_trace_root" which traces back such a node along the pointers until to a self-pointing "root". The property of the map ensures the termination.
Compute (PM.find 2 (proj1_sig test_map)).
===> Some 1
Compute (PM.find 1 (proj1_sig test_map)).
===> Some 1
Compute (pm_trace_root 1 test_map).
===> Some 1
But for 2, "Compute (pm_trace_root 2 test_map)." generates an output of 912 lines.
I doubt it is caused by the similar problem mentioned in Xavier Leroy's blog: http://gallium.inria.fr/blog/coq-eval/
But I'm not sure. Even it is for the same reason, I can not figure out which proof term caused this problem. I attached the code. Could anyone tell me how to debug this kind of things?
Thank you very much,
Shengyi Wang
Cell: [phone]

[Shengyi Wang]

Thank you very much!

I'll try to use this trick after I fixed the problem.

Shengyi Wang

Cell: [phone]

Post by Shengyi Wang

Post by Shengyi Wang
After some thought, I think my question is "How to preserve the "phase

distinction" in proofs used in a function?". I'm not sure opaque terns in
Pos_lt_wf' are the only causes. How about other lemmas involved in the
function definition such as "ptr_ok"?
I don't think there is a general answer to your question beyond "try to
evaluate and see what happens".
My personal experience with { x : A | P x } types and other instances of
mild uses of dependent types is that they compute well most of the time.
For proofs of well-foundedness / accessibility, there exists a neat trick
to turn an opaque proof (or a proof that computes very inefficiently) into
a transparent, computationally-cheap proof that lets you evaluate general
https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00034.html
I wish this trick was made available in the Coq stdlib.
- Xavier Leroy

Post by Shengyi Wang
Thank you,
Shengyi Wang
Cell: [phone]
Hi Shengyi,
are you referring to the opaque term issue? Yes, it causes that.
Lemma Pos_lt_wf': forall x y : positive, x < y -> Acc Pos.lt x.
Proof.
intros. rewrite Pos2Nat.inj_lt in H.
remember (Pos.to_nat y) as n. clear y Heqn. revert x H. induction

n; intros.

Post by Shengyi Wang
- pose proof (Pos2Nat.is_pos x). exfalso; intuition.
- apply lt_n_Sm_le, le_lt_or_eq in H. destruct H; auto.
constructor. intros. rewrite Pos2Nat.inj_lt, H in H0. apply IHn.

assumption.

Post by Shengyi Wang
Defined.
all highlighted terms are opaque. I use emacs + company-coq, so for

me `(company-coq-term-doc TERM)` will tell me if the term is opaque.
Effectively, you want to make the entire well-formedness proof transparent,
so probably all of them are the problem.

Post by Shengyi Wang
I got a question related to this: I am not sure if Pos2Nat.is_pos

being opaque matters here as the branch is discharged by falsehood. In this
case, we should not get into that branch. Is it correct to say that we
would never have to care about reducibility of lemmas concluding falsehood?

Post by Shengyi Wang
*Sincerely Yours,
*
*
Jason Hu*

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Post by Shengyi Wang
*Sent:* August 18, 2018 12:34:57 PM
*Subject:* [Coq-Club] Compute a general recursive function on

dependent types.

Post by Shengyi Wang
Dear Coq users,
Recently I defined a map of "sig" type from positive to positive.

The map should satisfy a property: it always maps a value v to a value

Post by Shengyi Wang
Definition pos_map_prop (t: PM.tree positive) : Prop :=
forall i j, PM.find i t = Some j -> j <= i.
Definition PosMap := {pm : PM.tree positive | pos_map_prop pm}.
Such a map can be viewed as a forest: each key in the map is a node.

Each node points to a smaller value or itself.

Post by Shengyi Wang
Then I successfully defined a general recursive function

"pm_trace_root" which traces back such a node along the pointers until to a
self-pointing "root". The property of the map ensures the termination.

Post by Shengyi Wang
So far everything seems fine until I try to run the function in Coq.
Compute (PM.find 2 (proj1_sig test_map)).
===> Some 1
Compute (PM.find 1 (proj1_sig test_map)).
===> Some 1
Compute (pm_trace_root 1 test_map).
===> Some 1
But for 2, "Compute (pm_trace_root 2 test_map)." generates an output

of 912 lines.

Post by Shengyi Wang
I doubt it is caused by the similar problem mentioned in Xavier

Leroy's blog: http://gallium.inria.fr/blog/coq-eval/

Post by Shengyi Wang
But I'm not sure. Even it is for the same reason, I can not figure

out which proof term caused this problem. I attached the code. Could anyone
tell me how to debug this kind of things?

Post by Shengyi Wang
Thank you very much,
Shengyi Wang
Cell: [phone]