[Agda] conjectures in agda

[Martin Escardo]

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