The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

On 20/02/2021 00:33, Daniel Schepler wrote:
> What if you assume the axiom classic_dec : forall P : Prop, {P} + {~P}
> and then define something along the lines of:
> Definition f := fun (X : Type) =>
> match classic_dec (bool = X) with
> | left Heq => match Heq in (_ = X') return ((unit -> X') -> X') with
>               | eq_refl => fun i => bnot (i tt)
>               end
> | right _ => fun i => i tt
> end.
> 
> That axiom should be consistent in Coq: after all, it's implied by the
> conjunction of classic : forall P : Prop, P \/ ~P and
> definite_description : forall (A : Type) (P : A -> Prop), exists! x:A,
> P x -> { x:A | P x }.

Yes, this is enough to convince me that the parametricy axiom is not
provable in Coq, but it might sound to admit it on its own.

See the proof script below. Note that I changed [X : Type] to [X : Set],
due to universe inconsistencies.

> Section Challenge.
> 
>   Variable classic_dec : forall P : Prop, {P} + {~P}.
>   Variable UIP_refl : forall (X : Type) (x : X) (H : x = x), H = eq_refl.
> 
>   Definition f :=
>     fun (X : Set) => (* Note that I changed the sort of [X] to [Set] *)
>       match classic_dec (bool = X) with
>       | left Heq => match Heq in (_ = X') return ((unit -> X') -> X') with
>                     | eq_refl => fun i => negb (i tt)
>                     end
>       | right _ => fun i => i tt
>       end.
> 
>   Variable tam : forall (f : forall X : Set, (unit -> X) -> X),
>     forall (X : Set) (i : unit -> X),
>       f X i = i tt.
>   Goal False.
>     specialize (tam f bool (fun _ => true)); unfold f in tam.
>     destruct (classic_dec (bool = bool)); cbn in *; try tauto.
>     pose proof UIP_refl _ _ e as ->.
>     discriminate.
>   Qed.
> 
> End Challenge.

This is just another reminder that we ought to be careful about which
axioms we admit ;-)

-- Maximilian


PS: Fortunately, I didn't need this axiom mentioned in the first mail.
Using it would have spared me over 1k boilerplate LOC though. Basically,
I have used instances of this axiom for some classes of functions [f].