| products/sources/formale Sprachen/VDM/VDMPP/MondexPP/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Specif.v Sprache: Unknown
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Basic specifications : sets that may contain logical information *) Set Implicit Arguments. Set Reversible Pattern Implicit. Require Import Notations. Require Import Datatypes. Require Import Logic. (** 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. (* Notations *) 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_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. 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 & P }" := (sigT (fun x => P)) : type_scope. 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. Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope. Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope. Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope. Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) : type_scope. Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope. Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) : 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)] *) (* 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 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)]. *) 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 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. Local Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ; '/ ' y )"). Local Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1"). Local Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2"). (** [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] *) 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). (** [sigT2] of a predicate is equivalent to [sig2] *) 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). (** η Principles *) Definition sigT_eta {A P} (p : { a : A & P a }) : p = existT _ (projT1 p) (projT2 p). Proof. destruct p; reflexivity. Defined. Definition sig_eta {A P} (p : { a : A | P a }) : p = exist _ (proj1_sig p) (proj2_sig p). Proof. destruct p; reflexivity. Defined. Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a }) : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p). Proof. destruct p; reflexivity. Defined. Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). Proof. destruct p; reflexivity. Defined. (** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *) Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}. Proof. intros [x y]. exact (inhabits (exist _ x y)). Qed. Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x. Proof. intros [[x y]];exists x;exact y. Qed. (** Equality of sigma types *) Import EqNotations. Local Notation "'rew' 'dependent' H 'in' H'" := (match H with | eq_refl => H' end) (at level 10, H' at level 10, format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). (** Equality for [sigT] *) Section sigT. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) : u.1 = v.1 := f_equal (fun x => x.1) p. (** Projecting an equality of a pair to equality of the second components *) Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v) : rew projT1_eq p in u.2 = v.2 := rew dependent p in eq_refl. (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *) Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 & rew p in u2 = v2 }) : (u1; u2) = (v1; v2). Proof. destruct pq as [p q]. destruct q; simpl in *. destruct p; reflexivity. Defined. (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *) Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a }) (pq : { p : u.1 = v.1 & rew p in u.2 = v.2 }) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. apply eq_existT_uncurried; exact pq. Defined. Lemma eq_existT_curried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (p : u1 = v1) (q : rew p in u2 = v2) : (u1; u2) = (v1; v2). Proof. destruct p, q. reflexivity. Defined. Local Notation "(= u ; v )" := (eq_existT_curried u v) (at level 0, format "(= u ; '/ ' v Lemma eq_existT_curried_map {A A' P P'} (f:A -> A') (g:forall u:A, P u -> P' (f u)) {u1 v1 : A} {u2 : P u1} {v2 : P v1} (p : u1 = v1) (q : rew p in u2 = v2) : f_equal (fun x => (f x.1; g x.1 x.2)) (= p; q) = (= f_equal f p; f_equal_dep2 f g p q). Proof. destruct p, q. reflexivity. Defined. Lemma eq_existT_curried_trans {A P} {u1 v1 w1 : A} {u2 : P u1} {v2 : P v1} {w2 : P w1} (p : u1 = v1) (q : rew p in u2 = v2) (p' : v1 = w1) (q': rew p' in v2 = w2) : eq_trans (= p; q) (= p'; q') = (= eq_trans p p'; eq_trans_map p p' q q'). Proof. destruct p', q'. reflexivity. Defined. Theorem eq_existT_curried_congr {A P} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {p p' : u1 = v1} {q : rew p in u2 = v2} {q': rew p' in u2 = v2} (r : p = p') : rew [fun H => rew H in u2 = v2] r in q = q' -> (= p; q) = (= p'; q'). Proof. destruct r, 1. reflexivity. Qed. (** Curried version of proving equality of sigma types *) Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a }) (p : u.1 = v.1) (q : rew p in u.2 = v.2) : u = v := eq_sigT_uncurried u v (existT _ p q). (** Equality of [sigT] when the property is an hProp *) Definition eq_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A & P a }) (p : u.1 = v.1) : u = v := eq_sigT u v p (P_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. *) Definition eq_sigT_uncurried_iff {A P} (u v : { a : A & P a }) : u = v <-> { p : u.1 = v.1 & rew p in u.2 = v.2 }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ]. Defined. (** Induction principle for [@eq (sigT _)] *) Definition eq_sigT_rect {A P} {u v : { a : A & P a }} (Q : u = v -> Type) (f : forall p q, Q (eq_sigT u v p q)) : forall p, Q p. Proof. intro p; specialize (f (projT1_eq p) (projT2_eq p)); destruct u, p; exact f. Defined. Definition eq_sigT_rec {A P u v} (Q : u = v :> { a : A & P a } -> Set) := eq_sigT_rect Q. Definition eq_sigT_ind {A P u v} (Q : u = v :> { a : A & P a } -> Prop) := eq_sigT_rec Q. (** Equivalence of equality of [sigT] involving hProps with equality of the first components * Definition eq_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A & P a }) : u = v <-> (u.1 = v.1) := conj (fun p => f_equal (@projT1 _ _) p) (eq_sigT_hprop P_hprop u v). (** Non-dependent classification of equality of [sigT] *) Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B }) (p : u.1 = v.1) (q : u.2 = v.2) : u = v := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q). (** Classification of transporting across an equality of [sigT]s *) Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x & Q x p }) {y} (H : x = y) : rew [fun a => { p : P a & Q a p }] H in u = existT (Q y) (rew H in u.1) (rew dependent H in (u.2)). Proof. destruct H, u; reflexivity. Defined. End sigT. (** Equality for [sig] *) Section sig. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) Definition proj1_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) : proj1_sig u = proj1_sig v := f_equal (@proj1_sig _ _) p. (** Projecting an equality of a pair to equality of the second components *) Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v) : rew proj1_sig_eq p in proj2_sig u = proj2_sig v := rew dependent p in eq_refl. (** Equality of [sig] is itself a [sig] (forwards-reasoning version) *) Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (pq : { p : u1 = v1 | rew p in u2 = v2 }) : exist _ u1 u2 = exist _ v1 v2. Proof. destruct pq as [p q]. destruct q; simpl in *. destruct p; reflexivity. Defined. (** Equality of [sig] is itself a [sig] (backwards-reasoning version) *) Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. apply eq_exist_uncurried; exact pq. Defined. (** Curried version of proving equality of sigma types *) Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a }) (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) : u = v := eq_sig_uncurried u v (exist _ p q). (** Induction principle for [@eq (sig _)] *) Definition eq_sig_rect {A P} {u v : { a : A | P a }} (Q : u = v -> Type) (f : forall p q, Q (eq_sig u v p q)) : forall p, Q p. Proof. intro p; specialize (f (proj1_sig_eq p) (proj2_sig_eq p)); destruct u, p; exact f. Defi Definition eq_sig_rec {A P u v} (Q : u = v :> { a : A | P a } -> Set) := eq_sig_rect Q. Definition eq_sig_ind {A P u v} (Q : u = v :> { a : A | P a } -> Prop) := eq_sig_rec Q. (** Equality of [sig] when the property is an hProp *) Definition eq_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A | P a }) (p : proj1_sig u = proj1_sig v) : u = v := eq_sig u v p (P_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. *) Definition eq_sig_uncurried_iff {A} {P : A -> Prop} (u v : { a : A | P a }) : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ]. Defined. (** Equivalence of equality of [sig] involving hProps with equality of the first components *) Definition eq_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q) (u v : { a : A | P a }) : u = v <-> (proj1_sig u = proj1_sig v) := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v). Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x | Q x p }) {y} (H : x = y) : rew [fun a => { p : P a | Q a p }] H in u = exist (Q y) (rew H in proj1_sig u) (rew dependent H in proj2_sig u). Proof. destruct H, u; reflexivity. Defined. End sig. (** Equality for [sigT] *) Section sigT2. (* We make [sigT_of_sigT2] a coercion so we can use [projT1], [projT2] on [sigT2] *) Local Coercion sigT_of_sigT2 : sigT2 >-> sigT. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) Definition sigT_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : u = v :> { a : A & P a } := f_equal _ p. Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : u.1 = v.1 := projT1_eq (sigT_of_sigT2_eq p). (** Projecting an equality of a pair to equality of the second components *) Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : rew projT1_of_sigT2_eq p in u.2 = v.2 := rew dependent p in eq_refl. (** Projecting an equality of a pair to equality of the third components *) Definition projT3_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v) : rew projT1_of_sigT2_eq p in projT3 u = projT3 v := rew dependent p in eq_refl. (** Equality of [sigT2] is itself a [sigT2] (forwards-reasoning version) *) Definition eq_existT2_uncurried {A : Type} {P Q : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} (pqr : { p : u1 = v1 & rew p in u2 = v2 & rew p in u3 = v3 }) : existT2 _ _ u1 u2 u3 = existT2 _ _ v1 v2 v3. Proof. destruct pqr as [p q r]. destruct r, q, p; simpl. reflexivity. Defined. (** Equality of [sigT2] is itself a [sigT2] (backwards-reasoning version) *) Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (pqr : { p : u.1 = v.1 & rew p in u.2 = v.2 & rew p in projT3 u = projT3 v }) : u = v. Proof. destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. apply eq_existT2_uncurried; exact pqr. Defined. (** Curried version of proving equality of sigma types *) Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a }) (p : u.1 = v.1) (q : rew p in u.2 = v.2) (r : rew p in projT3 u = projT3 v) : u = v := eq_sigT2_uncurried u v (existT2 _ _ p q r). (** Equality of [sigT2] when the second property is an hProp *) Definition eq_sigT2_hprop {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q) (u v : { a : A & P a & Q a }) (p : u = v :> { a : A & P a }) : u = v := eq_sigT2 u v (projT1_eq p) (projT2_eq p) (Q_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. *) Definition eq_sigT2_uncurried_iff {A P Q} (u v : { a : A & P a & Q a }) : u = v <-> { p : u.1 = v.1 & rew p in u.2 = v.2 & rew p in projT3 u = projT3 v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ]. Defined. (** Induction principle for [@eq (sigT2 _ _)] *) Definition eq_sigT2_rect {A P Q} {u v : { a : A & P a & Q a }} (R : u = v -> Type) (f : forall p q r, R (eq_sigT2 u v p q r)) : forall p, R p. Proof. intro p. specialize (f (projT1_of_sigT2_eq p) (projT2_of_sigT2_eq p) (projT3_eq p)). destruct u, p; exact f. Defined. Definition eq_sigT2_rec {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Set) := eq_sigT2_rect R. Definition eq_sigT2_ind {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Prop) := eq_sigT2_rec R. (** Equivalence of equality of [sigT2] involving hProps with equality of the first components Definition eq_sigT2_hprop_iff {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q) (u v : { a : A & P a & Q a }) : u = v <-> (u = v :> { a : A & P a }) := conj (fun p => f_equal (@sigT_of_sigT2 _ _ _) p) (eq_sigT2_hprop Q_hprop u v). (** Non-dependent classification of equality of [sigT] *) Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C }) (p : u.1 = v.1) (q : u.2 = v.2) (r : projT3 u = projT3 v) : u = v := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sigT2]s *) Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : { p : P x & Q x p & R x p }) {y} (H : x = y) : rew [fun a => { p : P a & Q a p & R a p }] H in u = existT2 (Q y) (R y) (rew H in u.1) (rew dependent H in u.2) (rew dependent H in projT3 u). Proof. destruct H, u; reflexivity. Defined. End sigT2. (** Equality for [sig2] *) Section sig2. (* We make [sig_of_sig2] a coercion so we can use [proj1], [proj2] on [sig2] *) Local Coercion sig_of_sig2 : sig2 >-> sig. Local Unset Implicit Arguments. (** Projecting an equality of a pair to equality of the first components *) Definition sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : u = v :> { a : A | P a } := f_equal _ p. Definition proj1_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : proj1_sig u = proj1_sig v := proj1_sig_eq (sig_of_sig2_eq p). (** Projecting an equality of a pair to equality of the second components *) Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v := rew dependent p in eq_refl. (** Projecting an equality of a pair to equality of the third components *) Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v := rew dependent p in eq_refl. (** Equality of [sig2] is itself a [sig2] (fowards-reasoning version) *) Definition eq_exist2_uncurried {A} {P Q : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1} (pqr : { p : u1 = v1 | rew p in u2 = v2 & rew p in u3 = v3 }) : exist2 _ _ u1 u2 u3 = exist2 _ _ v1 v2 v3. Proof. destruct pqr as [p q r]. destruct r, q, p; simpl. reflexivity. Defined. (** Equality of [sig2] is itself a [sig2] (backwards-reasoning version) *) Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (pqr : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }) : u = v. Proof. destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *. apply eq_exist2_uncurried; exact pqr. Defined. (** Curried version of proving equality of sigma types *) Definition eq_sig2 {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) (r : rew p in proj3_sig u = proj3_sig v) : u = v := eq_sig2_uncurried u v (exist2 _ _ p q r). (** Equality of [sig2] when the second property is an hProp *) Definition eq_sig2_hprop {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) (u v : { a : A | P a & Q a }) (p : u = v :> { a : A | P a }) : u = v := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_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. *) Definition eq_sig2_uncurried_iff {A P Q} (u v : { a : A | P a & Q a }) : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig2_uncurried ]. Defined. (** Induction principle for [@eq (sig2 _ _)] *) Definition eq_sig2_rect {A P Q} {u v : { a : A | P a & Q a }} (R : u = v -> Type) (f : forall p q r, R (eq_sig2 u v p q r)) : forall p, R p. Proof. intro p. specialize (f (proj1_sig_of_sig2_eq p) (proj2_sig_of_sig2_eq p) (proj3_sig_eq p)). destruct u, p; exact f. Defined. Definition eq_sig2_rec {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Set) := eq_sig2_rect R. Definition eq_sig2_ind {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Prop) := eq_sig2_rec R. (** Equivalence of equality of [sig2] involving hProps with equality of the first components * Definition eq_sig2_hprop_iff {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q) (u v : { a : A | P a & Q a }) : u = v <-> (u = v :> { a : A | P a }) := conj (fun p => f_equal (@sig_of_sig2 _ _ _) p) (eq_sig2_hprop Q_hprop u v). (** Non-dependent classification of equality of [sig] *) Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C)) (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v) : u = v := @eq_sig2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r). (** Classification of transporting across an equality of [sig2]s *) Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : { p : P x | Q x p & R x p }) {y} (H : x = y) : rew [fun a => { p : P a | Q a p & R a p }] H in u = exist2 (Q y) (R y) (rew H in proj1_sig u) (rew dependent H in proj2_sig u) (rew dependent H in proj3_sig u). Proof. destruct H, u; reflexivity. Defined. End sig2. (** [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] _. (* Unset Universe Polymorphism. *) (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. Variables S S' : Set. Variable R : S -> S' -> Prop. Variable R' : S -> S' -> Set. Variables R1 R2 : S -> Prop. Lemma Choice : (forall x:S, {y:S' | R x y}) -> {f:S -> S' | forall z:S, R z (f z)}. Proof. intro H. exists (fun z => proj1_sig (H z)). intro z; destruct (H z); assumption. Defined. Lemma Choice2 : (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}. Proof. intro H. exists (fun z => projT1 (H z)). intro z; destruct (H z); assumption. Defined. Lemma bool_choice : (forall x:S, {R1 x} + {R2 x}) -> {f:S -> bool | forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}. Proof. intro H. exists (fun z:S => if H z then true else false). intro z; destruct (H z); auto. Defined. End Choice_lemmas. Section Dependent_choice_lemmas. Variable X : Set. Variable R : X -> X -> Prop. Lemma dependent_choice : (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. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. split. - reflexivity. - induction n; simpl; apply proj2_sig. Defined. End Dependent_choice_lemmas. (** 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. (* for compatibility with previous versions *) Arguments except [P] _. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Proof. intros A C h1 h2. apply False_rec. apply (h2 h1). Defined. Hint Resolve left right inleft inright: core. Hint Resolve exist exist2 existT existT2: core. [ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ] |