[Agda] conjectures in agda

[Andrés Sicard-Ramírez]

Hi Martin,

Maybe I am missing something about your approach, but why not define
conjecture by

postulate
   conjecture : {A : Set} → A

On Wed, Jan 6, 2010 at 7:10 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

> 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).
>
> 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).
>
> For example, suppose you need a lemma for the proof of a theorem:
>
>  lemma : ... statement ...
>
> Suppose everything else has been proved, using this lemma, but not the
> lemma itself. The you can write the following:
>
>  lemma : ... statement ...
>  lemma = conjecture
>
> If your proof of the theorem is correct assuming the conjecture, your agda
> file will compile, and it won't otherwise.
>
> Moreover, you can use this when there are several cases, e.g.
>
>  lemma : ... statement ...
>  lemma O = conjecture
>  lemma (succ n) = another-lemma n (lemma n)
>
> 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).
>
> I thought you might find this useful. (I didn't take universe polymorphism
> into account.)
>
> Martin
> --
> module Conjecture where
> -- Use this module to be able to compile
> -- proofs/programs with missing parts.
>
> conjecture : {A : Set} → A
> conjecture {A} = ! inhabitant-of-∅
>  where data ∅ : Set where
>       -- no elements in the empty set.
>       ! : ∅ → A
>       ! ()
>       postulate inhabitant-of-∅ : ∅
>
> -- End of message
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100106/7d662318/attachment.html