The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

On Dec 12, 2013 2:12 PM, "Arthur Azevedo de Amorim" <arthur.aa AT gmail.com> wrote:

Wow, I'm really impressed that the termination checker accepts the definition of  contradiction... Why is this reasonable?

On Dec 12, 2013 2:02 PM, "Daniel Schepler" <dschepler AT gmail.com> wrote:

Section func_unit_discr.

Hypothesis Heq : (False -> False) = unit :> Type.

Fixpoint contradiction (u : unit) : False :=

match u with

| tt => contradiction (

        match Heq in (_ = T) return T with

        | eq_refl => fun f:False => match f with end

        end

        )

end.

End func_unit_discr.

Definition func_unit_discr :

  (False -> False) <> unit :> Type :=

fun Heq => contradiction Heq tt.

Section bijective_impl_eq.

Definition injective {A B:Type} (f:A->B) : Prop :=

forall x y:A, f x = f y -> x = y.

Definition surjective {A B:Type} (f:A->B) : Prop :=

forall y:B, exists x:A, f x = y.

Definition bijective {A B:Type} (f:A->B) : Prop :=

injective f /\ surjective f.

Hypothesis bijective_impl_eq :

  forall (A B:Type) (f:A->B), bijective f -> A = B.

Hypothesis functional_extensionality :

  forall (A B:Type) (f g:A->B),

  (forall x:A, f x = g x) -> f = g.

Lemma unit_eq_False_False_funs :

  (False -> False) = unit :> Type.

Proof.

apply bijective_impl_eq with (f := fun _ => tt).

split.

+ intros f g ?.

  apply functional_extensionality.

  intros [].

+ intros [].

  exists (fun f:False => match f with end).

  reflexivity.

Qed.

Definition not_bijective_impl_eq : False :=

func_unit_discr unit_eq_False_False_funs.

End bijective_impl_eq.

-- 

Daniel Schepler