Library Corelib.Init.Specif
Basic specifications : sets that may contain logical information
Subsets and Sigma-types
(sig A P), or more suggestively {x:A | P x}, denotes the subset of elements of the type A which satisfy the predicate P. Similarly (sig2 A P Q), or {x:A | P x & Q x}, denotes the subset of elements of the type A which satisfy both P and Q.
#[universes(template)]
Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.
Register sig as core.sig.type.
Register exist as core.sig.intro.
Register sig_rect as core.sig.rect.
#[universes(template)]
Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
exist2 : forall x:A, P x -> Q x -> sig2 P Q.
(sigT A P), or more suggestively {x:A & (P x)} is a Sigma-type. Similarly for (sigT2 A P Q), also written {x:A & (P x) & (Q x)}.
#[universes(template)]
Inductive sigT (A:Type) (P:A -> Type) : Type :=
existT : forall x:A, P x -> sigT P.
Register sigT as core.sigT.type.
Register existT as core.sigT.intro.
Register sigT_rect as core.sigT.rect.
#[universes(template)]
Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
Arguments sig (A P)%_type.
Arguments sig2 (A P Q)%_type.
Arguments sigT (A P)%_type.
Arguments sigT2 (A P Q)%_type.
Notation "{ x | P }" := (sig (fun x => P%_type)) : type_scope.
Notation "{ x | P & Q }" := (sig2 (fun x => P%_type) (fun x => Q%_type)) : type_scope.
Notation "{ x : A | P }" := (sig (A:=A) (fun x => P%_type)) : type_scope.
Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P%_type) (fun x => Q%_type)) :
type_scope.
Notation "{ x & P }" := (sigT (fun x => P%_type)) : type_scope.
Notation "{ x & P & Q }" := (sigT2 (fun x => P%_type) (fun x => Q%_type)) : type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P%_type)) : type_scope.
Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P%_type) (fun x => Q)) :
type_scope.
Notation "{ ' pat | P }" := (sig (fun pat => P%_type)) : type_scope.
Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P%_type) (fun pat => Q%_type)) : type_scope.
Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P%_type)) : type_scope.
Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P%_type) (fun pat => Q%_type)) :
type_scope.
Notation "{ ' pat & P }" := (sigT (fun pat => P%_type)) : type_scope.
Notation "{ ' pat & P & Q }" := (sigT2 (fun pat => P%_type) (fun pat => Q%_type)) : type_scope.
Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P%_type)) : type_scope.
Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P%_type) (fun pat => Q%_type)) :
type_scope.
Add Printing Let sig.
Add Printing Let sig2.
Add Printing Let sigT.
Add Printing Let sigT2.
Projections of sig
An element y of a subset {x:A | (P x)} is the pair of an a of type A and of a proof h that a satisfies P. Then (proj1_sig y) is the witness a and (proj2_sig y) is the proof of (P a)
Section Subset_projections.
Variable A : Type.
Variable P : A -> Prop.
Definition proj1_sig (e:sig P) := match e with
| exist _ a b => a
end.
Definition proj2_sig (e:sig P) :=
match e return P (proj1_sig e) with
| exist _ a b => b
end.
Register proj1_sig as core.sig.proj1.
Register proj2_sig as core.sig.proj2.
End Subset_projections.
sig2 of a predicate can be projected to a sig.
This allows proj1_sig and proj2_sig to be usable with sig2.
The let statements occur in the body of the exist so that proj1_sig of a coerced X : sig2 P Q will unify with let (a, _, _) := X in a
Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P
:= exist P
(let (a, _, _) := X in a)
(let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
Projections of sig2
An element y of a subset {x:A | (P x) & (Q x)} is the triple of an a of type A, a of a proof h that a satisfies P, and a proof h' that a satisfies Q. Then (proj1_sig (sig_of_sig2 y)) is the witness a, (proj2_sig (sig_of_sig2 y)) is the proof of (P a), and (proj3_sig y) is the proof of (Q a).
Projections of sigT
An element x of a sigma-type {y:A & P y} is a dependent pair made of an a of type A and an h of type P a. Then, (projT1 x) is the first projection and (projT2 x) is the second projection, the type of which depends on the projT1.
Section Projections.
Variable A : Type.
Variable P : A -> Type.
Definition projT1 (x:sigT P) : A := match x with
| existT _ a _ => a
end.
Definition projT2 (x:sigT P) : P (projT1 x) :=
match x return P (projT1 x) with
| existT _ _ h => h
end.
Register projT1 as core.sigT.proj1.
Register projT2 as core.sigT.proj2.
End Projections.
Module SigTNotations.
Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ; '/ ' y )").
Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1").
Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2").
End SigTNotations.
Import SigTNotations.
sigT2 of a predicate can be projected to a sigT.
This allows projT1 and projT2 to be usable with sigT2.
The let statements occur in the body of the existT so that projT1 of a coerced X : sigT2 P Q will unify with let (a, _, _) := X in a
Definition sigT_of_sigT2 (A : Type) (P Q : A -> Type) (X : sigT2 P Q) : sigT P
:= existT P
(let (a, _, _) := X in a)
(let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
Projections of sigT2
An element x of a sigma-type {y:A & P y & Q y} is a dependent pair made of an a of type A, an h of type P a, and an h' of type Q a. Then, (projT1 (sigT_of_sigT2 x)) is the first projection, (projT2 (sigT_of_sigT2 x)) is the second projection, and (projT3 x) is the third projection, the types of which depends on the projT1.
sigT of a predicate is equivalent to sig
sigT2 of a predicate is equivalent to sig2
sig of a predicate on Props can be turned into ex
sigT of a predicate on Props can be turned into ex
sig2 of a predicate on Props can be turned into ex2
sigT2 of a predicate on Props can be turned into ex2
η Principles
exists x : A, B is equivalent to inhabited {x : A | B}
Subtyping for prod
Equality of sigma types
Equality for sigT
Section sigT.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Equality of sigT is itself a sigT (forwards-reasoning version)
Equality of sigT is itself a sigT (backwards-reasoning version)
Curried version of proving equality of sigma types
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
Equality of sigT when the property is an hProp
Equivalence of equality of sigT with a sigT of equality We could actually prove an isomorphism here, and not just <->, but for simplicity, we don't.
Induction principle for @eq (sigT _)
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
We want uncurried versions so inversion_sigma can accept intropatterns, but we use ex types for the induction hypothesis to avoid extraction errors about informative inductive types having Prop instances
Equivalence of equality of sigT involving hProps with equality of the first components
Non-dependent classification of equality of sigT
Classification of transporting across an equality of sigTs
Equality for sig
Section sig.
We define this as a Let rather than a Definition to avoid extraction errors about informative inductive types having Prop instances
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Equality of sig is itself a sig (forwards-reasoning version)
Equality of sig is itself a sig (backwards-reasoning version)
Curried version of proving equality of sigma types
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
Induction principle for @eq (sig _)
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
We want uncurried versions so inversion_sigma can accept intropatterns, but we use ex types for the induction hypothesis to avoid extraction errors about informative inductive types having Prop instances
Equality of sig when the property is an hProp
Equivalence of equality of sig with a sig of equality We could actually prove an isomorphism here, and not just <->, but for simplicity, we don't.
Equivalence of equality of sig involving hProps with equality of the first components
Equality for sigT2
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Projecting an equality of a pair to equality of the third components
Equality of sigT2 is itself a sigT2 (forwards-reasoning version)
Equality of sigT2 is itself a sigT2 (backwards-reasoning version)
Curried version of proving equality of sigma types
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
Equality of sigT2 when the second property is an hProp
Equivalence of equality of sigT2 with a sigT2 of equality We could actually prove an isomorphism here, and not just <->, but for simplicity, we don't.
Induction principle for @eq (sigT2 _ _)
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
We want uncurried versions so inversion_sigma can accept intropatterns, but we use ex2 types for the induction hypothesis to avoid extraction errors about informative inductive types having Prop instances
Equivalence of equality of sigT2 involving hProps with equality of the first components
Non-dependent classification of equality of sigT
Classification of transporting across an equality of sigT2s
Equality for sig2
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Projecting an equality of a pair to equality of the third components
Equality of sig2 is itself a sig2 (fowards-reasoning version)
Equality of sig2 is itself a sig2 (backwards-reasoning version)
Curried version of proving equality of sigma types
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
Equality of sig2 when the second property is an hProp
Equivalence of equality of sig2 with a sig2 of equality We could actually prove an isomorphism here, and not just <->, but for simplicity, we don't.
Induction principle for @eq (sig2 _ _)
In order to have a performant inversion_sigma, we define specialized versions for when we have constructors on one or both sides of the equality
We want uncurried versions so inversion_sigma can accept intropatterns, but we use ex2 types for the induction hypothesis to avoid extraction errors about informative inductive types having Prop instances
Equivalence of equality of sig2 involving hProps with equality of the first components
Non-dependent classification of equality of sig
Classification of transporting across an equality of sig2s
sumbool is a boolean type equipped with the justification of their value
Inductive sumbool (A B:Prop) : Set :=
| left : A -> {A} + {B}
| right : B -> {A} + {B}
where "{ A } + { B }" := (sumbool A B) : type_scope.
Add Printing If sumbool.
Arguments left {A B} _, [A] B _.
Arguments right {A B} _ , A [B] _.
Register sumbool as core.sumbool.type.
sumor is an option type equipped with the justification of why it may not be a regular value
#[universes(template)]
Inductive sumor (A:Type) (B:Prop) : Type :=
| inleft : A -> A + {B}
| inright : B -> A + {B}
where "A + { B }" := (sumor A B) : type_scope.
Add Printing If sumor.
Arguments inleft {A B} _ , [A] B _.
Arguments inright {A B} _ , A [B] _.
Various forms of the axiom of choice for specifications
A result of type (Exc A) is either a normal value of type A or an error :
Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A).
It is implemented using the option type.
Section Exc.
Variable A : Type.
Definition Exc := option A.
Definition value := @Some A.
Definition error := @None A.
End Exc.
Arguments error {A}.
Definition except := False_rec.
Arguments except [P] _.
Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
#[global]
Hint Resolve left right inleft inright: core.
#[global]
Hint Resolve exist exist2 existT existT2: core.