The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 28 Sep 2012 19:03:05 +0200,
Jonas Oberhauser 
<s9joober AT gmail.com>
 a écrit :

> 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

I guess you mean "∀ x, f x = right tt → ¬P x"
(or "∀ x, f x = No _ _ → ¬ P x" with my example)

> 
> 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 used "half" rather than "semi" in order to avoid confusion.

> 
> 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.

I think it cannot really be a lot harder, but proofs can be quite
different in appearance.

Using my previous definitions:

---------

Definition list_dec1 {A} (d : ∀ (a b : A), {a=b}+{a≠b})
: ∀ (l m : list A), dec (eq l) m.
refine (
  fix ld l :=
  match l as l return ∀ m, dec (eq l) m with
  | nil => λ m, match m with
                | nil => Ok _ _ eq_refl
                | cons hm m => Ko _ _ _
                end
  | cons hl l => λ m, match m with
                      | nil => Ko _ _ _
                      | cons hm m => if d hl hm
                                     then if ld l m
                                          then Ok _ _ _
                                          else Ko _ _ _
                                     else Ko _ _ _
                      end
  end
).
Proof.
  clear; abstract (exact (λ H, match H with eq_refl => True end)).
Proof.
  clear; abstract (exact (λ H, match H with eq_refl => True end)).
Proof.
  clear - _H _H0;
  abstract (exact (match _H with eq_refl =>
                   match _H0 with eq_refl =>
                   eq_refl
                   end end)).
Proof.
  clear - _H0;
  abstract (exact (λ H, _H0 match H with eq_refl => eq_refl end)).
Proof.
  clear - _H;
  abstract (exact (λ H, _H match H with eq_refl => eq_refl end)).
Defined.

Definition list_dec2 {A} (d : ∀ (a b : A), {a=b}+{a≠b})
: ∀ (l m : list A), sdec (eq l) m.
refine (
  fix ld l :=
  match l as l return ∀ m, sdec (eq l) m with
  | nil => λ m, match m with
                | nil => Yes _ _ eq_refl
                | cons hm m => No _ _
                end
  | cons hl l => λ m, match m with
                      | nil => No _ _
                      | cons hm m => if d hl hm
                                     then if ld l m
                                          then Yes _ _ _
                                          else No _ _
                                     else No _ _
                      end
  end
).
Proof.
  clear - _H _H0;
  abstract (exact (match _H with eq_refl =>
                   match _H0 with eq_refl =>
                   eq_refl
                   end end)).
Defined. (* only one proof here! *)
Lemma ld2strong {A} d (l:list A) : Strong_sdec (list_dec2 d l).
Proof.
  intros m [].
  induction l; simpl; auto.
    repeat esplit.
  destruct IHl; rewrite H; clear.
  destruct (d a a).
    repeat esplit.
  now destruct n.
Qed.

--------------

I know I didn't use powerful tactics, and I know of "decide equality",
"discriminate", "inversion" and all that stuff. In this case, I think I
could provide one line tactics, but I do not care of it. For me, the
two approaches are different. The second one doesn't have to deal with
so many "…→False".

> 
> Kind regards, jonas
>