The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 28.09.2012 19:55, schrieb AUGER Cédric:
> 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)
I do not think this matters since∀ π : unit, π = tt
But I believe my formulation could save you a destruct here and there.

> > 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.
Oh, my bad. It appears I accidentaly reversed your terminology. I meant 
half-decision procedures of course.

> > 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 u.
>    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".
The two approaches are different, but how much work does it save you? Of 
course you could argue that the "…→False" are the annoying part of the 
proofs, in which case this approach could be certainly interesting. I 
mean, this type is inhabited:

"forall X (P : X -> Prop) (f : forall x : X, P x + unit) (H : forall x, 
P x -> exists p, f x = inl unit p) x, {P x} + {~ P x}"

(sorry for not using the nice formatting that you do but I'm not familar 
with it yet)

Hence we can always use that second approach and get the same results 
anyway.