The Coq mailing list

[Shengyi Wang <txyyss AT gmail.com>]

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: +65-83509639

Attachment: dep_map.v
Description: Binary data