The Coq mailing list

[Shengyi Wang <txyyss AT gmail.com>]

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

Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> 于2018年8月19日周日 上午2:29写道：

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-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Shengyi Wang <txyyss AT gmail.com>
Sent: August 18, 2018 12:34:57 PM
To: coq-club AT 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: +65-83509639