The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/15/2014 10:32 AM, Hugo Herbelin wrote:
> ...
> You would need -impredicative-set option to show that the
> interpretation of Prop as the impredicative variant of Set satisfies
> your axiom.
>
> Inductive Erasable(S : Set) : Set := erasable: S -> Erasable S.

I note that here Erasable is Set -> Set, not Set -> Prop.

> Arguments erasable [S] _.
>
> Theorem Erasable_inj : forall {S : Set}{a b : S}, erasable a=erasable b -> 
> a=b.
> Proof.
> intros * H.
> set (f := fun (x:Erasable S) => let 'erasable y := x in y).
> apply f_equal with (f:=f) in H.
> assumption.
> Qed.

But that's provable with or without -impredicative-set.  (a shorter 
proof is just: intros * H. injection H. trivial)

> But you don't need -impredicative-set to technically postulate your
> axiom (having option -impredicative-set on does not ensure in itself
> that the interpretation of Prop as the impredicative variant of Set is
> sound - an analysis of the CIC rules is necessary -, nor does it
> prevent introducing other axioms that would contradict this
> interpretation of Prop).
>
> Hugo

I guess in this case, the devil we don't know is better than the devil 
we do know.  I will incorporate a summary of this discussion and its 
caveats into my github project.

A side note: Making sure that other axioms aren't introduced that cause 
a problem is not so easy.  For example, Program makes use of 
proof_irrelevance.  I guess I should always do Print Assumptions.

A suggestion:  how about adding something like a "Restrict Assumptions" 
command that would take a list of axioms and raise an error if the 
actual assumptions used is not a subset of those mentioned in the list?

-- Jonathan