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
)
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
sym_id
:
identity
x
y
->
identity
y
x
.
Lemma
trans_id
:
identity
x
y
->
identity
y
z
->
identity
x
z
.
Lemma
congr_id
:
identity
x
y
->
identity
(
f
x
) (
f
y
).
Lemma
sym_not_id
:
notT
(
identity
x
y
) ->
notT
(
identity
y
x
).
End
identity_is_a_congruence
.
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
.
Hint
Immediate
sym_id
sym_not_id
:
core
v62
.