diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Init/Specif.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Init/Specif.v')
-rw-r--r-- | theories/Init/Specif.v | 123 |
1 files changed, 100 insertions, 23 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index cc5a1932..1384901b 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -45,11 +45,11 @@ Arguments sigT2 (A P Q)%type. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope. -Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. -Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. Add Printing Let sig. @@ -65,24 +65,57 @@ Add Printing Let sigT2. [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the proof of [(P a)] *) - +(* Set Universe Polymorphism. *) Section Subset_projections. Variable A : Type. Variable P : A -> Prop. Definition proj1_sig (e:sig P) := match e with - | exist a b => a + | exist _ a b => a end. Definition proj2_sig (e:sig P) := match e return P (proj1_sig e) with - | exist a b => b + | exist _ a b => b end. 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)]. *) + +Section Subset_projections2. + + Variable A : Type. + Variables P Q : A -> Prop. + + Definition proj3_sig (e : sig2 P Q) := + let (a, b, c) return Q (proj1_sig (sig_of_sig2 e)) := e in c. + +End Subset_projections2. + + (** Projections of [sigT] An element [x] of a sigma-type [{y:A & P y}] is a dependent pair @@ -90,31 +123,71 @@ End Subset_projections. [(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 + | existT _ a _ => a end. + Definition projT2 (x:sigT P) : P (projT1 x) := match x return P (projT1 x) with - | existT _ h => h + | existT _ _ h => h end. End Projections. +(** [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]. *) + +Section Projections2. + + Variable A : Type. + Variables P Q : A -> Type. + + Definition projT3 (e : sigT2 P Q) := + let (a, b, c) return Q (projT1 (sigT_of_sigT2 e)) := e in c. + +End Projections2. + (** [sigT] of a predicate is equivalent to [sig] *) -Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P. -Proof. destruct 1 as (x,H); exists x; trivial. Defined. +Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P + := exist P (projT1 X) (projT2 X). + +Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P + := existT P (proj1_sig X) (proj2_sig X). -Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P. -Proof. destruct 1 as (x,H); exists x; trivial. Defined. +(** [sigT2] of a predicate is equivalent to [sig2] *) -Coercion sigT_of_sig : sig >-> sigT. -Coercion sig_of_sigT : sigT >-> sig. +Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q + := exist2 P Q (projT1 (sigT_of_sigT2 X)) (projT2 (sigT_of_sigT2 X)) (projT3 X). + +Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q + := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). (** [sumbool] is a boolean type equipped with the justification of their value *) @@ -142,6 +215,8 @@ Add Printing If sumor. Arguments inleft {A B} _ , [A] B _. Arguments inright {A B} _ , A [B] _. +(* Unset Universe Polymorphism. *) + (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. @@ -187,10 +262,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. @@ -203,12 +278,14 @@ End Dependent_choice_lemmas. [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. -Definition value := Some. -Definition error := @None. - -Arguments error [A]. + Definition Exc := option A. + Definition value := @Some A. + Definition error := @None A. +End Exc. +Arguments error {A}. Definition except := False_rec. (* for compatibility with previous versions *) |