Library Coq.Init.Logic_Type


This module defines type constructors for types in Type (Datatypes.v and Logic.v defined them for types in Set)

Set Implicit Arguments.

Require Import Ltac.
Require Import Datatypes.
Require Export Logic.

Negation of a type in Type

Definition notT (A:Type) := A -> False.

Properties of identity

Section identity_is_a_congruence.

 Variables A B : Type.
 Variable f : A -> B.

 Variables x y z : A.

 Lemma identity_sym : identity x y -> identity y x.

 Lemma identity_trans : identity x y -> identity y z -> identity x z.

 Lemma identity_congr : identity x y -> identity (f x) (f y).

 Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).

End identity_is_a_congruence.

Register identity_sym as core.identity.sym.
Register identity_trans as core.identity.trans.
Register identity_congr as core.identity.congr.

Definition identity_ind_r :
  forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
Defined.

Definition identity_rec_r :
  forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
Defined.

Definition identity_rect_r :
  forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
Defined.

#[global]
Hint Immediate identity_sym not_identity_sym: core.

Notation refl_id := identity_refl (only parsing).
Notation sym_id := identity_sym (only parsing).
Notation trans_id := identity_trans (only parsing).
Notation sym_not_id := not_identity_sym (only parsing).