Hi Martin,<br><br>Maybe I am missing something about your approach, but why not define conjecture by<br><br>postulate<br> conjecture : {A : Set} → A<br><br><div class="gmail_quote">On Wed, Jan 6, 2010 at 7:10 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Some of you have discussed how to compile agda proofs with missing parts. Some of you have suggested to use postulates, but this is inconvenient in several ways. For example, among other things, you have to explicitly type postulates, and one advantage of agda is the facility to infer types (often).<br>
<br>
I've come across the following clean way of doing this. I define a module "Conjecture" (listed below after my signature), which defines a proof "conjecture" that proves everything (using "postulate", of course).<br>
<br>
For example, suppose you need a lemma for the proof of a theorem:<br>
<br>
lemma : ... statement ...<br>
<br>
Suppose everything else has been proved, using this lemma, but not the lemma itself. The you can write the following:<br>
<br>
lemma : ... statement ...<br>
lemma = conjecture<br>
<br>
If your proof of the theorem is correct assuming the conjecture, your agda file will compile, and it won't otherwise.<br>
<br>
Moreover, you can use this when there are several cases, e.g.<br>
<br>
lemma : ... statement ...<br>
lemma O = conjecture<br>
lemma (succ n) = another-lemma n (lemma n)<br>
<br>
Additionally, there can be several conjectures in a proof, and your proof will compile with the conjectures regarded as hypotheses (giving an error, or accepting your proof from the conjectured hypotheses).<br>
<br>
I thought you might find this useful. (I didn't take universe polymorphism into account.)<br>
<br>
Martin<br>
--<br>
module Conjecture where<br>
-- Use this module to be able to compile<br>
-- proofs/programs with missing parts.<br>
<br>
conjecture : {A : Set} → A<br>
conjecture {A} = ! inhabitant-of-∅<br>
where data ∅ : Set where<br>
-- no elements in the empty set.<br>
! : ∅ → A<br>
! ()<br>
postulate inhabitant-of-∅ : ∅<br>
<br>
-- End of message<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br><br clear="all"><br>-- <br>Andrés<br>