The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 28.09.2012 18:18, schrieb AUGER Cédric:
> Given a type X:Type and a predicate P:X→Prop, a decision procedure is
> some function of type ∀ x, {P x}+{¬P x}.
>
> I was interested in a simpler thing, that is some procedure of type ∀
> x, {P x}+unit (that is that you do not care to prove that your property
> is wrong). I do not know how would be called such a procedure
> (semi-decision procedure wouldn’t fit as it stands for something
> slightly different, let us call that a half-decision procedure. If you
> have a better name, let me know, I would be interested).
>
> Basically you have two special cases, the not very interesting one
> defined by "λ x, right tt" (so you always say 'wrong') and the most
> interesting one (or an extensionnaly equal one) "λ x, match f x with
> left π => left π | right π => right tt end".
>
> So I was wondering what criterion would be good to say which ones are
> good and which ones are bad. I thought that if you have the following
> property: "∀ x, P x → ∃ π, f x = left π" where 'f' is my half-decision
> procedure. I thought that if a function 'f' verifies this property,
> then I could classically prove that it is a decision procedure. In fact
> it ended up that this is even intuitionistically provable. But in
> practice, I have the feeling that when P is some big inductive type, it
> easier to build a half-decision procedure and prove that it verifies
> our property than to directly write the decision procedure.
>
> I lack some experimentation with "half-decision", so my feelings may be
> wrong. But when I used to try the direct approach, it occured that all
> those "¬P" I encountered in goals and hypothesis were a little annoying.
>
> -----------------
> Require Import Utf8.
>
> Definition Pred X := X → Prop.
>
> Inductive dec {X} (P : Pred X) (x : X) : Type :=
>    | Ok : P x → dec P x
>    | Ko : ¬ P x → dec P x
> .
>
> Inductive sdec {X} (P : Pred X) (x : X) : Type :=
>    | Yes : P x → sdec P x
>    | No : sdec P x
> .
>
> Definition Strong_sdec {X} {P : Pred X} (f : ∀ x, sdec P x) :=
>    ∀ x, P x → ∃ π, f x = Yes P x π.
>
> Definition strengthen_dec {X} {P : Pred X} (f : ∀ x, sdec P x)
> : Strong_sdec f → ∀ x, dec P x
> := λ H x, match f x as y return (P x → ∃ π, y = Yes P x π) → dec P x
> with | Yes π => λ _, Ok P x π
>            | No => λ H, Ko P x (λ K, match H K with ex_intro π ρ =>
>                                      match ρ with eq_refl => True
>                                      end end)
>            end (H x).

∀ x, P x → ∃ π, f x = left π

If you can prove that property, then you also have:

∀ x π, f x = right π → ¬P x

And obviously you have

∀ x π, f x = left π → P x
(since π : P x)

I guess this is a proof why semi-decidable problems can not be decided by 
semi-decidable procedures in coq (I'm sticking to your terminology here).

I have not worked with this approach myself, but I assume that proving the 
lemma takes about as much sweat as proving the decision procedure.

Kind regards, jonas