The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

The following piece of code accomplishes the same thing as my example with tactics, using Program:

Require Program.Tactics.

Unset Transparent Obligations.
Program Definition positive : { n : nat | n > 0 } := exist _ 1 _.
(* Solving obligations automatically... *)
Compute proj1_sig positive. (* 1 *)
About positive. (* ... positive is transparent *)
Print positive.
(* positive =
    exist (fun n : nat => n > 0) 1 positive_obligation_1
     : {n : nat | n > 0} *)
About positive_obligation_1. (* ... positive_obligation_1 is opaque *)

Le lun. 22 janv. 2018 à 11:18, Siddharth Bhat <siddu.druid AT gmail.com> a écrit :

That is interesting information, thank you.

When one uses Program, what happens to the proof obligations one provides? Do those "leak out" as well? (The impression I got from some cursory use is that it does not). If not, how does that work?

I left trying to dependent type my code for a while now, because I don't deally understand how to control proof terms with dependent types.

Cheers

Siddharth

On Mon 22 Jan, 2018, 15:03 Théo Zimmermann, <theo.zimmi AT gmail.com> wrote:

There are on-going debates whether programming definitions using tactics is OK or not but what is agreed on is that building transparent terms (definitions) using automated tactics is not a good idea (you should have a clear idea of what the tactic is doing).

When you want to use an automated tactic to prove a proof obligation as part of a definition, you may encapsulate it into "abstract" to make this part of the term opaque :

Require Import Omega.

Definition positive : { n : nat | n > 0 }.
  exists 1.
  abstract omega.
Defined.

Compute proj1_sig positive. (* 1 *)

About positive. (* ... positive is transparent *)

Print positive.

(* positive =
    exist (fun n : nat => n > 0) 1 positive_subproof
     : {n : nat | n > 0} *)

About positive_subproof.
(* positive_subproof : 1 > 0

    positive_subproof is opaque *)

That being said, I'm not aware of any clear advantage of this method over using Program.

Théo

Le sam. 20 janv. 2018 à 14:27, Siddharth Bhat <siddu.druid AT gmail.com> a écrit :

I've been trying to learn how to write dependently typed code in Coq.

As far as I can tell, there are three styles:

1. Use tactics to fill in Definition blocks.

2. Directly "implement" stuff with dependent types (like Idris)

3. Use Program to delay obligations, so write "normal" code and fulfil obligations later.

The problem I face with #1 is that _proving_ things about Definitions encoded this way is impossible for me. For example, if I use omega in some Definition D, I cannot prove anything about D, because on unfolding D, I see the mess that is the omega implementation, I assume.

So, for proving things about definitions, #1 is out.

#2 is.. challenging, and as a newbie, I find that I often do not know how to express the things I want to say, or do not know how to convince Coq that certain things are impossible (eg: safe indexing into a vector)

So, for now, #3 seems easiest.

I would like references on the third style of implementing things. Could someone please recommend reading material?

Thanks,

Siddharth

--

Sending this from my phone, please excuse any typos!

--

Sending this from my phone, please excuse any typos!