The Coq mailing list

[Shengyi Wang <txyyss AT gmail.com>]

Thank you very much!

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

Shengyi Wang

Cell: +65-83509639

Xavier Leroy <Xavier.Leroy AT inria.fr> 于2018年8月20日周一 上午12:21写道：

On 08/19/2018 02:23 AM, Shengyi Wang wrote:
>
> 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: +65-83509639
>
>
> Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com <mailto: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 <mailto:coq-club-request AT inria.fr> <coq-club-request AT inria.fr <mailto:coq-club-request AT inria.fr>> on behalf of Shengyi Wang <txyyss AT gmail.com <mailto:txyyss AT gmail.com>>
>     *Sent:* August 18, 2018 12:34:57 PM
>     *To:* coq-club AT inria.fr <mailto: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
>