The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

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
>