From 62810c3e490549c15986e2347a1ba45c1d17b162 Mon Sep 17 00:00:00 2001 From: "Daniel R. Grayson" Date: Fri, 24 Jun 2011 09:37:13 +0200 Subject: [PATCH] replace (S 0) by 1, etc.; fix Makefile so TAGS file is in correct order --- Main_Library/Generalities/uu1uu0.v | 4 +-- Main_Library/hlevel1/hProp.v | 2 +- Main_Library/hlevel1/hProp_up.v | 2 +- Main_Library/hlevel2/finite_sets.v | 32 +++++++++++------------ Main_Library/hlevel2/set_quotients_r_up.v | 2 +- Makefile | 29 ++++++++++---------- 6 files changed, 36 insertions(+), 35 deletions(-) diff --git a/Main_Library/Generalities/uu1uu0.v b/Main_Library/Generalities/uu1uu0.v index 96e5f66..7f571e3 100644 --- a/Main_Library/Generalities/uu1uu0.v +++ b/Main_Library/Generalities/uu1uu0.v @@ -74,11 +74,11 @@ assert (s: uu1.isofhlevel n (paths _ x x')). apply (IHn _ (X0 x x')). apply (uu1 Coercion u0isofhleveltou1isofhlevel: isofhlevel >-> uu1.isofhlevel. -Definition u0isaproptou1isaprop (X : UU0) := u0isofhleveltou1isofhlevel (S O) X : isaprop X -> uu1.isaprop X. +Definition u0isaproptou1isaprop (X : UU0) := u0isofhleveltou1isofhlevel 1 X : isaprop X -> uu1.isaprop X. Coercion u0isaproptou1isaprop : isaprop >-> uu1.isaprop. -Definition u1isaproptou0isaprop (X : UU0) := u1isofhleveltou0isofhlevel (S O) X : uu1.isaprop X -> isaprop X. +Definition u1isaproptou0isaprop (X : UU0) := u1isofhleveltou0isofhlevel 1 X : uu1.isaprop X -> isaprop X. Coercion u1isaproptou0isaprop : uu1.isaprop >-> isaprop. diff --git a/Main_Library/hlevel1/hProp.v b/Main_Library/hlevel1/hProp.v index 762f213..7120a20 100644 --- a/Main_Library/hlevel1/hProp.v +++ b/Main_Library/hlevel1/hProp.v @@ -88,7 +88,7 @@ Definition hfalse : hProp := hProppair empty isapropempty. Canonical Structure hfalse. -Definition hconj (P Q : hProp) : hProp := hProppair (dirprod P Q) (isofhleveldirprod (S O) _ _ (uu1.pr22 _ _ P) (uu1.pr22 _ _ Q)). +Definition hconj (P Q : hProp) : hProp := hProppair (dirprod P Q) (isofhleveldirprod 1 _ _ (uu1.pr22 _ _ P) (uu1.pr22 _ _ Q)). Canonical Structure hconj. Definition uu1hdisj (P Q : hProp) := ishinh (coprod P Q). diff --git a/Main_Library/hlevel1/hProp_up.v b/Main_Library/hlevel1/hProp_up.v index 902e726..c3c7f72 100644 --- a/Main_Library/hlevel1/hProp_up.v +++ b/Main_Library/hlevel1/hProp_up.v @@ -54,7 +54,7 @@ set (is2:= uu1.gradth _ _ _ _ egf efg). apply ( uu1.isweqtotaltofib _ P1 P2 (fun XY: uu1.dirprod hProp hProp => (match XY with uu1.tpair X Y => eqweqmaphProp X Y end)) is2 ( uu1.dirprodpair _ _ P P')). Defined. Corollary uu1isasethProp : uu1.isaset hProp. -Proof. unfold isaset. simpl. intro. intro. apply (uu1.isofhlevelweqb (S O) _ _ _ (univfromtwoaxiomshProp x x') (uu1.isapropweq x x' (uu1.pr22 _ _ x'))). Defined. +Proof. unfold isaset. simpl. intro. intro. apply (uu1.isofhlevelweqb 1 _ _ _ (univfromtwoaxiomshProp x x') (uu1.isapropweq x x' (uu1.pr22 _ _ x'))). Defined. diff --git a/Main_Library/hlevel2/finite_sets.v b/Main_Library/hlevel2/finite_sets.v index 140333f..6d646a6 100644 --- a/Main_Library/hlevel2/finite_sets.v +++ b/Main_Library/hlevel2/finite_sets.v @@ -120,14 +120,14 @@ Proof. intros X X0. apply (hinhpr _ (weqinv _ _ (weqpair _ _ _ (isweqtoempty _ X Corollary isof0elempty: isofnel O empty. Proof. apply (isof0elb empty (fun x:_ => x)). Defined. -Lemma isof1ela (X:UU0): isofnel (S O) X -> iscontr X. -Proof. intros X X0. apply (isofnelimpl (S O) X X0 (iscontr_hprop X)). set (w2:= (weqinv _ _ (weqfromcoprodwithempty unit))). intro X1. set (w3:= weqcomp _ _ _ w2 X1). apply (iscontrifweqtounit _ (weqinv _ _ w3)). assumption. Defined. +Lemma isof1ela (X:UU0): isofnel 1 X -> iscontr X. +Proof. intros X X0. apply (isofnelimpl 1 X X0 (iscontr_hprop X)). set (w2:= (weqinv _ _ (weqfromcoprodwithempty unit))). intro X1. set (w3:= weqcomp _ _ _ w2 X1). apply (iscontrifweqtounit _ (weqinv _ _ w3)). assumption. Defined. -Lemma isof1elb (X:UU0): (iscontr X) -> isofnel (S O) X. +Lemma isof1elb (X:UU0): (iscontr X) -> isofnel 1 X. Proof. intros X X0. set (w1:= weqpair _ _ _ (isweqcontrtounit _ X0)). set (w2:= weqfromcoprodwithempty unit). set (w:= weqcomp _ _ _ w2 (weqinv _ _ w1)). apply (hinhpr _ w). Defined. -Lemma isof1elunit: isofnel (S O) unit. +Lemma isof1elunit: isofnel 1 unit. Proof. apply (hinhpr _ (weqfromcoprodwithempty unit)). Defined. @@ -140,8 +140,8 @@ Lemma isofnelweqf (n:nat)(X Y:UU0)(f:X -> Y)(is: isweq _ _ f): isofnel n X -> is Proof. intros n X Y f is X0. set (ff:= fun u:weq (stn n) X => weqcomp _ _ _ u (weqpair _ _ f is)). apply (hinhfunct _ _ ff X0). Defined. -Lemma isof2elbool : isofnel (S (S O)) bool. -Proof. apply (isofnelweqf _ _ _ _ (pr22 _ _ boolascoprod) (isofsnel (S O) unit isof1elunit)). Defined. +Lemma isof2elbool : isofnel 2 bool. +Proof. apply (isofnelweqf _ _ _ _ (pr22 _ _ boolascoprod) (isofsnel 1 unit isof1elunit)). Defined. @@ -214,7 +214,7 @@ Defined. Definition weqtoinitintervalsn (n:nat) : weq (coprod (initinterval n) unit) (initinterval (S n)). Proof. intro. set (f:= toinitintervalsn n). set (g:= frominitintervalsn n). split with f. -set (u:= coprodf _ _ _ _ (initintervaltonat n) (fun t:unit => t)). assert (is: isincl _ _ u). apply (isofhlevelfcoprodf (S O) _ _ _ _ _ _ (isinclinitintervaltonat n) (isofhlevelfweq (S O) _ _ _ (idisweq unit))). +set (u:= coprodf _ _ _ _ (initintervaltonat n) (fun t:unit => t)). assert (is: isincl _ _ u). apply (isofhlevelfcoprodf 1 _ _ _ _ _ _ (isinclinitintervaltonat n) (isofhlevelfweq 1 _ _ _ (idisweq unit))). assert (egf: forall x:_, paths _ (g (f x)) x). intro. assert (egf0: paths _ (u (g (f x))) (u x)). destruct x. simpl. destruct i as [ t x ]. destruct t. simpl. apply idpath. simpl. destruct (isdeceqnat n t). simpl. induction p. apply (initmap _ (neglebsnn t x)). simpl. apply idpath. destruct u0. destruct n. apply idpath. simpl. destruct (isdeceqnat n n) as [|e]. apply idpath. apply (initmap _ (e (idpath _ _))). apply (invmaponpathsincl _ _ _ is _ _ egf0). assert (efg: forall x:_, paths _ (f (g x)) x). intro. @@ -264,7 +264,7 @@ Proof. assert (c1: decidable (paths _ t t0)). apply isdeceqnat. destruct c1. - apply (invmaponpathsincl (isfinite0 X) nat (pr21 _ _) (isofhlevelfpr21 (S O) _ _ (fun n:nat => isapropdneg (weq (stn n) X))) (tpair nat (fun n : nat => isofnel0 n X) t x0) (tpair nat (fun n : nat => isofnel0 n X) t0 x) p). + apply (invmaponpathsincl (isfinite0 X) nat (pr21 _ _) (isofhlevelfpr21 1 _ _ (fun n:nat => isapropdneg (weq (stn n) X))) (tpair nat (fun n : nat => isofnel0 n X) t x0) (tpair nat (fun n : nat => isofnel0 n X) t0 x) p). assert (is1: dneg (dirprod (weq (stn t0) X) (weq (stn t) X))). apply (dneganddnegimpldneg _ _ x x0). assert (is2: dneg (weq (stn t0) (stn t))). @@ -302,10 +302,10 @@ Definition isfinitestn (n:nat): isfinite (stn n) := hinhpr _ (finitestructstn n) Definition finitestructempty := finitestructpair _ O (idweq _). Definition isfiniteempty : isfinite empty := hinhpr _ finitestructempty. -Definition finitestructunit: finitestruct unit := finitestructpair _ (S O) (weqfromcoprodwithempty unit). +Definition finitestructunit: finitestruct unit := finitestructpair _ 1 (weqfromcoprodwithempty unit). Definition isfiniteunit : isfinite unit := hinhpr _ finitestructunit. -Definition finitestructbool := finitestructpair _ (S (S O)) (weqcomp _ _ _ (weqcoprodf _ _ _ _ (weqfromcoprodwithempty unit) (idweq unit)) boolascoprod). +Definition finitestructbool := finitestructpair _ 2 (weqcomp _ _ _ (weqcoprodf _ _ _ _ (weqfromcoprodwithempty unit) (idweq unit)) boolascoprod). Definition isfinitebool : isfinite bool := hinhpr _ finitestructbool. Definition finitestructinitinterval (n:nat) := finitestructpair _ (S n) (weqstntoinitinterval n). @@ -434,7 +434,7 @@ Proof. intros. *) -(*Eval compute in carddneg _ (isfinitedirprod _ _ (isfinitestn (S (S (S (S O))))) (isfinitestn (S (S (S O))))).*) +(*Eval compute in carddneg _ (isfinitedirprod _ _ (isfinitestn 4) (isfinitestn 3)).*) Eval compute in carddneg _ (isfiniteempty). @@ -456,7 +456,7 @@ Eval compute in carddneg _ (isfinitedirprod _ _ isfinitebool isfinitebool). Eval compute in carddneg _ (isfinitedirprod _ _ isfinitebool (isfinitedirprod _ _ isfinitebool isfinitebool)). -Eval compute in carddneg _ (isfinitecoprod _ _ (isfinitebool) (isfinitecomplement _ (ii1 _ _ (ii2 _ _ tt)) (isfinitestn (S (S (S O)))))). +Eval compute in carddneg _ (isfinitecoprod _ _ (isfinitebool) (isfinitecomplement _ (ii1 _ _ (ii2 _ _ tt)) (isfinitestn 3))). Eval lazy in carddneg _ (isfinitecomplement _ (ii1 _ _ tt) (isfinitecoprod _ _ (isfiniteunit) (isfinitebool))). @@ -465,7 +465,7 @@ Eval lazy in carddneg _ (isfinitecomplement _ (ii1 _ _ tt) (isfinitecoprod _ _ ( (*Eval compute in carddneg _ (isfinitecomplement _ (dirprodpair _ _ tt tt) (isfinitedirprod _ _ isfiniteunit isfiniteunit)).*) -(*Definition finitestructunit: finitestruct unit := finitestructpair _ (S O) (weqfromcoprodwithempty unit).*) +(*Definition finitestructunit: finitestruct unit := finitestructpair _ 1 (weqfromcoprodwithempty unit).*) Eval lazy in (pr21 _ _ (finitestructcomplement _ (dirprodpair _ _ tt tt) (finitestructdirprod _ _ (finitestructunit) (finitestructunit)))). @@ -483,16 +483,16 @@ Eval lazy in carddneg _ (isfinitecomplement _ (dirprodpair _ _ true (dirprodpair (* -Eval compute in (pr21 _ _ (isfinitedirprod _ _ (isfinitestn (S (S (S (S O))))) (isfinitestn (S (S (S O)))))). +Eval compute in (pr21 _ _ (isfinitedirprod _ _ (isfinitestn 4) (isfinitestn 3))). Print empty_rect. -Lemma isof1elfrom0el (X Y:UU0): isofnel O X -> isofnel (S O) (X -> Y). +Lemma isof1elfrom0el (X Y:UU0): isofnel O X -> isofnel 1 (X -> Y). Proof. intros. unfold isofnel. intro. simpl. Theorem isfinitefunctions (X Y:UU0)(isx: isfinite X)(isy: isfinite Y): isfinite (X -> Y). -Proof. intros. destruct isx. generalize Y isy X x. clear isy Y x X. induction t. intros. split with (S O). +Proof. intros. destruct isx. generalize Y isy X x. clear isy Y x X. induction t. intros. split with 1. diff --git a/Main_Library/hlevel2/set_quotients_r_up.v b/Main_Library/hlevel2/set_quotients_r_up.v index e9b287c..da08aef 100644 --- a/Main_Library/hlevel2/set_quotients_r_up.v +++ b/Main_Library/hlevel2/set_quotients_r_up.v @@ -102,7 +102,7 @@ set (r1:= pr21 _ _ (pr22 _ _ is)). unfold issymm in r1. set (ax := is1 x x' a). set (ax' := is1 x' x (r1 _ _ a)). set (f:= fun u: R x t => (r1 _ _ (ax (r1 _ _ u)))). set (g:= fun u: R x' t => (r1 _ _ (ax' (r1 _ _ u)))). apply (uahp _ _ f g). -set (is2:= isofhlevelfpr21 (S O) _ _ (fun A: hsubtypes X => (isapropiseqclass X R A))). +set (is2:= isofhlevelfpr21 1 _ _ (fun A: hsubtypes X => (isapropiseqclass X R A))). apply (invmaponpathsincl _ _ _ is2 _ _ e). Defined. (* Uses univalence for hProp *) diff --git a/Makefile b/Makefile index 114e602..f44860b 100644 --- a/Makefile +++ b/Makefile @@ -2,20 +2,20 @@ M=Main_Library P=Proof_of_Extensionality COQFLAGS = -opt -q -VFILES := \ - $M/Generalities/uu0.v \ - $M/Generalities/uu1.v \ - $M/Generalities/uu1uu0.v \ - $P/univ01.v \ - $M/hlevel1/hProp.v \ - $M/hlevel2/finite_sets.v \ - $M/hlevel1/hProp_up.v \ - $M/hlevel1/hProp_r.v \ - $M/hlevel1/hProp_r_up.v \ - $M/hlevel2/hSet_r.v \ - $M/hlevel2/hSet_r_up.v \ - $M/hlevel2/set_quotients_r_up.v \ - $M/hlevel2/set_quotients_constr2_r_up.v +VFILES := \ + $M/hlevel2/set_quotients_constr2_r_up.v \ + $M/hlevel2/set_quotients_r_up.v \ + $M/hlevel2/hSet_r_up.v \ + $M/hlevel2/hSet_r.v \ + $M/hlevel1/hProp_r_up.v \ + $M/hlevel1/hProp_r.v \ + $M/hlevel1/hProp_up.v \ + $M/hlevel2/finite_sets.v \ + $M/hlevel1/hProp.v \ + $P/univ01.v \ + $M/Generalities/uu1uu0.v \ + $M/Generalities/uu1.v \ + $M/Generalities/uu0.v VOFILES := $(VFILES:.v=.vo) MADE_FILES = %.glob %.vo: %.v @@ -46,6 +46,7 @@ $M/Generalities/uu1.v: $M/Generalities/uu0.v Makefile uu1.sed rm -f $@ sed <$< >$@ -f uu1.sed chmod a-w $@ +$M/Generalities/uu1.vo:| $M/Generalities/uu0.vo $P/univ01.vo $M/Generalities/uu1uu0.vo: $M/Generalities/uu0.vo $M/Generalities/uu1.vo clean: