The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/02/2014 01:02 PM, Eddy Westbrook wrote:
> Well, but given that it is a choice principle, maybe we can conclude (in 
> response to Jonathan’s original question) that it is not really constructive…?
>
> -Eddy

Mostly, I was just trying to think of what Coq's logic would allow if 
its Prop elimination rules were extended to allow Prop elimination 
anywhere in a Prop-rooted proof subtree instead of just in Prop subgoals 
themselves.

It is interesting that such an extension would be equivalent to a kind 
of weak choice axiom.  Because I was just thinking in very practical 
terms - sometimes one finds oneself in a non-Prop subgoal in a 
Prop-rooted proof subtree and needs to analyze a Prop - and currently 
the only way to do that is to undo back to some earlier Prop subgoal 
(perhaps the root of that subtree) and do the analysis there - and such 
undoing could require restructuring the proof.  So, I thought that such 
an extension wouldn't add anything at all to the logic - but it does.  
And, it's a weak choice axiom, hence not constructive.

But, I guess that brings out a different kind of theoretical question.  
Coq's Props already have a different logic (impredicative) from the 
logic of Types.  And, of course, one doesn't have to worry about what 
Props would extract to, as they don't.  Why then keep Prop so constructive?

Certainly, one can always add their favorite choice axiom(s).  But, the 
above Prop-subtree elimination extension, even though it seems to be 
equivalent to a weak choice axiom, can't be added through use of any 
such axiom (that would be consistent with the rest of Coq's logic) - at 
least I can't see how.

-- Jonathan

> On Oct 2, 2014, at 9:41 AM, Arnaud Spiwack 
> <aspiwack AT lix.polytechnique.fr>
>  wrote:
>
> > Well, this principle of choice is equivalent to the dependent version of 
> > Pierre-Marie's above: [forall A B, (forall x:A, inhabited B) -> inhabited 
> > (forall x:A, B)]. I don't think it implies excluded-middle by itself. But it 
> > does if you add in quotient types. The non-dependent version, however, seems 
> > pretty weak.
> >
> > On 2 October 2014 18:01, Eddy Westbrook 
> > <westbrook AT kestrel.edu>
> >  wrote:
> > Yes, you are right, thanks!
> >
> > I got the name TTDA from Werner's paper "Sets in Types, Types in Sets", where 
> > he has a different axiom that he calls a choice principle.
> >
> > It also looks like AC_fun in Coq.Logic.ChoiceFacts.
> >
> > So, then, does this version of choice imply excluded middle? I can't find a 
> > proof in the standard library...
> >
> > Eddy
> >
> > Sent from my iPhone
> >
> > > On Oct 1, 2014, at 6:12 PM, Jonathan 
> > > <jonikelee AT gmail.com>
> > >  wrote:
> > >
> > > > On 10/01/2014 09:01 PM, Eddy Westbrook wrote:
> > > > The nondep_AC axiom below is, I think, equivalent to the Type-Theoretic 
> > > > Description Axiom (TTDA), which is this:
> > > >
> > > > Definition TTDA : Type :=
> > > >    forall (A B : Type) (P : A -> B -> Prop),
> > > >      (forall (a : A), exists b, P a b) ->
> > > >      (exists f, forall (a : A), P a (f a)).
> > > That looks like Coq.Logic.ClassicalChoice.choice.
> > >
> > > > TTDA has some sort of non-constructive content, in that it, with 
> > > > propositional Excluded Middle, allows you to prove informative Excluded 
> > > > Middle. I am not what TTDA just by itself allows, however.
> > > >
> > > > -Eddy
> > > >
> > > > > On Oct 1, 2014, at 5:29 AM, Pierre-Marie Pédrot 
> > > > > <pierre-marie.pedrot AT inria.fr>
> > > > >  wrote:
> > > > >
> > > > > > On 30/09/2014 22:47, Jonathan wrote:
> > > > > > Anyone seen it before?
> > > > > It seems instead equivalent to a weak form of a non-dependent axiom of
> > > > > choice, rather than to excluded middle :
> > > > >
> > > > > Definition nondep_AC := forall A B, (A -> inhabited B) -> inhabited (A
> > > > > -> B).
> > > > > Definition escape := forall A, inhabited (inhabited A -> A).
> > > > >
> > > > > Lemma dir : nondep_AC -> escape.
> > > > > Proof.
> > > > > intros ac A; apply ac; trivial.
> > > > > Qed.
> > > > >
> > > > > Lemma rev : escape -> nondep_AC.
> > > > > Proof.
> > > > > intros esc A B f.
> > > > > destruct (esc B) as [g].
> > > > > constructor; auto.
> > > > > Qed.
> > > > >
> > > > > PMP