./._Pelayo-Coq000777 000765 000024 00000000324 12404034066 013741 0ustar00nicolastaff000000 000000 Mac OS X  2¢ÔATTRÔ˜<˜<com.apple.quarantineq/0042;00000000;Safari;5085629F-B604-4322-A539-1F4796CB8AB1Pelayo-Coq/000777 000765 000024 00000000000 12404034066 013442 5ustar00nicolastaff000000 000000 Pelayo-Coq/._fps.v000777 000765 000024 00000000324 12104265162 014640 0ustar00nicolastaff000000 000000 Mac OS X  2¢ÔATTRÔ˜<˜<com.apple.quarantineq/0002;53a854a1;Safari;5085629F-B604-4322-A539-1F4796CB8AB1Pelayo-Coq/fps.v000777 000765 000024 00000154427 12104265162 014441 0ustar00nicolastaff000000 000000 (** *Formal Power Series *) (** By Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren *) (** January 2011 *) (** Settings *) Add Rec LoadPath "../Generalities". Add Rec LoadPath "../hlevel1". Add Rec LoadPath "../hlevel2". Add Rec LoadPath "../Proof_of_Extensionality". Add Rec LoadPath "../Algebra". Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *) (** Imports *) Require Export lemmas. (** ** I. Summation in a commutative ring *) Open Scope rng_scope. Definition natsummation0 { R : commrng } ( upper : nat ) ( f : nat -> R ) : R. Proof. intro R. intro upper. induction upper. intros. exact ( f 0%nat ). intros. exact ( ( IHupper f + ( f ( S upper ) ) ) ). Defined. Lemma natsummationpaths { R : commrng } { upper upper' : nat } ( u : upper ~> upper' ) ( f : nat -> R ) : natsummation0 upper f ~> natsummation0 upper' f. Proof. intros. destruct u. auto. Defined. Lemma natsummationpathsupperfixed { R : commrng } { upper : nat } ( f f' : nat -> R ) ( p : forall x : nat, natleh x upper -> f x ~> f' x ) : natsummation0 upper f ~> natsummation0 upper f'. Proof. intros R upper. induction upper. intros f f' p. simpl. apply p. apply isreflnatleh. intros. simpl. rewrite ( IHupper f f' ). rewrite ( p ( S upper ) ). apply idpath. apply isreflnatleh. intros x p'. apply p. apply ( istransnatleh _ upper ). assumption. apply natlthtoleh. apply natlthnsn. Defined. (* Here we consider summation of functions which are, in a fixed interval, 0 for all but either the first or last value. *) Lemma natsummationae0bottom { R : commrng } { f : nat -> R } ( upper : nat ) ( p : forall x : nat, natlth 0 x -> f x ~> 0 ) : natsummation0 upper f ~> ( f 0%nat ). Proof. intros R f upper. induction upper. auto. intro p. simpl. rewrite ( IHupper ). rewrite ( p ( S upper ) ). rewrite ( rngrunax1 R ). apply idpath. apply ( natlehlthtrans _ upper _ ). apply natleh0n. apply natlthnsn. assumption. Defined. Lemma natsummationae0top { R : commrng } { f : nat -> R } ( upper : nat ) ( p : forall x : nat, natlth x upper -> f x ~> 0 ) : natsummation0 upper f ~> ( f upper ). Proof. intros R f upper. induction upper. auto. intro p. assert ( natsummation0 upper f ~> ( natsummation0 ( R := R ) upper ( fun x : nat => 0 ) ) ) as g. apply natsummationpathsupperfixed. intros m q. apply p. exact ( natlehlthtrans m upper ( S upper ) q ( natlthnsn upper ) ). simpl. rewrite g. assert ( natsummation0 ( R := R ) upper ( fun _ : nat => 0 ) ~> 0 ) as g'. set ( g'' := fun x : nat => rngunel1 ( X := R ) ). assert ( forall x : nat, natlth 0 x -> g'' x ~> 0 ) as q0. intro k. intro pp. auto. exact ( natsummationae0bottom upper q0 ). rewrite g'. rewrite ( rnglunax1 R ). apply idpath. Defined. Lemma natsummationshift0 { R : commrng } ( upper : nat ) ( f : nat -> R ) : natsummation0 ( S upper ) f ~> ( natsummation0 upper ( fun x : nat => f ( S x ) ) + f 0%nat ). Proof. intros R upper. induction upper. intros f. simpl. apply R. intros. change ( natsummation0 ( S upper ) f + f ( S ( S upper ) ) ~> ( natsummation0 upper ( fun x : nat => f ( S x ) ) + f ( S ( S upper ) ) + f 0%nat ) ). rewrite IHupper. rewrite 2! ( rngassoc1 R ). rewrite ( rngcomm1 R ( f 0%nat ) _ ). apply idpath. Defined. Lemma natsummationshift { R : commrng } ( upper : nat ) ( f : nat -> R ) { i : nat } ( p : natleh i upper ) : natsummation0 ( S upper ) f ~> ( natsummation0 upper ( funcomp ( natcoface i ) f ) + f i ). Proof. intros R upper. induction upper. intros f i p. destruct i. unfold funcomp. apply R. assert empty. exact ( negnatlehsn0 i p ). contradiction. intros f i p. destruct i. apply natsummationshift0. destruct ( natlehchoice ( S i ) ( S upper ) p ) as [ h | k ]. change ( natsummation0 ( S upper ) f + f ( S ( S upper ) ) ~> ( natsummation0 ( S upper ) ( funcomp ( natcoface ( S i ) ) f ) + f ( S i ) ) ). rewrite ( IHupper f ( S i ) ). simpl. unfold funcomp at 3. unfold natcoface at 3. rewrite 2! ( rngassoc1 R ). rewrite ( rngcomm1 R _ ( f ( S i ) ) ). simpl. rewrite ( natgehimplnatgtbfalse i upper ). apply idpath. apply p. apply natlthsntoleh. assumption. simpl. assert ( natsummation0 upper ( funcomp ( natcoface ( S i ) ) f ) ~> natsummation0 upper f ) as h. apply natsummationpathsupperfixed. intros m q. unfold funcomp. unfold natcoface. assert ( natlth m ( S i ) ) as q'. apply ( natlehlthtrans _ upper ). assumption. rewrite k. apply natlthnsn. unfold natlth in q'. rewrite q'. apply idpath. rewrite <- h. unfold funcomp, natcoface at 3. simpl. rewrite ( natgehimplnatgtbfalse i upper ). rewrite 2! ( rngassoc1 R ). rewrite ( rngcomm1 R ( f ( S ( S upper ) ) ) ). rewrite k. apply idpath. apply p. Defined. Lemma natsummationplusdistr { R : commrng } ( upper : nat ) ( f g : nat -> R ) : natsummation0 upper ( fun x : nat => f x + g x ) ~> ( ( natsummation0 upper f ) + ( natsummation0 upper g ) ). Proof. intros R upper. induction upper. auto. intros f g. simpl. rewrite <- ( rngassoc1 R _ ( natsummation0 upper g ) _ ). rewrite ( rngassoc1 R ( natsummation0 upper f ) ). rewrite ( rngcomm1 R _ ( natsummation0 upper g ) ). rewrite <- ( rngassoc1 R ( natsummation0 upper f ) ). rewrite <- ( IHupper f g ). rewrite ( rngassoc1 R ). apply idpath. Defined. Lemma natsummationtimesdistr { R : commrng } ( upper : nat ) ( f : nat -> R ) ( k : R ) : k * ( natsummation0 upper f ) ~> ( natsummation0 upper ( fun x : nat => k * f x ) ). Proof. intros R upper. induction upper. auto. intros f k. simpl. rewrite <- ( IHupper ). rewrite <- ( rngldistr R ). apply idpath. Defined. Lemma natsummationtimesdistl { R : commrng } ( upper : nat ) ( f : nat -> R ) ( k : R ) : ( natsummation0 upper f ) * k ~> ( natsummation0 upper ( fun x : nat => f x * k ) ). Proof. intros R upper. induction upper. auto. intros f k. simpl. rewrite <- IHupper. rewrite ( rngrdistr R ). apply idpath. Defined. Lemma natsummationsswapminus { R : commrng } { upper n : nat } ( f : nat -> R ) ( q : natleh n upper ) : natsummation0 ( S ( minus upper n ) ) f ~> natsummation0 ( minus ( S upper ) n ) f. Proof. intros R upper. induction upper. intros n f q. destruct n. auto. assert empty. exact ( negnatlehsn0 n q ). contradiction. intros n f q. destruct n. auto. change ( natsummation0 ( S ( minus upper n ) ) f ~> natsummation0 ( minus ( S upper ) n ) f ). apply IHupper. apply q. Defined. (** The following lemma asserts that $\sum^{n}_{k=0}\sum^{k}_{l=0}f(l,k-l)=\sum^{n}_{k=0}\sum^{n-k}_{l=0}f(k,l)$ *) Lemma natsummationswap { R : commrng } ( upper : nat ) ( f : nat -> nat -> R ) : natsummation0 upper ( fun i : nat => natsummation0 i ( fun j : nat => f j ( minus i j ) ) ) ~> ( natsummation0 upper ( fun k : nat => natsummation0 ( minus upper k ) ( fun l : nat => f k l ) ) ). Proof. intros R upper. induction upper. auto. intros f. change ( natsummation0 upper (fun i : nat => natsummation0 i (fun j : nat => f j ( minus i j))) + natsummation0 ( S upper ) ( fun j : nat => f j ( minus ( S upper ) j ) ) ~> ( natsummation0 upper (fun k : nat => natsummation0 (S upper - k) (fun l : nat => f k l)) + natsummation0 ( minus ( S upper ) ( S upper ) ) ( fun l : nat => f ( S upper ) l ) ) ). change ( natsummation0 upper (fun i : nat => natsummation0 i (fun j : nat => f j ( minus i j))) + ( natsummation0 upper ( fun j : nat => f j ( minus ( S upper ) j ) ) + f ( S upper ) ( minus ( S upper ) ( S upper ) ) ) ~> ( natsummation0 upper (fun k : nat => natsummation0 (S upper - k) (fun l : nat => f k l)) + natsummation0 ( minus ( S upper ) ( S upper ) ) ( fun l : nat => f ( S upper ) l ) ) ). assert ( (natsummation0 upper (fun k : nat => natsummation0 ( S ( minus upper k ) ) (fun l : nat => f k l)) ) ~> (natsummation0 upper (fun k : nat => natsummation0 (minus ( S upper ) k) (fun l : nat => f k l)) ) ) as A. apply natsummationpathsupperfixed. intros n q. apply natsummationsswapminus. exact q. rewrite <- A. change ( fun k : nat => natsummation0 (S ( minus upper k)) (fun l : nat => f k l) ) with ( fun k : nat => natsummation0 ( minus upper k ) ( fun l : nat => f k l ) + f k ( S ( minus upper k ) ) ). rewrite ( natsummationplusdistr upper _ ( fun k : nat => f k ( S ( minus upper k ) ) ) ). rewrite IHupper. rewrite minusnn0. rewrite ( rngassoc1 R). assert ( natsummation0 upper ( fun j : nat => f j ( minus ( S upper ) j ) ) ~> natsummation0 upper ( fun k : nat => f k ( S ( minus upper k ) ) ) ) as g. apply natsummationpathsupperfixed. intros m q. rewrite pathssminus. apply idpath. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. rewrite g. apply idpath. Defined. (** * II. Reindexing along functions i : nat -> nat which are automorphisms of the interval of summation.*) Definition isnattruncauto ( upper : nat ) ( i : nat -> nat ) := dirprod ( forall x : nat, natleh x upper -> total2 ( fun y : nat => dirprod ( natleh y upper ) ( dirprod ( i y ~> x ) ( forall z : nat, natleh z upper -> i z ~> x -> y ~> z ) ) ) ) ( forall x : nat, natleh x upper -> natleh ( i x ) upper ). Lemma nattruncautoisinj { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n m : nat } ( n' : natleh n upper ) ( m' : natleh m upper ) : i n ~> i m -> n ~> m. Proof. intros upper i p n m n' m' h. assert ( natleh ( i m ) upper ) as q. apply p. assumption. set ( x := pr1 p ( i m ) q ). set ( v := pr1 x ). set ( w := pr1 ( pr2 x ) ). set ( y := pr1 ( pr2 ( pr2 x ) ) ). change ( pr1 x ) with v in w, y. assert ( v ~> n ) as a. apply ( pr2 x ). assumption. assumption. rewrite <- a. apply ( pr2 x ). assumption. apply idpath. Defined. Definition nattruncautopreimage { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) : nat := pr1 ( pr1 p n n' ). Definition nattruncautopreimagepath { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) : i ( nattruncautopreimage p n' ) ~> n := ( pr1 ( pr2 ( pr2 ( pr1 p n n' ) ) ) ). Definition nattruncautopreimageineq { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) : natleh ( nattruncautopreimage p n' ) upper := ( ( pr1 ( pr2 ( pr1 p n n' ) ) ) ). Definition nattruncautopreimagecanon { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) { m : nat } ( m' : natleh m upper ) ( q : i m ~> n ) : nattruncautopreimage p n' ~> m := ( pr2 ( pr2 ( pr2 ( pr1 p n n' ) ) ) ) m m' q. Definition nattruncautoinv { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) : nat -> nat. Proof. intros upper i p n. destruct ( natgthorleh n upper ) as [ l | r ]. exact n. exact ( nattruncautopreimage p r ). Defined. Lemma nattruncautoinvisnattruncauto { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) : isnattruncauto upper ( nattruncautoinv p ). Proof. intros. split. intros n n'. split with ( i n ). split. apply p. assumption. split. unfold nattruncautoinv. destruct ( natgthorleh ( i n ) upper ) as [ l | r ]. assert empty. apply ( isirreflnatlth ( i n ) ). apply ( natlehlthtrans _ upper ). apply p. assumption. assumption. contradiction. apply ( nattruncautoisinj p ). apply ( nattruncautopreimageineq ). assumption. apply ( nattruncautopreimagepath p r ). intros m x v. unfold nattruncautoinv in v. destruct ( natgthorleh m upper ) as [ l | r ]. assert empty. apply ( isirreflnatlth upper ). apply ( natlthlehtrans _ m ). assumption. assumption. contradiction. rewrite <- v. apply ( nattruncautopreimagepath p r ). intros x X. unfold nattruncautoinv. destruct ( natgthorleh x upper ) as [ l | r ]. assumption. apply ( nattruncautopreimageineq p r ). Defined. Definition truncnattruncauto { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) : nat -> nat. Proof. intros upper i p n. destruct ( natlthorgeh ( i n ) ( S upper ) ) as [ l | r ]. exact ( i n ). destruct ( natgehchoice _ _ r ) as [ a | b ]. exact ( i n ). destruct ( isdeceqnat n ( S upper ) ) as [ h | k ]. exact ( i n ). exact ( i ( S upper ) ). Defined. Lemma truncnattruncautobound { upper : nat } ( i : nat -> nat ) ( p : isnattruncauto ( S upper ) i ) ( n : nat ) ( q : natleh n upper ) : natleh ( truncnattruncauto p n ) upper. Proof. intros. unfold truncnattruncauto. destruct ( natlthorgeh ( i n ) ( S upper) ) as [ l | r ]. apply natlthsntoleh. assumption. destruct ( natgehchoice ( i n ) ( S upper ) ) as [ l' | r' ]. assert empty. apply ( isirreflnatlth ( i n ) ). apply ( natlehlthtrans _ ( S upper ) ). apply p. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. assumption. contradiction. destruct ( isdeceqnat n ( S upper ) ) as [ l'' | r'' ]. assert empty. apply ( isirreflnatlth upper ). apply ( natlthlehtrans _ ( S upper ) ). apply natlthnsn. rewrite <- l''. assumption. contradiction. assert ( natleh ( i ( S upper ) ) ( S upper ) ) as aux. apply p. apply isreflnatleh. destruct ( natlehchoice _ _ aux ) as [ l''' | r''' ]. apply natlthsntoleh. assumption. assert empty. apply r''. apply ( nattruncautoisinj p ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. apply isreflnatleh. rewrite r'. rewrite r'''. apply idpath. contradiction. Defined. Lemma truncnattruncautoisinj { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) { n m : nat } ( n' : natleh n upper ) ( m' : natleh m upper ) : truncnattruncauto p n ~> truncnattruncauto p m -> n ~> m. Proof. intros upper i p n m q r s. apply ( nattruncautoisinj p ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. unfold truncnattruncauto in s. destruct ( natlthorgeh ( i n ) ( S upper ) ) as [ a0 | a1 ]. destruct ( natlthorgeh ( i m ) ( S upper ) ) as [ b0 | b1 ]. assumption. assert empty. assert ( i m ~> S upper ) as f0. destruct ( natgehchoice ( i m ) ( S upper ) b1 ) as [ l | l' ]. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ ( i n ) ). rewrite s. assumption. assumption. contradiction. assumption. destruct ( natgehchoice ( i m ) ( S upper ) b1 ) as [ a00 | a10 ]. apply ( isirreflnatgth ( S upper ) ). rewrite f0 in a00. assumption. destruct ( isdeceqnat m ( S upper ) ) as [ a000 | a100 ]. rewrite s in a0. rewrite f0 in a0. apply ( isirreflnatlth ( S upper ) ). assumption. assert ( i m ~> n ) as f1. apply ( nattruncautoisinj p ). rewrite f0. apply isreflnatleh. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. rewrite f0. rewrite s. apply idpath. apply ( isirreflnatlth upper ). apply ( natlthlehtrans _ n ). rewrite <- f1, f0. apply natlthnsn. assumption. contradiction. destruct ( natgehchoice ( i n ) ( S upper ) a1 ) as [ a00 | a01 ]. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlthlehtrans _ ( i n ) ). assumption. apply ( p ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. contradiction. destruct ( natlthorgeh ( i m ) ( S upper ) ) as [ b0 | b1 ]. destruct ( isdeceqnat n ( S upper ) ) as [ a000 | a001 ]. assumption. assert ( S upper ~> m ) as f0. apply ( nattruncautoisinj p ). apply isreflnatleh. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. assumption. assert empty. apply a001. rewrite f0. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite f0. assumption. apply natlthnsn. contradiction. contradiction. destruct ( natgehchoice ( i m ) ( S upper ) b1 ) as [ b00 | b01 ]. assert empty. apply ( isirreflnatlth ( i m ) ). apply ( natlehlthtrans _ ( S upper ) ). apply p. apply ( natlthtoleh ). apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. assumption. contradiction. rewrite b01. rewrite a01. apply idpath. Defined. Lemma truncnattruncautoisauto { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) : isnattruncauto upper ( truncnattruncauto p ). Proof. intros. split. intros n q. assert ( natleh n ( S upper ) ) as q'. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. destruct ( isdeceqnat ( nattruncautopreimage p q' ) ( S upper ) ) as [ i0 | i1 ]. split with ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ). split. assert ( natleh ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ( S upper ) ) as aux. apply nattruncautopreimageineq. destruct ( natlehchoice _ _ aux ) as [ l | r ]. apply natlthsntoleh. assumption. assert ( n ~> S upper ) as f0. rewrite <- ( nattruncautopreimagepath p q' ). rewrite i0. rewrite <- r. rewrite ( nattruncautopreimagepath p ( isreflnatleh ( S upper) ) ). rewrite r. apply idpath. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite <- f0. assumption. apply natlthnsn. contradiction. split. apply ( nattruncautoisinj p ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). apply truncnattruncautobound. destruct ( natlehchoice _ _ ( nattruncautopreimageineq p ( isreflnatleh ( S upper ) ) ) ) as [ l | r]. apply natlthsntoleh. assumption. assert empty. assert ( S upper ~> n ) as f0. rewrite <- ( nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). rewrite r. rewrite <- i0. rewrite ( nattruncautopreimagepath p q' ). apply idpath. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite f0. assumption. apply natlthnsn. contradiction. apply natlthnsn. assumption. unfold truncnattruncauto. destruct ( isdeceqnat ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) as [ l | r ]. assert empty. assert ( S upper ~> n ) as f0. rewrite <- ( nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). rewrite l. rewrite <- i0. rewrite ( nattruncautopreimagepath p q' ). apply idpath. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite f0. assumption. apply natlthnsn. contradiction. destruct ( natlthorgeh ( i ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) ( S upper ) ) as [ l' | r' ]. assert empty. apply ( isirreflnatlth ( S upper ) ) . rewrite ( nattruncautopreimagepath p ) in l'. assumption. contradiction. destruct ( natgehchoice _ _ r' ) as [ l'' | r'' ]. assert empty. apply ( isirreflnatlth ( S upper ) ) . rewrite ( nattruncautopreimagepath p ) in l''. assumption. contradiction. rewrite <- i0. rewrite ( nattruncautopreimagepath p q' ). apply idpath. intros x X y. apply ( nattruncautoisinj p ). apply nattruncautopreimageineq. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. unfold truncnattruncauto in y. destruct ( natlthorgeh ( i x ) ( S upper ) ) as [ l | r ]. assert ( S upper ~> x ) as f0. apply ( nattruncautoisinj p ). apply isreflnatleh. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. rewrite <- i0. rewrite y. rewrite ( nattruncautopreimagepath p q' ). apply idpath. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite f0. assumption. apply natlthnsn. contradiction. destruct ( isdeceqnat x ( S upper ) ) as [ l' | r' ]. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite <- l'. assumption. apply natlthnsn. contradiction. destruct ( natgehchoice _ _ r ) as [ l'' | r'' ]. assert empty. apply ( isirreflnatlth n ). apply ( natlehlthtrans _ ( S upper ) ). assumption. rewrite <- y. assumption. contradiction. rewrite ( nattruncautopreimagepath p _ ). rewrite r''. apply idpath. split with ( nattruncautopreimage p q' ). split. destruct ( natlehchoice _ _ ( nattruncautopreimageineq p q' ) ) as [ l | r ]. apply natlthsntoleh. assumption. assert empty. apply i1. assumption. contradiction. split. unfold truncnattruncauto. destruct ( natlthorgeh ( i ( nattruncautopreimage p q' ) ) ( S upper ) ) as [ l | r ]. apply nattruncautopreimagepath. destruct ( natgehchoice _ _ r ) as [ l' | r' ]. apply nattruncautopreimagepath. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite <- r'. rewrite ( nattruncautopreimagepath p q' ). assumption. apply natlthnsn. contradiction. intros x X y. apply ( nattruncautoisinj p ). apply ( pr1 p ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. rewrite ( nattruncautopreimagepath p q' ). unfold truncnattruncauto in y. destruct ( natlthorgeh ( i x ) ( S upper ) ) as [ l | r ]. rewrite y. apply idpath. destruct ( isdeceqnat x ( S upper ) ) as [ l' | r' ]. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). rewrite <- l'. assumption. apply natlthnsn. contradiction. destruct ( natgehchoice _ _ r ). rewrite y. apply idpath. assert empty. apply i1. apply ( nattruncautoisinj p ). apply ( nattruncautopreimageineq p ). apply isreflnatleh. rewrite ( nattruncautopreimagepath p q' ). rewrite y. apply idpath. contradiction. apply truncnattruncautobound. Defined. Definition truncnattruncautoinv { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) : nat -> nat := nattruncautoinv ( truncnattruncautoisauto p ). Lemma precompwithnatcofaceisauto { upper : nat } ( i : nat -> nat ) ( p : isnattruncauto ( S upper ) i ) ( bound : natlth 0 ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) : isnattruncauto upper (funcomp ( natcoface ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) i ). Proof. intros. set ( v := nattruncautopreimage p ( isreflnatleh ( S upper ) ) ). change ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) with v in bound. unfold isnattruncauto. split. intros m q. unfold funcomp. assert ( natleh m ( S upper ) ) as aaa. apply natlthtoleh. apply natlehlthtrans with ( m := upper ). assumption. exact ( natlthnsn upper ). set ( m' := nattruncautopreimage p aaa ). destruct ( natlthorgeh m' v ) as [ l | r ]. (* CASE m' < v *) split with m'. split. apply natlthsntoleh. apply ( natlthlehtrans _ v ). assumption. apply ( nattruncautopreimageineq p _ ). split. unfold natcoface. rewrite l. apply ( nattruncautopreimagepath p aaa ). intros n j w. assert ( natcoface v n ~> m' ) as f0. apply pathsinv0. apply ( nattruncautopreimagecanon p aaa ). apply natcofaceleh. assumption. assumption. rewrite <- f0. destruct ( natgthorleh v n ) as [ l' | r' ]. unfold natcoface. rewrite l'. apply idpath. assert empty. apply ( isirreflnatlth v ). apply ( natlehlthtrans _ n ). assumption. apply ( istransnatlth _ ( S n ) ). apply natlthnsn. unfold natcoface in f0. rewrite ( natgehimplnatgtbfalse v n r' ) in f0. rewrite f0. assumption. contradiction. (* CASE v <= m' *) set ( j := nattruncautopreimagepath p aaa ). change ( nattruncautopreimage p aaa ) with m' in j. set ( m'' := minus m' 1 ). assert ( natleh m'' upper ) as a0. destruct ( natlthorgeh 0 m' ) as [ h | h' ]. rewrite <- ( minussn1 upper ). apply minus1leh. assumption. apply ( natlehlthtrans _ upper ). apply natleh0n. apply natlthnsn. apply ( nattruncautopreimageineq ). destruct ( natgehchoice 0 m' h' ) as [ k | k' ]. assert empty. apply ( negnatgth0n m' k ). contradiction. unfold m''. rewrite <- k'. apply natleh0n. destruct ( natgehchoice m' v r ) as [ l' | r' ]. assert ( natleh v m'' ) as a2. apply natlthsntoleh. unfold m''. rewrite pathssminus. rewrite minussn1. assumption. destruct ( natlehchoice 0 m' ( natleh0n m' ) ) as [ k | k' ]. assumption. assert empty. apply ( negnatgth0n v ). rewrite k'. assumption. contradiction. assert ( i ( natcoface v m'' ) ~> m ) as a1. unfold natcoface. rewrite ( natgehimplnatgtbfalse v m'' a2 ). unfold m''. rewrite pathssminus. rewrite minussn1. assumption. destruct ( natlehchoice 0 m' ( natleh0n m' ) ) as [ k | k' ]. assumption. assert empty. apply ( negnatgth0n v ). rewrite k'. assumption. contradiction. split with m''. split. assumption. split. assumption. intros n s t. assert ( natcoface v n ~> natcoface v m'' ) as g. assert ( natcoface v n ~> m' ) as g0. apply pathsinv0. apply ( nattruncautopreimagecanon p aaa ). apply natcofaceleh. assumption. assumption. assert ( natcoface v m'' ~> m' ) as g1. unfold m'. unfold nattruncautopreimage. apply pathsinv0. apply ( nattruncautopreimagecanon p aaa ). apply natcofaceleh. assumption. assumption. rewrite g0, g1. apply idpath. change ( idfun _ m'' ~> idfun _ n ). rewrite <- ( natcofaceretractisretract v ). unfold funcomp. rewrite g. apply idpath. assert empty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). assert ( S upper ~> m ) as g. rewrite <- ( nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). change ( i v ~> m ). rewrite <- j. rewrite r'. apply idpath. rewrite g. assumption. apply natlthnsn. contradiction. intros x X. unfold funcomp. assert ( natleh ( i ( natcoface v x ) ) ( S upper ) ) as a0. apply p. apply natcofaceleh. assumption. destruct ( natlehchoice _ _ a0 ) as [ l | r ]. apply natlthsntoleh. assumption. assert ( v ~> natcoface v x ) as g. unfold v. apply ( nattruncautopreimagecanon p ( isreflnatleh ( S upper ) ) ). unfold natcoface. destruct ( natgthorleh v x ) as [ a | b ]. unfold v in a. rewrite a. apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. unfold v in b. rewrite ( natgehimplnatgtbfalse _ x b ). assumption. assumption. assert empty. destruct ( natgthorleh v x ) as [ a | b ]. unfold natcoface in g. rewrite a in g. apply ( isirreflnatlth x ). rewrite g in a. assumption. unfold natcoface in g. rewrite ( natgehimplnatgtbfalse v x b ) in g. apply ( isirreflnatlth x ). apply ( natlthlehtrans _ ( S x ) ). apply natlthnsn. rewrite <- g. assumption. contradiction. Defined. Lemma nattruncautocompstable { R : commrng } { upper : nat } ( i j : nat -> nat ) ( p : isnattruncauto upper i ) ( p' : isnattruncauto upper j ) : isnattruncauto upper ( funcomp j i ). Proof. intros. split. intros n n'. split with ( nattruncautopreimage p' ( nattruncautopreimageineq p n' ) ). split. apply ( nattruncautopreimageineq p' ). split. unfold funcomp. rewrite ( nattruncautopreimagepath p' _ ). rewrite ( nattruncautopreimagepath p _ ). apply idpath. intros x X y. unfold funcomp in y. apply ( nattruncautoisinj p' ). apply nattruncautopreimageineq. assumption. apply ( nattruncautoisinj p ). apply p'. apply nattruncautopreimageineq. apply p'. assumption. rewrite ( nattruncautopreimagepath p' ). rewrite ( nattruncautopreimagepath p ). rewrite y. apply idpath. intros x X. unfold funcomp. apply p. apply p'. assumption. Defined. Definition nattruncreverse ( upper : nat ) : nat -> nat. Proof. intros upper n. destruct ( natgthorleh n upper ) as [ h | k ]. exact n. exact ( minus upper n ). Defined. Definition nattruncbottomtopswap ( upper : nat ) : nat -> nat. Proof. intros upper n. destruct ( isdeceqnat 0%nat n ) as [ h | k ]. exact ( upper ). destruct ( isdeceqnat upper n ) as [ l | r ]. exact ( 0%nat ). exact n. Defined. Lemma nattruncreverseisnattruncauto ( upper : nat ) : isnattruncauto upper ( nattruncreverse upper ). Proof. intros. unfold isnattruncauto. split. intros m q. set ( m' := minus upper m ). assert ( natleh m' upper ) as a0. apply minusleh. assert ( nattruncreverse upper m' ~> m ) as a1. unfold nattruncreverse. destruct ( natgthorleh m' upper ). assert empty. apply isirreflnatlth with ( n := m' ). apply natlehlthtrans with ( m := upper ). assumption. assumption. contradiction. unfold m'. rewrite doubleminuslehpaths. apply idpath. assumption. split with m'. split. assumption. split. assumption. intros n qq u. unfold m'. rewrite <- u. unfold nattruncreverse. destruct ( natgthorleh n upper ) as [ l | r ]. assert empty. apply ( isirreflnatlth n ). apply ( natlehlthtrans _ upper ). assumption. assumption. contradiction. rewrite doubleminuslehpaths. apply idpath. assumption. intros x X. unfold nattruncreverse. destruct ( natgthorleh x upper ) as [ l | r ]. assumption. apply minusleh. Defined. Lemma nattruncbottomtopswapselfinv ( upper n : nat ) : nattruncbottomtopswap upper ( nattruncbottomtopswap upper n ) ~> n. Proof. intros. unfold nattruncbottomtopswap. destruct ( isdeceqnat upper n ). destruct ( isdeceqnat 0%nat n ). destruct ( isdeceqnat 0%nat upper ). rewrite <- i0. rewrite <- i1. apply idpath. assert empty. apply e. rewrite i0. rewrite i. apply idpath. contradiction. destruct ( isdeceqnat 0%nat 0%nat ). assumption. assert empty. apply e0. auto. contradiction. destruct ( isdeceqnat 0%nat n ). destruct ( isdeceqnat 0%nat upper ). rewrite <- i. rewrite i0. apply idpath. destruct ( isdeceqnat upper upper ). assumption. assert empty. apply e1. auto. contradiction. destruct ( isdeceqnat 0%nat n ). assert empty. apply e0. assumption. contradiction. destruct ( isdeceqnat upper n ). assert empty. apply e. assumption. contradiction. auto. Defined. Lemma nattruncbottomtopswapbound ( upper n : nat ) ( p : natleh n upper ) : natleh (nattruncbottomtopswap upper n ) upper. Proof. intros. unfold nattruncbottomtopswap. destruct (isdeceqnat 0%nat n ). auto. destruct ( isdeceqnat upper n ). apply isreflnatleh. apply isreflnatleh. destruct ( isdeceqnat upper n ). apply natleh0n. assumption. Defined. Lemma nattruncbottomtopswapisnattruncauto ( upper : nat ) : isnattruncauto upper ( nattruncbottomtopswap upper ). Proof. intros. unfold isnattruncauto. split. intros m p. set ( m' := nattruncbottomtopswap upper m ). assert ( natleh m' upper ) as a0. apply nattruncbottomtopswapbound. assumption. assert (nattruncbottomtopswap upper m' ~> m) as a1. apply nattruncbottomtopswapselfinv. split with m'. split. assumption. split. assumption. intros k q u. unfold m'. rewrite <- u. rewrite nattruncbottomtopswapselfinv. apply idpath. intros n p. apply nattruncbottomtopswapbound. assumption. Defined. Lemma isnattruncauto0S { upper : nat } { i : nat -> nat } ( p : isnattruncauto (S upper) i ) ( j : i 0%nat ~> S upper ) : isnattruncauto upper ( funcomp S i ). Proof. intros. unfold isnattruncauto. split. intros m q. set ( v := nattruncautopreimage p (natlthtoleh m (S upper) (natlehlthtrans m upper (S upper) q (natlthnsn upper)))). destruct ( isdeceqnat 0%nat v ) as [ i0 | i1 ]. assert empty. apply ( isirreflnatlth ( i 0%nat ) ). apply ( natlehlthtrans _ upper ). rewrite i0. unfold v. rewrite ( nattruncautopreimagepath ). assumption. rewrite j. apply natlthnsn. contradiction. assert ( natlth 0 v ) as aux. destruct ( natlehchoice _ _ ( natleh0n v ) ). assumption. assert empty. apply i1. assumption. contradiction. split with ( minus v 1 ). split. rewrite <- ( minussn1 upper ). apply ( minus1leh aux ( natlehlthtrans _ _ _ ( natleh0n upper ) ( natlthnsn upper ) ) ( nattruncautopreimageineq p ( natlthtoleh m ( S upper ) ( natlehlthtrans m upper ( S upper ) q ( natlthnsn upper ) ) ) ) ). split. unfold funcomp. rewrite pathssminus. rewrite minussn1. apply nattruncautopreimagepath. assumption. intros n uu k. unfold funcomp in k. rewrite <- ( minussn1 n ). assert ( v ~> S n ) as f. apply ( nattruncautopreimagecanon p _ ). assumption. assumption. rewrite f. apply idpath. intros x X. unfold funcomp. assert ( natleh ( i ( S x ) ) ( S upper ) ) as aux. apply p. assumption. destruct ( natlehchoice _ _ aux ) as [ h | k ]. apply natlthsntoleh. assumption. assert empty. assert ( 0%nat ~> S x ) as ii. apply ( nattruncautoisinj p ). apply natleh0n. assumption. rewrite j. rewrite k. apply idpath. apply ( isirreflnatlth ( S x ) ). apply ( natlehlthtrans _ x ). rewrite <- ii. apply natleh0n. apply natlthnsn. contradiction. Defined. (* The following lemma says that we may reindex sums along automorphisms of the interval over which the finite summation is being taken. *) Lemma natsummationreindexing { R : commrng } { upper : nat } ( i : nat -> nat ) ( p : isnattruncauto upper i ) ( f : nat -> R ) : natsummation0 upper f ~> natsummation0 upper (funcomp i f ). Proof. intros R upper. induction upper. intros. simpl. unfold funcomp. assert ( 0%nat ~> i 0%nat ) as f0. destruct ( natlehchoice ( i 0%nat ) 0%nat ( pr2 p 0%nat ( isreflnatleh 0%nat ) ) ) as [ h | k ]. assert empty. exact ( negnatlthn0 ( i 0%nat ) h ). contradiction. rewrite k. apply idpath. rewrite <- f0. apply idpath. intros. simpl ( natsummation0 ( S upper ) f ). set ( j := nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). set ( v := nattruncautopreimage p ( isreflnatleh ( S upper ) ) ). change ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) with v in j. destruct ( natlehchoice 0%nat v ( natleh0n v ) ). set ( aaa := nattruncautopreimageineq p ( isreflnatleh ( S upper ) ) ). change ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) with v in aaa. destruct ( natlehchoice v ( S upper ) aaa ) as [ l | r ]. rewrite ( IHupper ( funcomp ( natcoface v ) i ) ). change ( funcomp ( funcomp ( natcoface v ) i ) f ) with ( funcomp ( natcoface v ) ( funcomp i f ) ). assert ( f ( S upper ) ~> ( funcomp i f ) v ) as f0. unfold funcomp. rewrite j. apply idpath. rewrite f0. assert ( natleh v upper ) as aux. apply natlthsntoleh. assumption. rewrite ( natsummationshift upper ( funcomp i f ) aux ). apply idpath. apply precompwithnatcofaceisauto. assumption. rewrite ( IHupper ( funcomp ( natcoface v ) i ) ). assert ( natsummation0 upper ( funcomp ( funcomp ( natcoface v ) i) f ) ~> natsummation0 upper ( funcomp i f ) ) as f0. apply natsummationpathsupperfixed. intros x X. unfold funcomp. unfold natcoface. assert ( natlth x v ) as a0. apply ( natlehlthtrans _ upper ). assumption. rewrite r. apply natlthnsn. rewrite a0. apply idpath. rewrite f0. assert ( f ( S upper ) ~> ( funcomp i f ) ( S upper ) ) as f1. unfold funcomp. rewrite <- r. rewrite j. rewrite <- r. apply idpath. rewrite f1. apply idpath. apply precompwithnatcofaceisauto. assumption. rewrite natsummationshift0. unfold funcomp at 2. rewrite i0. rewrite j. assert ( i 0%nat ~> S upper ) as j'. rewrite i0. rewrite j. apply idpath. rewrite ( IHupper ( funcomp S i ) ( isnattruncauto0S p j' ) ). apply idpath. Defined. (** * III. Formal Power Series *) Definition seqson ( A : UU ) := nat -> A. Lemma seqsonisaset ( A : hSet ) : isaset ( seqson A ). Proof. intros. unfold seqson. change ( isofhlevel 2 ( nat -> A ) ). apply impredfun. apply A. Defined. Definition isasetfps ( R : commrng ) : isaset ( seqson R ) := seqsonisaset R. Definition fps ( R : commrng ) : hSet := hSetpair _ ( isasetfps R ). Definition fpsplus ( R : commrng ) : binop ( fps R ) := fun v w n => ( ( v n ) + ( w n ) ). Definition fpstimes ( R : commrng ) : binop ( fps R ) := fun s t n => natsummation0 n ( fun x : nat => ( s x ) * ( t ( minus n x ) ) ). (* SOME TESTS OF THE SUMMATION AND FPSTIMES DEFINITIONS: Definition test0 : seqson hz. Proof. intro n. induction n. exact 0. exact ( nattohz ( S n ) ). Defined. Eval lazy in ( hzabsval ( natsummation0 1 test0 ) ). Definition test1 : seqson hz. Proof. intro n. induction n. exact ( 1 + 1 ). exact ( ( 1 + 1 ) * IHn ). Defined. Eval lazy in ( hzabsval ( fpstimes hz test0 test1 0%nat ) ). Eval lazy in ( hzabsval ( fpstimes hz test0 test1 1%nat ) ). Eval lazy in ( hzabsval ( fpstimes hz test0 test1 2%nat ) ). Eval lazy in ( hzabsval ( fpstimes hz test0 test1 3%nat ) ). Eval lazy in ( hzabsval ( fpstimes hz test0 test1 4%nat ) ). *) Definition fpszero ( R : commrng ) : fps R := ( fun n : nat => 0 ). Definition fpsone ( R : commrng ) : fps R. Proof. intros. intro n. destruct n. exact 1. exact 0. Defined. Definition fpsminus ( R : commrng ) : fps R -> fps R := ( fun s n => - ( s n ) ). Lemma ismonoidopfpsplus ( R : commrng ) : ismonoidop ( fpsplus R ). Proof. intros. unfold ismonoidop. split. unfold isassoc. intros s t u. unfold fpsplus. (* This is a hack which should work immediately without such a workaround! *) change ( (fun n : nat => s n + t n + u n) ~> (fun n : nat => s n + (t n + u n)) ). apply funextfun. intro n. apply R. unfold isunital. assert ( isunit ( fpsplus R ) ( fpszero R ) ) as a. unfold isunit. split. unfold islunit. intro s. unfold fpsplus. unfold fpszero. change ( (fun n : nat => 0 + s n) ~> s ). apply funextfun. intro n. apply rnglunax1. unfold isrunit. intro s. unfold fpsplus. unfold fpszero. change ( (fun n : nat => s n + 0) ~> s ). apply funextfun. intro n. apply rngrunax1. exact ( tpair ( fpszero R ) a ). Defined. Lemma isgropfpsplus ( R : commrng ) : isgrop ( fpsplus R ). Proof. intros. unfold isgrop. assert ( invstruct ( fpsplus R ) ( ismonoidopfpsplus R ) ) as a. unfold invstruct. assert ( isinv (fpsplus R) (unel_is (ismonoidopfpsplus R)) ( fpsminus R ) ) as b. unfold isinv. split. unfold islinv. intro s. unfold fpsplus. unfold fpsminus. unfold unel_is. simpl. unfold fpszero. apply funextfun. intro n. exact ( rnglinvax1 R ( s n ) ). unfold isrinv. intro s. unfold fpsplus. unfold fpsminus. unfold unel_is. simpl. unfold fpszero. apply funextfun. intro n. exact ( rngrinvax1 R ( s n ) ). exact ( tpair ( fpsminus R ) b ). exact ( tpair ( ismonoidopfpsplus R ) a ). Defined. Lemma iscommfpsplus ( R : commrng ) : iscomm ( fpsplus R ). Proof. intros. unfold iscomm. intros s t. unfold fpsplus. change ((fun n : nat => s n + t n) ~> (fun n : nat => t n + s n) ). apply funextfun. intro n. apply R. Defined. Lemma isassocfpstimes ( R : commrng ) : isassoc (fpstimes R). Proof. intros. unfold isassoc. intros s t u. unfold fpstimes. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( minus n x) (fun x0 : nat => s x * ( t x0 * u ( minus ( minus n x ) x0) )))) ~> (fun n : nat => natsummation0 n (fun x : nat => s x * natsummation0 ( minus n x) (fun x0 : nat => t x0 * u ( minus ( minus n x ) x0)))) ) as A. apply funextfun. intro n. apply natsummationpathsupperfixed. intros. rewrite natsummationtimesdistr. apply idpath. rewrite <- A. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( minus n x) (fun x0 : nat => s x * t x0 * u ( minus ( minus n x ) x0 )))) ~> (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( minus n x) (fun x0 : nat => s x * ( t x0 * u ( minus ( minus n x ) x0) )))) ) as B. apply funextfun. intro n. apply maponpaths. apply funextfun. intro m. apply maponpaths. apply funextfun. intro x. apply R. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 x (fun x0 : nat => s x0 * t ( minus x x0 ) * u ( minus n x )))) ~> (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( minus n x) (fun x0 : nat => s x * t x0 * u ( minus ( minus n x ) x0 )))) ) as C. apply funextfun. intro n. set ( f := fun x : nat => ( fun x0 : nat => s x * t x0 * u ( minus ( minus n x ) x0 ) ) ). assert ( natsummation0 n ( fun x : nat => natsummation0 x ( fun x0 : nat => f x0 ( minus x x0 ) ) ) ~> ( natsummation0 n ( fun x : nat => natsummation0 ( minus n x ) ( fun x0 : nat => f x x0 ) ) ) ) as D. apply natsummationswap. unfold f in D. assert ( natsummation0 n ( fun x : nat => natsummation0 x ( fun x0 : nat => s x0 * t ( minus x x0 ) * u ( minus n x ) ) ) ~> natsummation0 n ( fun x : nat => natsummation0 x ( fun x0 : nat => s x0 * t ( minus x x0 ) * u ( minus ( minus n x0 ) ( minus x x0 ) ) ) ) ) as E. apply natsummationpathsupperfixed. intros k p. apply natsummationpathsupperfixed. intros l q. rewrite ( natdoubleminus p q ). apply idpath. rewrite E, D. apply idpath. rewrite <- B. rewrite <- C. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 x (fun x0 : nat => s x0 * t ( minus x x0)) * u ( minus n x))) ~> (fun n : nat => natsummation0 n (fun x : nat => natsummation0 x (fun x0 : nat => s x0 * t ( minus x x0) * u ( minus n x)))) ) as D. apply funextfun. intro n. apply maponpaths. apply funextfun. intro m. apply natsummationtimesdistl. rewrite <- D. apply idpath. Defined. Lemma natsummationandfpszero ( R : commrng ) : forall m : nat, natsummation0 m ( fun x : nat => fpszero R x ) ~> ( @rngunel1 R ). Proof. intros R m. induction m. apply idpath. simpl. rewrite IHm. rewrite ( rnglunax1 R ). apply idpath. Defined. Lemma ismonoidopfpstimes ( R : commrng ) : ismonoidop ( fpstimes R ). Proof. intros. unfold ismonoidop. split. apply isassocfpstimes. split with ( fpsone R). split. intro s. unfold fpstimes. change ( ( fun n : nat => natsummation0 n ( fun x : nat => fpsone R x * s ( minus n x ) ) ) ~> s ). apply funextfun. intro n. destruct n. simpl. rewrite ( rnglunax2 R ). apply idpath. rewrite natsummationshift0. rewrite ( rnglunax2 R). rewrite minus0r. assert ( natsummation0 n ( fun x : nat => fpsone R ( S x ) * s ( minus n x ) ) ~> ( ( natsummation0 n ( fun x : nat => fpszero R x ) ) ) ) as f. apply natsummationpathsupperfixed. intros m m'. rewrite ( rngmult0x R ). apply idpath. change ( natsummation0 n ( fun x : nat => fpsone R ( S x ) * s ( minus n x ) ) + s ( S n ) ~> ( s ( S n ) ) ). rewrite f. rewrite natsummationandfpszero. apply ( rnglunax1 R ). intros s. unfold fpstimes. change ( ( fun n : nat => natsummation0 n ( fun x : nat => s x * fpsone R ( minus n x ) ) ) ~> s ). apply funextfun. intro n. destruct n. simpl. rewrite ( rngrunax2 R ). apply idpath. change ( natsummation0 n ( fun x : nat => s x * fpsone R ( minus ( S n ) x ) ) + s ( S n ) * fpsone R ( minus n n ) ~> s ( S n ) ). rewrite minusnn0. rewrite ( rngrunax2 R ). assert ( natsummation0 n ( fun x : nat => s x * fpsone R ( minus ( S n ) x )) ~> ( ( natsummation0 n ( fun x : nat => fpszero R x ) ) ) ) as f. apply natsummationpathsupperfixed. intros m m'. rewrite <- pathssminus. rewrite ( rngmultx0 R ). apply idpath. apply ( natlehlthtrans _ n ). assumption. apply natlthnsn. rewrite f. rewrite natsummationandfpszero. apply ( rnglunax1 R ). Defined. Lemma iscommfpstimes ( R : commrng ) ( s t : fps R ) : fpstimes R s t ~> fpstimes R t s. Proof. intros. unfold fpstimes. change ( ( fun n : nat => natsummation0 n (fun x : nat => s x * t ( minus n x) ) ) ~> (fun n : nat => natsummation0 n (fun x : nat => t x * s ( minus n x))) ). apply funextfun. intro n. assert ( natsummation0 n ( fun x : nat => s x * t ( minus n x ) ) ~> ( natsummation0 n ( fun x : nat => t ( minus n x ) * s x ) ) ) as a0. apply maponpaths. apply funextfun. intro m. apply R. assert ( ( natsummation0 n ( fun x : nat => t ( minus n x ) * s x ) ) ~> ( natsummation0 n ( funcomp ( nattruncreverse n ) ( fun x : nat => t x * s ( minus n x ) ) ) ) ) as a1. apply natsummationpathsupperfixed. intros m q. unfold funcomp. unfold nattruncreverse. destruct (natgthorleh m n ). assert empty. apply isirreflnatlth with ( n := n ). apply natlthlehtrans with ( m := m ). apply h. assumption. contradiction. apply maponpaths. apply maponpaths. apply pathsinv0. apply doubleminuslehpaths. assumption. assert ( ( natsummation0 n ( funcomp ( nattruncreverse n ) ( fun x : nat => t x * s ( minus n x ) ) ) ) ~> natsummation0 n ( fun x : nat => t x * s ( minus n x ) ) ) as a2. apply pathsinv0. apply natsummationreindexing. apply nattruncreverseisnattruncauto. exact ( pathscomp0 a0 ( pathscomp0 a1 a2 ) ). Defined. Lemma isldistrfps ( R : commrng ) ( s t u : fps R ) : fpstimes R s ( fpsplus R t u ) ~> ( fpsplus R ( fpstimes R s t ) ( fpstimes R s u ) ). Proof. intros. unfold fpstimes. unfold fpsplus. change ((fun n : nat => natsummation0 n (fun x : nat => s x * (t (minus n x) + u ( minus n x)))) ~> (fun n : nat => natsummation0 n (fun x : nat => s x * t (minus n x)) + natsummation0 n (fun x : nat => s x * u (minus n x))) ). apply funextfun. intro upper. assert ( natsummation0 upper ( fun x : nat => s x * ( t ( minus upper x ) + u ( minus upper x ) ) ) ~> ( natsummation0 upper ( fun x : nat => ( ( s x * t ( minus upper x ) ) + ( s x * u ( minus upper x ) ) ) ) ) ) as a0. apply maponpaths. apply funextfun. intro n. apply R. assert ( ( natsummation0 upper ( fun x : nat => ( ( s x * t ( minus upper x ) ) + ( s x * u ( minus upper x ) ) ) ) ) ~> ( ( natsummation0 upper ( fun x : nat => s x * t ( minus upper x ) ) ) + ( natsummation0 upper ( fun x : nat => s x * u ( minus upper x ) ) ) ) ) as a1. apply natsummationplusdistr. exact ( pathscomp0 a0 a1 ). Defined. Lemma isrdistrfps ( R : commrng ) ( s t u : fps R ) : fpstimes R ( fpsplus R t u ) s ~> ( fpsplus R ( fpstimes R t s ) ( fpstimes R u s ) ). Proof. intros. unfold fpstimes. unfold fpsplus. change ((fun n : nat => natsummation0 n (fun x : nat => (t x + u x) * s ( minus n x ) )) ~> (fun n : nat => natsummation0 n (fun x : nat => t x * s ( minus n x ) ) + natsummation0 n (fun x : nat => u x * s (minus n x))) ). apply funextfun. intro upper. assert ( natsummation0 upper ( fun x : nat => ( t x + u x ) * s ( minus upper x ) ) ~> ( natsummation0 upper ( fun x : nat => ( ( t x * s ( minus upper x ) ) + ( u x * s ( minus upper x ) ) ) ) ) ) as a0. apply maponpaths. apply funextfun. intro n. apply R. assert ( ( natsummation0 upper ( fun x : nat => ( ( t x * s ( minus upper x ) ) + ( u x * s ( minus upper x ) ) ) ) ) ~> ( ( natsummation0 upper ( fun x : nat => t x * s ( minus upper x ) ) ) + ( natsummation0 upper ( fun x : nat => u x * s ( minus upper x ) ) ) ) ) as a1. apply natsummationplusdistr. exact ( pathscomp0 a0 a1 ). Defined. Definition fpsrng ( R : commrng ) := setwith2binoppair ( hSetpair ( seqson R ) ( isasetfps R ) ) ( dirprodpair ( fpsplus R ) ( fpstimes R ) ). Theorem fpsiscommrng ( R : commrng ) : iscommrng ( fpsrng R ). Proof. intro. unfold iscommrng. unfold iscommrngops. split. unfold isrngops. split. split. unfold isabgrop. split. exact ( isgropfpsplus R ). exact ( iscommfpsplus R ). exact ( ismonoidopfpstimes R ). unfold isdistr. split. unfold isldistr. intros. apply ( isldistrfps R ). unfold isrdistr. intros. apply ( isrdistrfps R ). unfold iscomm. intros. apply ( iscommfpstimes R ). Defined. Definition fpscommrng ( R : commrng ) : commrng := commrngpair ( fpsrng R ) ( fpsiscommrng R ). Definition fpsshift { R : commrng } ( a : fpscommrng R ) : fpscommrng R := fun n : nat => a ( S n ). Lemma fpsshiftandmult { R : commrng } ( a b : fpscommrng R ) ( p : b 0%nat ~> 0 ) : forall n : nat, ( a * b ) ( S n ) ~> ( ( a * ( fpsshift b ) ) n ). Proof. intros. induction n. change ( a * b ) with ( fpstimes R a b ). change ( a * fpsshift b ) with ( fpstimes R a ( fpsshift b ) ). unfold fpstimes. unfold fpsshift. simpl. rewrite p. rewrite ( rngmultx0 R ). rewrite ( rngrunax1 R ). apply idpath. change ( a * b ) with ( fpstimes R a b ). change ( a * fpsshift b ) with ( fpstimes R a ( fpsshift b ) ). unfold fpsshift. unfold fpstimes. change ( natsummation0 (S (S n)) (fun x : nat => a x * b (minus ( S (S n) ) x)) ) with ( ( natsummation0 ( S n ) ( fun x : nat => a x * b ( minus ( S ( S n ) ) x ) ) ) + a ( S ( S n ) ) * b ( minus ( S ( S n ) ) ( S ( S n ) ) ) ). rewrite minusnn0. rewrite p. rewrite ( rngmultx0 R ). rewrite rngrunax1. apply natsummationpathsupperfixed. intros x j. apply maponpaths. apply maponpaths. rewrite pathssminus. apply idpath. apply ( natlehlthtrans _ ( S n ) _ ). assumption. apply natlthnsn. Defined. (** * IV. Apartness relation on formal power series *) Lemma apartbinarysum0 ( R : acommrng ) ( a b : R ) ( p : a + b # 0 ) : hdisj ( a # 0 ) ( b # 0 ). Proof. intros. intros P s. apply ( acommrng_acotrans R ( a + b ) a 0 p ). intro k. destruct k as [ l | r ]. apply s. apply ii2. assert ( a + b # a ) as l'. apply l. assert ( ( a + b ) # ( a + 0 ) ) as l''. rewrite rngrunax1. assumption. apply ( ( pr1 ( acommrng_aadd R ) ) a b 0 ). assumption. apply s. apply ii1. assumption. Defined. Lemma apartnatsummation0 ( R : acommrng ) ( upper : nat ) ( f : nat -> R ) ( p : ( natsummation0 upper f ) # 0 ) : hexists ( fun n : nat => dirprod ( natleh n upper ) ( f n # 0 ) ). Proof. intros R upper. induction upper. simpl. intros. intros P s. apply s. split with 0%nat. split. intros g. simpl in g. apply nopathsfalsetotrue. assumption. assumption. intros. intros P s. simpl in p. apply ( apartbinarysum0 R _ _ p ). intro k. destruct k as [ l | r ]. apply ( IHupper f l ). intro k. destruct k as [ n ab ]. destruct ab as [ a b ]. apply s. split with n. split. apply ( istransnatleh _ upper _ ). assumption. apply natlthtoleh. apply natlthnsn. assumption. apply s. split with ( S upper ). split. apply isreflnatleh. assumption. Defined. Definition fpsapart0 ( R : acommrng ) : hrel ( fpscommrng R ) := fun s t : fpscommrng R => ( hexists ( fun n : nat => ( s n # t n ) ) ). Definition fpsapart ( R : acommrng ) : apart ( fpscommrng R ). Proof. intros. split with ( fpsapart0 R ). split. intros s f. assert ( hfalse ) as i. apply f. intro k. destruct k as [ n p ]. apply ( acommrng_airrefl R ( s n ) p). apply i. split. intros s t p P j. apply p. intro k. destruct k as [ n q ]. apply j. split with n. apply ( acommrng_asymm R ( s n ) ( t n ) q ). intros s t u p P j. apply p. intro k. destruct k as [ n q ]. apply ( acommrng_acotrans R ( s n ) ( t n ) ( u n ) q ). intro l. destruct l as [ l | r ]. apply j. apply ii1. intros v V. apply V. split with n. assumption. apply j. apply ii2. intros v V. apply V. split with n. assumption. Defined. Lemma fpsapartisbinopapartplusl ( R : acommrng ) : isbinopapartl ( fpsapart R ) ( @op1 ( fpscommrng R ) ). Proof. intros. intros a b c p. intros P s. apply p. intro k. destruct k as [ n q ]. apply s. change ( ( a + b ) n ) with ( ( a n ) + ( b n ) ) in q. change ( ( a + c ) n ) with ( ( a n ) + ( c n ) ) in q. split with n. apply ( ( pr1 ( acommrng_aadd R ) ) ( a n ) ( b n ) ( c n ) q ). Defined. Lemma fpsapartisbinopapartplusr ( R : acommrng ) : isbinopapartr ( fpsapart R ) ( @op1 ( fpscommrng R ) ). Proof. intros. intros a b c p. rewrite ( rngcomm1 ( fpscommrng R ) ) in p. rewrite ( rngcomm1 ( fpscommrng R ) c ) in p. apply ( fpsapartisbinopapartplusl _ a b c ). assumption. Defined. Lemma fpsapartisbinopapartmultl ( R : acommrng ) : isbinopapartl ( fpsapart R ) ( @op2 ( fpsrng R ) ). Proof. intros. intros a b c p. intros P s. apply p. intro k. destruct k as [ n q ]. change ( ( a * b ) n ) with ( natsummation0 n ( fun x : nat => ( a x ) * ( b ( minus n x ) ) ) ) in q. change ( ( a * c ) n ) with ( natsummation0 n ( fun x : nat => ( a x ) * ( c ( minus n x ) ) ) ) in q. assert ( natsummation0 n ( fun x : nat => ( a x * b ( minus n x ) - ( a x * c ( minus n x ) ) ) ) # 0 ) as q'. assert ( natsummation0 n ( fun x : nat => ( a x * b ( minus n x ) ) ) - natsummation0 n ( fun x : nat => ( a x * c ( minus n x ) ) ) # 0 ) as q''. apply aaminuszero. assumption. assert ( (fun x : nat => a x * b (minus n x) - a x * c ( minus n x)) ~> (fun x : nat => a x * b ( minus n x) + ( - 1%rng ) * ( a x * c ( minus n x)) ) ) as i. apply funextfun. intro x. apply maponpaths. rewrite <- ( rngmultwithminus1 R ). apply idpath. rewrite i. rewrite natsummationplusdistr. rewrite <- ( natsummationtimesdistr n ( fun x : nat => a x * c ( minus n x ) ) ( - 1%rng ) ). rewrite ( rngmultwithminus1 R ). assumption. apply ( apartnatsummation0 R n _ q' ). intro k. destruct k as [ m g ]. destruct g as [ g g' ]. apply s. split with ( minus n m ). apply ( ( pr1 ( acommrng_amult R ) ) ( a m ) ( b ( minus n m ) ) ( c ( minus n m ) ) ). apply aminuszeroa. assumption. Defined. Lemma fpsapartisbinopapartmultr ( R : acommrng ) : isbinopapartr ( fpsapart R ) ( @op2 ( fpsrng R ) ). Proof. intros. intros a b c p. rewrite ( rngcomm2 ( fpscommrng R ) ) in p. rewrite ( rngcomm2 ( fpscommrng R ) c ) in p. apply ( fpsapartisbinopapartmultl _ a b c ). assumption. Defined. Definition acommrngfps ( R : acommrng ) : acommrng. Proof. intros. split with ( fpscommrng R ). split with ( fpsapart R ). split. split. apply ( fpsapartisbinopapartplusl R). apply ( fpsapartisbinopapartplusr R ). split. apply ( fpsapartisbinopapartmultl R ). apply ( fpsapartisbinopapartmultr R ). Defined. Definition isacommrngapartdec ( R : acommrng ) := isapartdec ( ( pr1 ( pr2 R ) ) ). Lemma leadingcoefficientapartdec ( R : aintdom ) ( a : fpscommrng R ) ( is : isacommrngapartdec R ) ( p : a 0%nat # 0 ) : forall n : nat, forall b : fpscommrng R, ( b n # 0 ) -> ( ( acommrngapartrel ( acommrngfps R ) ) ( a * b ) 0 ). Proof. intros R a is p n. induction n. intros b q. intros P s. apply s. split with 0%nat. change ( ( a * b ) 0%nat ) with ( ( a 0%nat ) * ( b 0%nat ) ). apply R. assumption. assumption. intros b q. destruct ( is ( b 0%nat ) 0 ) as [ left | right ]. intros P s. apply s. split with 0%nat. change ( ( a * b ) 0%nat ) with ( ( a 0%nat ) * ( b 0%nat ) ). apply R. assumption. assumption. assert ( ( acommrngapartrel ( acommrngfps R ) ) ( a * ( fpsshift b ) ) 0 ) as j. apply IHn. unfold fpsshift. assumption. apply j. intro k. destruct k as [ k i ]. intros P s. apply s. rewrite <- ( fpsshiftandmult a b right k ) in i. split with ( S k ). assumption. Defined. Lemma apartdecintdom0 ( R : aintdom ) ( is : isacommrngapartdec R ) : forall n : nat, forall a b : fpscommrng R, ( a n # 0 ) -> ( acommrngapartrel ( acommrngfps R ) b 0 ) -> ( acommrngapartrel ( acommrngfps R ) ( a * b ) 0 ). Proof. intros R is n. induction n. intros a b p q. apply q. intros k. destruct k as [ k k0 ]. apply ( leadingcoefficientapartdec R a is p k ). assumption. intros a b p q. destruct ( is ( a 0%nat ) 0 ) as [ left | right ]. apply q. intros k. destruct k as [ k k0 ]. apply ( leadingcoefficientapartdec R a is left k ). assumption. assert ( acommrngapartrel ( acommrngfps R ) ( ( fpsshift a ) * b ) 0 ) as i. apply IHn. unfold fpsshift. assumption. assumption. apply i. intros k. destruct k as [ k k0 ]. intros P s. apply s. split with ( S k ). rewrite rngcomm2. rewrite fpsshiftandmult. rewrite rngcomm2. assumption. assumption. Defined. Theorem apartdectoisaintdomfps ( R : aintdom ) ( is : isacommrngapartdec R ) : aintdom. Proof. intros R. split with ( acommrngfps R ). split. intros P s. apply s. split with 0%nat. change ( ( @rngunel1 ( fpscommrng R ) ) 0%nat ) with ( @rngunel1 R ). change ( @rngunel2 R # ( @rngunel1 R ) ). apply R. intros a b p q. apply p. intro n. destruct n as [ n n0 ]. apply ( apartdecintdom0 R is n) . assumption. assumption. Defined. Close Scope rng_scope. (** END OF FILE *)Pelayo-Coq/._frac.v000777 000765 000024 00000000324 12104265206 014762 0ustar00nicolastaff000000 000000 Mac OS X  2¢ÔATTRÔ˜<˜<com.apple.quarantineq/0002;53a854a1;Safari;5085629F-B604-4322-A539-1F4796CB8AB1Pelayo-Coq/frac.v000777 000765 000024 00000043336 12104265206 014557 0ustar00nicolastaff000000 000000 (** *The Heyting field of fractions for an apartness domain *) (** By Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren *) (** February 2011 and August 2012 *) (** Settings *) Add Rec LoadPath "../Generalities". Add Rec LoadPath "../hlevel1". Add Rec LoadPath "../hlevel2". Add Rec LoadPath "../Algebra". Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *) (** Imports *) Require Export lemmas. (** * I. The field of fractions for an integrable domain with an apartness relation *) Open Scope rng_scope. Section aint. Variable A : aintdom. Ltac permute := solve [ repeat rewrite rngassoc2; match goal with | [ |- ?X ~> ?X ] => apply idpath | [ |- ?X * ?Y ~> ?X * ?Z ] => apply maponpaths; permute | [ |- ?Y * ?X ~> ?Z * ?X ] => apply ( maponpaths ( fun x => x * X ) ); permute | [ |- ?X * ?Y ~> ?Y * ?X ] => apply rngcomm2 | [ |- ?X * ?Y ~> ?K ] => solve [ repeat rewrite <- rngassoc2; match goal with | [ |- ?H ~> ?V * X ] => rewrite ( @rngcomm2 A V X ); repeat rewrite rngassoc2; apply maponpaths; permute end | repeat rewrite rngassoc2; match goal with | [ |- ?H ~> ?Z * ?V ] => repeat rewrite <- rngassoc2; match goal with | [ |- ?W * Z ~> ?L ] => rewrite ( @rngcomm2 A W Z ); repeat rewrite rngassoc2; apply maponpaths; permute end end ] |[ |- ?X * ( ?Y * ?Z ) ~> ?K ] => rewrite ( @rngcomm2 A Y Z ); permute end | repeat rewrite <- rngassoc2; match goal with | [ |- ?X * ?Y ~> ?X * ?Z ] => apply maponpaths; permute | [ |- ?Y * ?X ~> ?Z * ?X ] => apply ( maponpaths ( fun x => x * X ) ); permute | [ |- ?X * ?Y ~> ?Y * ?X ] => apply rngcomm2 end | apply idpath | idtac "The tactic permute does not apply to the current goal!" ]. Lemma azerorelcomp ( cd : dirprod A ( aintdomazerosubmonoid A ) ) ( ef : dirprod A ( aintdomazerosubmonoid A ) ) ( p : ( pr1 cd ) * ( pr1 ( pr2 ef ) ) ~> ( ( pr1 ef ) * ( pr1 ( pr2 cd ) ) ) ) ( q : ( pr1 cd ) # 0 ) : ( pr1 ef ) # 0. Proof. intros. change ( ( @op2 A ( pr1 cd ) ( pr1 ( pr2 ef ) ) ) ~> ( @op2 A ( pr1 ef ) ( pr1 ( pr2 cd ) ) ) ) in p. assert ( ( @op2 A ( pr1 cd ) ( pr1 ( pr2 ef ) ) ) # 0 ) as v. apply A. assumption. apply ( pr2 ( pr2 ef ) ). rewrite p in v. apply ( pr1 ( timesazero v ) ). Defined. Lemma azerolmultcomp { a b c : A } ( p : a # 0 ) ( q : b # c ) : a * b # a * c. Proof. intros. apply aminuszeroa. rewrite <- rngminusdistr. apply ( pr2 A ). assumption. apply aaminuszero. assumption. Defined. Lemma azerormultcomp { a b c : A } ( p : a # 0 ) ( q : b # c ) : b * a # c * a. Proof. intros. rewrite ( @rngcomm2 A b ). rewrite ( @rngcomm2 A c ). apply ( azerolmultcomp p q ). Defined. Definition afldfracapartrelpre : hrel ( dirprod A ( aintdomazerosubmonoid A ) ) := fun ab cd : _ => ( ( pr1 ab ) * ( pr1 ( pr2 cd ) ) ) # ( ( pr1 cd ) * ( pr1 ( pr2 ab ) ) ). Lemma afldfracapartiscomprel : iscomprelrel ( eqrelcommrngfrac A ( aintdomazerosubmonoid A ) ) ( afldfracapartrelpre ). Proof. intros ab cd ef gh p q. unfold afldfracapartrelpre. destruct ab as [ a b ]. destruct b as [ b b' ]. destruct cd as [ c d ]. destruct d as [ d d' ]. destruct ef as [ e f ]. destruct f as [ f f' ]. destruct gh as [ g h ]. destruct h as [ h h' ]. simpl in *. apply uahp. intro u. apply p. intro p'. apply q. intro q'. destruct p' as [ p' j ]. destruct p' as [ i p' ]. destruct q' as [ q' j' ]. destruct q' as [ i' q' ]. simpl in *. assert ( a * f * d * i * h * i' # e * b * d * i * h * i') as v0. assert ( a * f * d # e * b * d ) as v0. apply azerormultcomp. apply d'. assumption. assert ( a * f * d * i # e * b * d * i ) as v1. apply azerormultcomp. assumption. assumption. assert ( a * f * d * i * h # e * b * d * i * h ) as v2. apply azerormultcomp. apply h'. assumption. apply azerormultcomp. assumption. assumption. apply ( pr2 ( acommrng_amult A ) b ). apply ( pr2 ( acommrng_amult A ) f ). apply ( pr2 ( acommrng_amult A ) i ). apply ( pr2 ( acommrng_amult A ) i' ). assert ( a * f * d * i * h * i' ~> c * h * b * f * i * i' ) as l. assert ( a * f * d * i * h * i' ~> a * d * i * f * h * i' ) as l0. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a f ) d ) i ) h ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a d ) i ) f ) h ) i' ). permute. rewrite l0. rewrite j. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c b ) i ) f ) h ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c h ) b ) f ) i ) i' ). permute. rewrite l in v0. assert ( e * b * d * i * h * i' ~> g * d * b * f * i * i' ) as k. assert ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) i ) h ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e h ) i' ) i ) b ) d ) as k0. permute. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) i ) h ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g d ) b ) f ) i ) i' ). rewrite k0. assert ( @op2 A ( @op2 A e h ) i' ~> @op2 A ( @op2 A g f ) i' ) as j''. assumption. rewrite j''. permute. rewrite k in v0. assumption. intro u. apply p. intro p'. apply q. intro q'. destruct p' as [ p' j ]. destruct p' as [ i p' ]. destruct q' as [ q' j' ]. destruct q' as [ i' q' ]. simpl in *. assert ( c * h * b * f * i * i' # g * d * b * f * i * i' ) as v. apply azerormultcomp. apply q'. apply azerormultcomp. apply p'. apply azerormultcomp. apply f'. apply azerormultcomp. apply b'. assumption. apply ( pr2 ( acommrng_amult A ) d ). apply ( pr2 ( acommrng_amult A ) h ). apply ( pr2 ( acommrng_amult A ) i ). apply ( pr2 ( acommrng_amult A ) i' ). assert ( c * h * b * f * i * i' ~> a * f * d * h * i * i' ) as k. assert ( c * h * b * f * i * i' ~> c * b * i * f * h * i' ) as k0. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c h ) b ) f ) i ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c b ) i ) f ) h ) i' ). permute. rewrite k0. rewrite <- j. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a d ) i ) f ) h ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a f ) d ) h ) i ) i' ). permute. rewrite k in v. assert ( g * d * b * f * i * i' ~> e * b * d * h * i * i' ) as l. assert ( g * d * b * f * i * i' ~> g * f * i' * d * i * b ) as l0. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g d ) b ) f ) i ) i' ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g f ) i' ) d ) i ) b ). permute. rewrite l0. rewrite <- j'. change (@op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e h ) i' ) d ) i ) b ~> @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) h ) i ) i' ). permute. rewrite l in v. assumption. Defined. (** We now arrive at the apartness relation on the field of fractions itself.*) Definition afldfracapartrel := quotrel afldfracapartiscomprel. Lemma isirreflafldfracapartrelpre : isirrefl afldfracapartrelpre. Proof. intros ab. apply acommrng_airrefl. Defined. Lemma issymmafldfracapartrelpre : issymm afldfracapartrelpre. Proof. intros ab cd. apply ( acommrng_asymm A ). Defined. Lemma iscotransafldfracapartrelpre : iscotrans afldfracapartrelpre. Proof. intros ab cd ef p. destruct ab as [ a b ]. destruct b as [ b b' ]. destruct cd as [ c d ] . destruct d as [ d d' ] . destruct ef as [ e f ]. destruct f as [ f f' ]. assert ( a * f * d # e * b * d ) as v. apply azerormultcomp. assumption. assumption. apply ( ( acommrng_acotrans A ( a * f * d ) ( c * b * f ) ( e * b * d ) ) v ). intro u. intros P k. apply k. unfold afldfracapartrelpre in *. simpl in *. destruct u as [ left | right ]. apply ii1. apply ( pr2 ( acommrng_amult A ) f ). assert ( @op2 A ( @op2 A a f ) d ~> @op2 A ( @op2 A a d ) f ) as i. permute. change ( @op2 A ( @op2 A a d ) f # @op2 A ( @op2 A c b ) f ). rewrite <- i. assumption. apply ii2. apply ( pr2 ( acommrng_amult A ) b ). assert ( @op2 A ( @op2 A c f ) b ~> @op2 A ( @op2 A c b ) f ) as i. permute. change ( @op2 A ( @op2 A c f ) b # @op2 A ( @op2 A e d ) b ). rewrite i. assert ( @op2 A ( @op2 A e d ) b ~> @op2 A ( @op2 A e b ) d ) as j. permute. change ( @op2 A ( @op2 A c b ) f # @op2 A ( @op2 A e d ) b ). rewrite j. assumption. Defined. Lemma isapartafldfracapartrel : isapart afldfracapartrel. Proof. intros. split. apply isirreflquotrel. exact ( isirreflafldfracapartrelpre ). split. apply issymmquotrel. exact ( issymmafldfracapartrelpre ). apply iscotransquotrel. exact ( iscotransafldfracapartrelpre ). Defined. Definition afldfracapart : apart ( commrngfrac A (aintdomazerosubmonoid A)). Proof. intros. unfold apart. split with afldfracapartrel. exact isapartafldfracapartrel. Defined. Lemma isbinapartlafldfracop1 : isbinopapartl afldfracapart op1. Proof. intros. unfold isbinopapartl. assert ( forall a b c : commrngfrac A ( aintdomazerosubmonoid A ), isaprop ( pr1 (afldfracapart) ( commrngfracop1 A ( aintdomazerosubmonoid A ) a b) ( commrngfracop1 A ( aintdomazerosubmonoid A ) a c) -> pr1 (afldfracapart ) b c) ) as int. intros a b c. apply impred. intro p. apply ( pr1 ( afldfracapart ) b c ). apply ( setquotuniv3prop _ ( fun a b c => hProppair _ ( int a b c ) ) ). intros ab cd ef p. destruct ab as [ a b ]. destruct b as [ b b' ]. destruct cd as [ c d ]. destruct d as [ d d' ]. destruct ef as [ e f ]. destruct f as [ f f' ]. unfold afldfracapart in *. simpl. unfold afldfracapartrel. unfold quotrel. rewrite setquotuniv2comm. unfold afldfracapartrelpre. simpl. assert ( afldfracapartrelpre ( dirprodpair ( @op1 A ( @op2 A d a ) ( @op2 A b c ) ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair d d' ) ) ) ( dirprodpair ( @op1 A ( @op2 A f a ) ( @op2 A b e ) ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair f f' ) ) ) ) as u. apply p. unfold afldfracapartrelpre in u. simpl in u. rewrite 2! ( @rngrdistr A ) in u. repeat rewrite <- rngassoc2 in u. assert ( (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) d a) b) f) ~> (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) f a) b) d) ) as i. permute. rewrite i in u. assert ( (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) b c) b) f) ~> (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) c f) b) b) ) as j. permute. rewrite j in u. assert ( (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) b e) b) d) ~> (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (pr1rng (commrngtorng (acommrngtocommrng (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) e d) b) b) ) as j'. permute. rewrite j' in u. apply ( pr2 ( acommrng_amult A ) b ). apply ( pr2 ( acommrng_amult A ) b ). apply ( pr1 ( acommrng_aadd A) ( f * a * b * d ) ). assumption. Defined. Lemma isbinapartrafldfracop1 : isbinopapartr afldfracapart op1. Proof. intros a b c. rewrite ( rngcomm1 ). rewrite ( rngcomm1 _ c ). apply isbinapartlafldfracop1. Defined. Lemma isbinapartlafldfracop2 : isbinopapartl afldfracapart op2. Proof. intros. unfold isbinopapartl. assert ( forall a b c : commrngfrac A ( aintdomazerosubmonoid A ), isaprop ( pr1 (afldfracapart ) ( commrngfracop2 A ( aintdomazerosubmonoid A ) a b) ( commrngfracop2 A ( aintdomazerosubmonoid A ) a c) -> pr1 (afldfracapart ) b c) ) as int. intros a b c. apply impred. intro p. apply ( pr1 ( afldfracapart ) b c ). apply ( setquotuniv3prop _ ( fun a b c => hProppair _ ( int a b c ) ) ). intros ab cd ef p. destruct ab as [ a b ]. destruct b as [ b b' ]. destruct cd as [ c d ]. destruct d as [ d d' ]. destruct ef as [ e f ]. destruct f as [ f f' ]. assert ( afldfracapartrelpre ( dirprodpair ( ( a * c ) ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair d d' ) ) ) ( dirprodpair ( a * e ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair f f' ) ) ) ) as u. apply p. unfold afldfracapart in *. simpl. unfold afldfracapartrel. unfold quotrel. rewrite ( setquotuniv2comm ( eqrelcommrngfrac A ( aintdomazerosubmonoid A ) ) ). unfold afldfracapartrelpre in *. simpl. simpl in u. apply ( pr2 ( acommrng_amult A ) a ). apply ( pr2 ( acommrng_amult A ) b ). assert ( c * f * a * b ~> (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) a c) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) b f)) ) as i. change ( c * f * a * b ~> a * c * ( b * f ) ). permute. change ( c * f * a * b # e * d * a * b ). rewrite i. assert ( e * d * a * b ~> (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) a e) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommrngops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommrngtocommrng (pr1aintdom A))) b d)) ) as i'. change ( e * d * a * b ~> a * e * ( b * d ) ). permute. rewrite i'. assumption. Defined. Lemma isbinapartrafldfracop2 : isbinopapartr (afldfracapart ) op2. Proof. intros a b c. rewrite rngcomm2. rewrite ( rngcomm2 _ c ). apply isbinapartlafldfracop2. Defined. Definition afldfrac0 : acommrng. Proof. intros. split with ( commrngfrac A ( aintdomazerosubmonoid A ) ). split with ( afldfracapart ). split. split. apply ( isbinapartlafldfracop1 ). apply ( isbinapartrafldfracop1 ). split. apply ( isbinapartlafldfracop2 ). apply ( isbinapartrafldfracop2 ). Defined. Definition afldfracmultinvint ( ab : dirprod A ( aintdomazerosubmonoid A ) ) ( is : afldfracapartrelpre ab ( dirprodpair ( @rngunel1 A ) ( unel ( aintdomazerosubmonoid A ) )) ) : dirprod A ( aintdomazerosubmonoid A ). Proof. intros. destruct ab as [ a b ]. destruct b as [ b b' ]. split with b. simpl in is. split with a. unfold afldfracapartrelpre in is. simpl in is. change ( a # 0 ). rewrite ( @rngmult0x A ) in is. rewrite ( @rngrunax2 A ) in is. assumption. Defined. Definition afldfracmultinv ( a : afldfrac0 ) ( is : a # 0 ) : multinvpair afldfrac0 a. Proof. intros. assert ( forall b : afldfrac0, isaprop ( b # 0 -> multinvpair afldfrac0 b ) ) as int. intros. apply impred. intro p. apply ( isapropmultinvpair afldfrac0 ). assert ( forall b : afldfrac0, b # 0 -> multinvpair afldfrac0 b ) as p. apply ( setquotunivprop _ ( fun x0 => hProppair _ ( int x0 ) ) ). intros bc q. destruct bc as [ b c ]. assert ( afldfracapartrelpre ( dirprodpair b c ) ( dirprodpair ( @rngunel1 A ) ( unel ( aintdomazerosubmonoid A ) ) ) ) as is'. apply q. split with (setquotpr (eqrelcommrngfrac A (aintdomazerosubmonoid A)) ( afldfracmultinvint ( dirprodpair b c ) is' ) ). split. change ( setquotpr ( eqrelcommrngfrac A ( aintdomazerosubmonoid A ) ) ( dirprodpair ( @op2 A ( pr1 ( afldfracmultinvint ( dirprodpair b c ) is' ) ) b ) ( @op ( aintdomazerosubmonoid A ) ( pr2 ( afldfracmultinvint ( dirprodpair b c ) is' ) ) c ) ) ~> ( commrngfracunel2 A ( aintdomazerosubmonoid A ) ) ). apply iscompsetquotpr. unfold commrngfracunel2int. destruct c as [ c c' ]. simpl. apply total2tohexists. split with ( carrierpair ( fun x : pr1 A => x # 0 ) 1 ( pr1 ( pr2 A ) ) ). simpl. rewrite 3! ( @rngrunax2 A ). rewrite ( @rnglunax2 A ). apply ( @rngcomm2 A ). change ( setquotpr ( eqrelcommrngfrac A ( aintdomazerosubmonoid A ) ) ( dirprodpair ( @op2 A b ( pr1 ( afldfracmultinvint ( dirprodpair b c ) is' ) ) ) ( @op ( aintdomazerosubmonoid A ) c ( pr2 ( afldfracmultinvint ( dirprodpair b c ) is' ) ) ) ) ~> ( commrngfracunel2 A ( aintdomazerosubmonoid A ) ) ). apply iscompsetquotpr. destruct c as [ c c' ]. simpl. apply total2tohexists. split with ( carrierpair ( fun x : pr1 A => x # 0 ) 1 ( pr1 ( pr2 A ) ) ). simpl. rewrite 3! ( @rngrunax2 A ). rewrite ( @rnglunax2 A ). apply ( @rngcomm2 A ). apply p. assumption. Defined. Theorem afldfracisafld : isaafield afldfrac0. Proof. intros. split. change ( ( afldfracapartrel ) ( @rngunel2 ( commrngfrac A ( aintdomazerosubmonoid A ) ) ) ( @rngunel1 ( commrngfrac A ( aintdomazerosubmonoid A ) ) ) ). unfold afldfracapartrel. cut ( ( @op2 A ( @rngunel2 A ) ( @rngunel2 A ) ) # ( @op2 A ( @rngunel1 A ) ( @rngunel2 A ) ) ). intro v. apply v. rewrite 2! ( @rngrunax2 A ). apply A. intros a p. apply afldfracmultinv. assumption. Defined. Definition afldfrac := afldpair afldfrac0 afldfracisafld. End aint. Close Scope rng_scope. (** END OF FILE *)Pelayo-Coq/._lemmas.v000777 000765 000024 00000000324 12104265222 015323 0ustar00nicolastaff000000 000000 Mac OS X  2¢ÔATTRÔ˜<˜<com.apple.quarantineq/0002;53a854a1;Safari;5085629F-B604-4322-A539-1F4796CB8AB1Pelayo-Coq/lemmas.v000777 000765 000024 00000075635 12104265222 015127 0ustar00nicolastaff000000 000000 (** *Fixing notation, terminology and basic lemmas *) (** By Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren *) (** Settings *) Add Rec LoadPath "../Generalities". Add Rec LoadPath "../hlevel1". Add Rec LoadPath "../hlevel2". Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *) (** Imports *) Require Export hSet. Require Export hnat. Require Export hz. (*Require Export finitesets. Require Export stnfsets.*) (** Fixing some notation *) (** * Notation, terminology and very basic facts *) Notation "x ~> y" := ( paths x y ) ( at level 50 ) : type_scope. Implicit Arguments tpair [ T P ]. Lemma pathintotalfiber ( B : UU ) ( E : B -> UU ) ( b0 b1 : B ) ( e0 : E b0 ) ( e1 : E b1 ) ( p0 : b0 ~> b1 ) ( p1 : transportf E p0 e0 ~> e1 ) : ( tpair b0 e0 ) ~> ( tpair b1 e1 ). Proof. intros. destruct p0, p1. apply idpath. Defined. Definition neq ( X : UU0 ) : X -> X -> hProp := fun x y : X => hProppair (neg (x ~> y)) (isapropneg (x ~> y)). Definition pathintotalpr1 { B : UU } { E : B -> UU } { v w : total2 E } ( p : v ~> w ) : ( pr1 v ) ~> ( pr1 w ) := maponpaths ( fun x => pr1 x ) p. Lemma isinclisinj { A B : UU } { f : A -> B } ( p : isincl f ) { a b : A } ( p : f a ~> f b ) : a ~> b. Proof. intros. set ( q := p ( f a ) ). set ( a' := hfiberpair f a ( idpath ( f a ) ) ). set ( b' := hfiberpair f b ( pathsinv0 p0 ) ). assert ( a' ~> b' ) as p1. apply ( p ( f a ) ). apply ( pathintotalpr1 p1 ). Defined. (** * I. Lemmas on natural numbers *) Lemma minus0r ( n : nat ) : minus n 0 ~> n. Proof. intros n. destruct n. apply idpath. apply idpath. Defined. Lemma minusnn0 ( n : nat ) : minus n n ~> 0%nat. Proof. intro. induction n. apply idpath. assumption. Defined. Lemma minussn1 ( n : nat ) : minus ( S n ) 1 ~> n. Proof. intro. destruct n. apply idpath. apply idpath. Defined. Lemma minussn1non0 ( n : nat ) ( p : natlth 0 n ) : S ( minus n 1 ) ~> n. Proof. intro. destruct n. intro p. assert empty. exact ( isirreflnatlth 0%nat p ). contradiction. intro. apply maponpaths. apply minus0r. Defined. Lemma minusleh ( n m : nat ) : natleh ( minus n m ) n. Proof. intros n. induction n. intros m. apply isreflnatleh. intros m. destruct m. apply isreflnatleh. exact ( istransnatleh ( minus n m ) n ( S n ) ( IHn m ) ( natlthtoleh n ( S n ) ( natlthnsn n ) ) ). Defined. Lemma minus1leh { n m : nat } ( p : natlth 0 n ) ( q : natlth 0 m ) ( r : natleh n m ) : natleh ( minus n 1 ) ( minus m 1 ). Proof. intro n. destruct n. auto. intros m p q r. destruct m. assert empty. exact ( isirreflnatlth 0%nat q ). contradiction. assert ( natleh n m ) as a. apply r. assert ( natleh ( minus n 0%nat ) m ) as a0. exact ( transportf ( fun x : nat => natleh x m ) ( pathsinv0 ( minus0r n ) ) a ). exact ( transportf ( fun x : nat => natleh ( minus n 0 ) x ) ( pathsinv0 ( minus0r m ) ) a0 ). Defined. Lemma minuslth ( n m : nat ) ( p : natlth 0 n ) ( q : natlth 0 m ) : natlth ( minus n m ) n. Proof. intro n. destruct n. auto. intros m p q. destruct m. assert empty. exact ( isirreflnatlth 0%nat q ). contradiction. apply ( natlehlthtrans _ n _ ). apply ( minusleh n m ). apply natlthnsn. Defined. Lemma natlthsntoleh ( n m : nat ) : natlth m ( S n ) -> natleh m n. Proof. intro. induction n. intros m p. destruct m. apply isreflnatleh. assert ( natlth m 0 ) as q. apply p. intro. unfold natlth in q. exact ( negnatgth0n m q ). intros m p. destruct m. apply natleh0n. apply ( IHn m ). assumption. Defined. Lemma natlthminus0 { n m : nat } ( p : natlth m n ) : natlth 0 ( minus n m ). Proof. intro n. induction n. intros m p. assert empty. exact ( negnatlthn0 m p ). contradiction. intros m p. destruct m. auto. apply IHn. apply p. Defined. Lemma natlthsnminussmsn ( n m : nat ) ( p : natlth m n ) : natlth ( minus ( S n ) ( S m ) ) ( S n ). Proof. intro. induction n. intros m p. assert empty. apply nopathsfalsetotrue. assumption. contradiction. intros m p. destruct m. assert ( minus ( S ( S n ) ) 1 ~> S n ) as f. destruct n. auto. auto. rewrite f. apply natlthnsn. apply ( istransnatlth _ ( S n ) _ ). apply IHn. assumption. apply natlthnsn. Defined. Lemma natlehsnminussmsn ( n m : nat ) ( p : natleh m n ) : natleh ( minus ( S n ) ( S m ) ) ( S n ). Proof. intro n. induction n. intros m p X. assert empty. apply nopathsfalsetotrue. assumption. assumption. intros m p. destruct m. apply natlthtoleh. apply natlthnsn. apply ( istransnatleh _ ( S n ) _ ). apply IHn. assumption. apply natlthtoleh. apply natlthnsn. Defined. Lemma pathssminus ( n m : nat ) ( p : natlth m ( S n ) ) : S ( minus n m ) ~> minus ( S n ) m. Proof. intro n. induction n. intros m p. destruct m. auto. assert empty. apply nopathstruetofalse. apply pathsinv0. assumption. contradiction. intros m p. destruct m. auto. apply IHn. apply p. Defined. Lemma natlehsminus ( n m : nat ) : natleh ( minus ( S n ) m ) ( S ( minus n m ) ). Proof. intro n. induction n. intros m X. apply nopathstruetofalse. apply pathsinv0. destruct m. assumption. assumption. intros m. destruct m. apply isreflnatleh. apply IHn. Defined. Lemma natlthssminus { n m l : nat } ( p : natlth m ( S n ) ) ( q : natlth l ( S ( minus ( S n ) m ) ) ) : natlth l ( S ( S n ) ). Proof. intro n. intros m l p q. apply ( natlthlehtrans _ ( S ( minus ( S n ) m ) ) ). assumption. destruct m. apply isreflnatleh. apply natlthtoleh. apply natlthsnminussmsn. assumption. Defined. Lemma natdoubleminus { n k l : nat } ( p : natleh k n ) ( q : natleh l k ) : ( minus n k) ~> ( minus ( minus n l ) ( minus k l ) ). Proof. intro n. induction n. auto. intros k l p q. destruct k. destruct l. auto. assert empty. exact ( negnatlehsn0 l q ). contradiction. destruct l. auto. apply ( IHn k l ). assumption. assumption. Defined. Lemma minusnleh1 ( n m : nat ) ( p : natlth m n ) : natleh m ( minus n 1 ). Proof. intro n. destruct n. intros m p. assert empty. exact ( negnatlthn0 m p ). contradiction. intros m p. destruct m. apply natleh0n. apply natlthsntoleh. change ( minus ( S n ) 1 ) with ( minus n 0 ). rewrite minus0r. assumption. Defined. Lemma doubleminuslehpaths ( n m : nat ) ( p : natleh m n ) : minus n ( minus n m ) ~> m. Proof. intro n. induction n. intros m p. destruct ( natlehchoice m 0 p ) as [ h | k ]. assert empty. apply negnatlthn0 with ( n := m ). assumption. contradiction. simpl. apply pathsinv0. assumption. intros. destruct m. simpl. apply minusnn0. change ( minus ( S n ) ( minus n m ) ~> S m ). rewrite <- pathssminus. rewrite IHn. apply idpath. assumption. apply ( minuslth ( S n ) ( S m ) ). apply ( natlehlthtrans _ n ). apply natleh0n. apply natlthnsn. apply ( natlehlthtrans _ m ). apply natleh0n. apply natlthnsn. Defined. Lemma boolnegtrueimplfalse ( v : bool ) ( p : neg ( v ~> true ) ) : v ~> false. Proof. intros. destruct v. assert empty. apply p. auto. contradiction. auto. Defined. Definition natcoface ( i : nat ) : nat -> nat. Proof. intros i n. destruct ( natgtb i n ). exact n. exact ( S n ). Defined. Lemma natcofaceleh ( i n upper : nat ) ( p : natleh n upper ) : natleh ( natcoface i n ) ( S upper ). Proof. intros. unfold natcoface. destruct ( natgtb i n ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). assumption. apply natlthnsn. apply p. Defined. Lemma natgehimplnatgtbfalse ( m n : nat ) ( p : natgeh n m ) : natgtb m n ~> false. Proof. intros. unfold natgeh in p. unfold natgth in p. apply boolnegtrueimplfalse. intro q. apply p. auto. Defined. Definition natcofaceretract ( i : nat ) : nat -> nat. Proof. intros i n. destruct ( natgtb i n ). exact n. exact ( minus n 1 ). Defined. Lemma natcofaceretractisretract ( i : nat ) : funcomp ( natcoface i ) ( natcofaceretract i ) ~> idfun nat. Proof. intro i. apply funextfun. intro n. unfold funcomp. set ( c := natlthorgeh n i ). destruct c as [ h | k ]. unfold natcoface. rewrite h. unfold natcofaceretract. rewrite h. apply idpath. assert ( natgtb i n ~> false ) as f. apply natgehimplnatgtbfalse. assumption. unfold natcoface. rewrite f. unfold natcofaceretract. assert ( natgtb i ( S n ) ~> false ) as ff. apply natgehimplnatgtbfalse. apply ( istransnatgeh _ n ). apply natgthtogeh. apply natgthsnn. assumption. rewrite ff. rewrite minussn1. apply idpath. Defined. Lemma isinjnatcoface ( i x y : nat ) : natcoface i x ~> natcoface i y -> x ~> y. Proof. intros i x y p. change x with ( ( idfun _ ) x ). rewrite <- ( natcofaceretractisretract i ). change y with ( ( idfun _ ) y ). rewrite <- ( natcofaceretractisretract i ). unfold funcomp. rewrite p. apply idpath. Defined. Lemma natlehdecomp ( b a : nat ) : hexists ( fun c : nat => ( a + c )%nat ~> b ) -> natleh a b. Proof. intro b. induction b. intros a p. apply p. intro t. destruct t as [ c f ]. destruct a. apply isreflnatleh. assert empty. simpl in f . exact ( negpathssx0 ( a + c ) f ). contradiction. intros a p. apply p. intro t. destruct t as [ c f ]. destruct a. apply natleh0n. assert ( natleh a b ) as q. simpl in f. apply IHb. intro P. intro s. apply s. split with c. apply invmaponpathsS. assumption. apply q. Defined. Lemma natdivleh ( a b k : nat ) ( f : ( a * k )%nat ~> b ) : coprod ( natleh a b ) ( b ~> 0%nat ). Proof. intros. destruct k. rewrite natmultcomm in f. simpl in f. apply ii2. apply pathsinv0. assumption. rewrite natmultcomm in f. simpl in f. apply ii1. apply natlehdecomp. intro P. intro g. apply g. split with ( k * a )%nat. assumption. Defined. (** * II. Lemmas on rings *) Open Scope rng_scope. Lemma rngminusdistr { X : commrng } ( a b c : X ) : a * (b - c) ~> (a * b - a * c). Proof. intros. rewrite rngldistr. rewrite rngrmultminus. apply idpath. Defined. Lemma rngminusdistl { X : commrng } ( a b c : X ) : (b - c) * a ~> (b * a - c * a). Proof. intros. rewrite rngrdistr. rewrite rnglmultminus. apply idpath. Defined. Lemma multinvmultstable ( A : commrng ) ( a b : A ) ( p : multinvpair A a ) ( q : multinvpair A b ) : multinvpair A ( a * b ). Proof. intros. destruct p as [ a' p ]. destruct q as [ b' q ]. split with ( b' * a' ). split. change ( ( ( b' * a' ) * ( a * b ) )%rng ~> ( @rngunel2 A )). rewrite ( rngassoc2 A b'). rewrite <- ( rngassoc2 A a' ). change ( dirprod ( ( a' * a )%rng ~> ( @rngunel2 A ) ) ( ( a * a' )%rng ~> ( @rngunel2 A ) ) ) in p. change ( dirprod ( ( b' * b )%rng ~> ( @rngunel2 A ) ) ( ( b * b' )%rng ~> ( @rngunel2 A ) ) ) in q. rewrite <- ( pr1 q ). apply maponpaths. assert ( a' * a * b ~> 1 * b ) as f. apply ( maponpaths ( fun x => x * b ) ( pr1 p ) ). rewrite rnglunax2 in f. assumption. change ( ( ( a * b ) * ( b' * a' ) )%rng ~> ( @rngunel2 A )). rewrite ( rngassoc2 A a). rewrite <- ( rngassoc2 A b ). change ( dirprod ( ( a' * a )%rng ~> ( @rngunel2 A ) ) ( ( a * a' )%rng ~> ( @rngunel2 A ) ) ) in p. change ( dirprod ( ( b' * b )%rng ~> ( @rngunel2 A ) ) ( ( b * b' )%rng ~> ( @rngunel2 A ) ) ) in q. rewrite <- ( pr2 q ). rewrite ( pr2 q ). rewrite rnglunax2. apply p. Defined. Lemma commrngaddinvunique ( X : commrng ) ( a b c : X ) ( p : @op1 X a b ~> @rngunel1 X ) ( q : @op1 X a c ~> @rngunel1 X ) : b ~> c. Proof. intros. rewrite ( pathsinv0 ( rngrunax1 X b ) ). rewrite ( pathsinv0 q ). rewrite ( pathsinv0 ( rngassoc1 X _ _ _ ) ). rewrite ( rngcomm1 X b _ ). rewrite p. rewrite rnglunax1. apply idpath. Defined. Lemma isapropmultinvpair ( X : commrng ) ( a : X ) : isaprop ( multinvpair X a ). Proof. intros. unfold isaprop. intros b c. assert ( b ~> c ) as f. destruct b as [ b b' ]. destruct c as [ c c' ]. assert ( b ~> c ) as f0. rewrite <- ( @rngrunax2 X b ). change ( b * ( @rngunel2 X ) ) with ( b * 1 )%multmonoid. rewrite <- ( pr2 c' ). change ( ( b * ( a * c ) )%rng ~> c ). rewrite <- ( rngassoc2 X ). change ( b * a )%rng with ( b * a )%multmonoid. rewrite ( pr1 b' ). change ( ( @rngunel2 X ) * c ~> c )%rng. apply rnglunax2. apply pathintotalfiber with ( p0 := f0 ). assert ( isaprop ( dirprod (c * a ~> ( @rngunel2 X ) ) (a * c ~> ( @rngunel2 X )) ) ) as is. apply isofhleveldirprod. apply ( setproperty X ). apply ( setproperty X ). apply is. split with f. intros g. assert ( isaset ( multinvpair X a ) ) as is. unfold multinvpair. unfold invpair. change isaset with ( isofhlevel 2 ). apply isofhleveltotal2. apply ( pr1 ( pr1 ( rigmultmonoid X ) ) ). intros. apply isofhleveldirprod. apply hlevelntosn. apply ( setproperty X ). apply hlevelntosn. apply ( setproperty X ). apply is. Defined. Close Scope rng_scope. (** * III. Lemmas on hz *) Open Scope hz_scope. Lemma hzaddinvplus ( n m : hz ) : - ( n + m ) ~> ( ( - n ) + ( - m ) ). Proof. intros. apply commrngaddinvunique with ( a := n + m ). apply rngrinvax1. assert ( ( n + m ) + ( - n + - m ) ~> ( n + - n + m + - m ) ) as i. assert ( n + m + ( - n + - m ) ~> ( n + ( m + ( - n + - m ) ) ) ) as i0. apply rngassoc1. assert ( n + ( m + ( - n + - m ) ) ~> ( n + ( m + - n + - m ) ) ) as i1. apply maponpaths. apply pathsinv0. apply rngassoc1. assert ( n + ( m + - n + - m ) ~> ( n + ( - n + m + - m ) ) ) as i2. apply maponpaths. apply ( maponpaths ( fun x : _ => x + - m ) ). apply rngcomm1. assert ( n + ( - n + m + - m ) ~> ( n + ( - n + m ) + - m ) ) as i3. apply pathsinv0. apply rngassoc1. assert ( n + ( - n + m ) + - m ~> ( n + - n + m + - m ) ) as i4. apply pathsinv0. apply ( maponpaths ( fun x : _ => x + - m ) ). apply rngassoc1. exact ( pathscomp0 i0 ( pathscomp0 i1 ( pathscomp0 i2 ( pathscomp0 i3 i4 ) ) ) ). assert ( n + - n + m + -m ~> 0 ) as j. assert ( n + - n + m + - m ~> ( 0 + m + - m ) ) as j0. apply ( maponpaths ( fun x : _ => x + m + - m ) ). apply rngrinvax1. assert ( 0 + m + - m ~> ( m + - m ) ) as j1. apply ( maponpaths ( fun x : _ => x + - m ) ). apply rnglunax1. assert ( m + - m ~> 0 ) as j2. apply rngrinvax1. exact ( pathscomp0 j0 ( pathscomp0 j1 j2 ) ). exact ( pathscomp0 i j ). Defined. Lemma hzgthsntogeh ( n m : hz ) ( p : hzgth ( n + 1 ) m ) : hzgeh n m. Proof. intros. set ( c := hzgthchoice2 ( n + 1 ) m ). destruct c as [ h | k ]. exact p. assert ( hzgth n m ) as a. exact ( hzgthandplusrinv n m 1 h ). apply hzgthtogeh. exact a. rewrite ( hzplusrcan n m 1 k ). apply isreflhzgeh. Defined. Lemma hzlthsntoleh ( n m : hz ) ( p : hzlth m ( n + 1 ) ) : hzleh m n. Proof. intros. unfold hzlth in p. assert ( hzgeh n m ) as a. apply hzgthsntogeh. exact p. exact a. Defined. Lemma hzabsvalchoice ( n : hz ) : coprod ( 0%nat ~> ( hzabsval n ) ) ( total2 ( fun x : nat => S x ~> ( hzabsval n ) ) ). Proof. intros. destruct ( natlehchoice _ _ ( natleh0n ( hzabsval n ) ) ) as [ l | r ]. apply ii2. split with ( minus ( hzabsval n ) 1 ). rewrite pathssminus. change ( minus ( hzabsval n ) 0 ~> hzabsval n ). rewrite minus0r. apply idpath. assumption. apply ii1. assumption. Defined. Lemma hzlthminusswap ( n m : hz ) ( p : hzlth n m ) : hzlth ( - m ) ( - n ). Proof. intros. rewrite <- ( hzplusl0 ( - m ) ). rewrite <- ( hzrminus n ). change ( hzlth ( n + - n + - m ) ( - n ) ). rewrite hzplusassoc. rewrite ( hzpluscomm ( -n ) ). rewrite <- hzplusassoc. assert ( - n ~> ( 0 + - n ) ) as f. apply pathsinv0. apply hzplusl0. assert ( hzlth ( n + - m + - n ) ( 0 + - n ) ) as q. apply hzlthandplusr. rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). apply hzlthandplusr. assumption. rewrite <- f in q. assumption. Defined. Lemma hzlthminusequiv ( n m : hz ) : dirprod ( ( hzlth n m ) -> ( hzlth 0 ( m - n ) ) ) ( ( hzlth 0 ( m - n ) ) -> ( hzlth n m ) ). Proof. intros. rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). change ( m - n ) with ( m + - n ). split. intro p. apply hzlthandplusr. assumption. intro p. rewrite <- ( hzplusr0 n ). rewrite <- ( hzplusr0 m ). rewrite <- ( hzlminus n ). rewrite <- 2! hzplusassoc. apply hzlthandplusr. assumption. Defined. Lemma hzlthminus ( n m k : hz ) ( p : hzlth n k ) ( q : hzlth m k ) ( q' : hzleh 0 m ) : hzlth ( n - m ) k. Proof. intros. destruct ( hzlehchoice 0 m q' ) as [ l | r ]. apply ( istranshzlth _ n _ ). assert ( hzlth ( n - m ) ( n + 0 ) ) as i0. rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). rewrite <- ( hzplusassoc ). apply hzlthandplusr. assert ( hzlth ( n + 0 ) ( n + m ) ) as i00. apply hzlthandplusl. assumption. rewrite ( hzplusr0 ) in i00. assumption. rewrite hzplusr0 in i0. assumption. assumption. rewrite <- r. change ( n - 0 ) with ( n + - 0 ). rewrite hzminuszero. rewrite ( hzplusr0 n ). assumption. Defined. Lemma hzabsvalandminuspos ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) : nattohz ( hzabsval ( n - m ) ) ~> nattohz ( hzabsval ( m - n ) ). Proof. intros. destruct ( hzlthorgeh n m ) as [ l | r ]. assert ( hzlth ( n - m ) 0 ) as a. change ( n - m ) with ( n + - m ). rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). apply ( hzlthandplusr ). assumption. assert ( hzlth 0 ( m - n ) ) as b. change ( m - n ) with ( m + - n ). rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). apply hzlthandplusr. assumption. rewrite ( hzabsvallth0 a ). rewrite hzabsvalgth0. change ( n - m ) with ( n + - m ). rewrite hzaddinvplus. change ( - - m ) with ( - - m )%rng. rewrite ( rngminusminus ). rewrite hzpluscomm. apply idpath. apply b. destruct ( hzgehchoice n m r ) as [ h | k ]. assert ( hzlth 0 ( n - m ) ) as a. change ( n - m ) with ( n + - m ). rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). apply hzlthandplusr. assumption. assert ( hzlth ( m - n ) 0 ) as b. change ( m - n ) with ( m + - n ). rewrite <- ( hzrminus n ). apply hzlthandplusr. apply h. rewrite ( hzabsvallth0 b ). rewrite ( hzabsvalgth0 ). change ( ( n + - m ) ~> - ( m + - n ) ). rewrite hzaddinvplus. change ( - - n ) with ( - - n )%rng. rewrite rngminusminus. rewrite hzpluscomm. apply idpath. apply a. rewrite k. apply idpath. Defined. Lemma hzabsvalneq0 ( n : hz ) ( p : hzneq 0 n ) : hzlth 0 ( nattohz ( hzabsval n ) ). Proof. intros. destruct ( hzneqchoice 0 n p ) as [ left | right ]. rewrite hzabsvallth0. apply hzlth0andminus. apply left. apply left. rewrite hzabsvalgth0. assumption. apply right. Defined. Definition hzrdistr ( a b c : hz ) : ( a + b ) * c ~> ( ( a * c ) + ( b * c ) ) := rngrdistr hz a b c. Definition hzldistr ( a b c : hz ) : c * ( a + b ) ~> ( ( c * a ) + ( c * b ) ) := rngldistr hz a b c. Lemma hzabsvaland1 : hzabsval 1 ~> 1%nat. Proof. apply ( isinclisinj isinclnattohz ). rewrite hzabsvalgth0. rewrite nattohzand1. apply idpath. rewrite <- ( hzplusl0 1). apply ( hzlthnsn 0 ). Defined. Lemma hzabsvalandplusnonneg ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) : hzabsval ( n + m ) ~> ( ( hzabsval n ) + ( hzabsval m ) )%nat. Proof. intros. assert ( hzleh 0 ( n + m ) ) as r. rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). apply hzlehandplusl. apply ( istranshzleh _ 0 _ ). apply hzgeh0andminus. apply p. assumption. apply ( isinclisinj isinclnattohz ). rewrite nattohzandplus. rewrite 3! hzabsvalgeh0. apply idpath. apply q. apply p. apply r. Defined. Lemma hzabsvalandplusneg ( n m : hz ) ( p : hzlth n 0 ) ( q : hzlth m 0 ) : hzabsval ( n + m ) ~> ( ( hzabsval n ) + ( hzabsval m ) )%nat. Proof. intros. assert ( hzlth ( n + m ) 0 ) as r. rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). apply hzlthandplusl. apply ( istranshzlth _ 0 _ ). assumption. apply hzlth0andminus. assumption. apply ( isinclisinj isinclnattohz ). rewrite nattohzandplus. rewrite 3! hzabsvallth0. rewrite hzaddinvplus. apply idpath. apply q. apply p. apply r. Defined. Lemma hzabsvalandnattohz ( n : nat ) : hzabsval ( nattohz n ) ~> n. Proof. induction n. rewrite nattohzand0. rewrite hzabsval0. apply idpath. rewrite nattohzandS. rewrite hzabsvalandplusnonneg. rewrite hzabsvaland1. simpl. apply maponpaths. assumption. rewrite <- ( hzplusl0 1). apply hzlthtoleh. apply ( hzlthnsn 0 ). rewrite <- nattohzand0. apply nattohzandleh. apply natleh0n. Defined. Lemma hzabsvalandlth ( n m : hz ) ( p : hzleh 0 n ) ( p' : hzlth n m ) : natlth ( hzabsval n ) ( hzabsval m ). Proof. intros. destruct ( natlthorgeh ( hzabsval n ) ( hzabsval m ) ) as [ h | k ]. assumption. assert empty. apply ( isirreflhzlth m ). apply ( hzlehlthtrans _ n _ ). rewrite <- ( hzabsvalgeh0 ). rewrite <- ( hzabsvalgeh0 p ). apply nattohzandleh. apply k. apply hzgthtogeh. apply ( hzgthgehtrans _ n _ ). apply p'. apply p. assumption. contradiction. Defined. Lemma nattohzandlthinv ( n m : nat ) ( p : hzlth ( nattohz n ) (nattohz m ) ) : natlth n m. Proof. intros. rewrite <- ( hzabsvalandnattohz n ). rewrite <- ( hzabsvalandnattohz m ). apply hzabsvalandlth. change 0 with ( nattohz 0%nat ). apply nattohzandleh. apply natleh0n . assumption. Defined. Close Scope hz_scope. (** * IV. Generalities on apartness relations *) Definition iscomparel { X : UU0 } ( R : hrel X ) := forall x y z : X, R x y -> coprod ( R x z ) ( R z y ). Definition isapart { X : UU0 } ( R : hrel X ) := dirprod ( isirrefl R ) ( dirprod ( issymm R ) ( iscotrans R ) ). Definition istightapart { X : UU0 } ( R : hrel X ) := dirprod ( isapart R ) ( forall x y : X, neg ( R x y ) -> ( x ~> y ) ). Definition apart ( X : hSet ) := total2 ( fun R : hrel X => isapart R ). Definition isbinopapartl { X : hSet } ( R : apart X ) ( opp : binop X ) := forall a b c : X, ( ( pr1 R ) ( opp a b ) ( opp a c ) ) -> ( pr1 R ) b c. Definition isbinopapartr { X : hSet } ( R : apart X ) ( opp : binop X ) := forall a b c : X, ( pr1 R ) ( opp b a ) ( opp c a ) -> ( pr1 R ) b c. Definition isbinopapart { X : hSet } ( R : apart X ) ( opp : binop X ) := dirprod ( isbinopapartl R opp ) ( isbinopapartr R opp ). Lemma deceqtoneqapart { X : UU0 } ( is : isdeceq X ) : isapart ( neq X ). Proof. intros. split. intros a. intro p. apply p. apply idpath. split. intros a b p q. apply p. apply pathsinv0. assumption. intros a c b p P s. apply s. destruct ( is a c ) as [ l | r ]. apply ii2. rewrite <- l. assumption. apply ii1. assumption. Defined. Definition isapartdec { X : hSet } ( R : apart X ) := forall a b : X, coprod ( ( pr1 R ) a b ) ( a ~> b ). Lemma isapartdectodeceq { X : hSet } ( R : apart X ) ( is : isapartdec R ) : isdeceq X. Proof. intros X R is y z. destruct ( is y z ) as [ l | r ]. apply ii2. intros f. apply ( ( pr1 ( pr2 R ) ) z). rewrite f in l. assumption. apply ii1. assumption. Defined. Lemma isdeceqtoisapartdec ( X : hSet ) ( is : isdeceq X ) : isapartdec ( tpair _ ( deceqtoneqapart is ) ). Proof. intros X is a b. destruct ( is a b ) as [ l | r ]. apply ii2. assumption. apply ii1. intros f. apply r. assumption. Defined. (** * V. Apartness relations on rings *) Open Scope rng_scope. Definition acommrng := total2 ( fun X : commrng => total2 ( fun R : apart X => dirprod ( isbinopapart R ( @op1 X ) ) ( isbinopapart R ( @op2 X ) ) ) ). Definition acommrngpair := tpair ( P := fun X : commrng => total2 ( fun R : apart X => dirprod ( isbinopapart R ( @op1 X ) ) ( isbinopapart R ( @op2 X ) ) ) ). Definition acommrngconstr := acommrngpair. Definition acommrngtocommrng : acommrng -> commrng := @pr1 _ _. Coercion acommrngtocommrng : acommrng >-> commrng. Definition acommrngapartrel ( X : acommrng ) := pr1 ( pr1 ( pr2 X ) ). Notation " a # b " := ( acommrngapartrel _ a b ) ( at level 50 ) : rng_scope. Definition acommrng_aadd ( X : acommrng ) : isbinopapart ( pr1 ( pr2 X ) ) op1 := ( pr1 ( pr2 ( pr2 X ) ) ). Definition acommrng_amult ( X : acommrng ) : isbinopapart ( pr1 ( pr2 X ) ) op2 := ( pr2 ( pr2 ( pr2 X ) ) ). Definition acommrng_airrefl ( X : acommrng ) : isirrefl ( pr1 ( pr1 ( pr2 X ) ) ) := pr1 ( pr2 ( pr1 ( pr2 X ) ) ). Definition acommrng_asymm ( X : acommrng ) : issymm ( pr1 ( pr1 ( pr2 X ) ) ) := pr1 ( pr2 ( pr2 ( pr1 ( pr2 X ) ) ) ). Definition acommrng_acotrans ( X : acommrng ) : iscotrans ( pr1 ( pr1 ( pr2 X ) ) ) := pr2 ( pr2 ( pr2 ( pr1 ( pr2 X ) ) ) ). Definition aintdom := total2 ( fun A : acommrng => dirprod ( ( rngunel2 ( X := A ) ) # 0 ) ( forall a b : A, ( a # 0 ) -> ( b # 0 ) -> ( ( a * b ) # 0 ) ) ). Definition aintdompair := tpair ( P := fun A : acommrng => dirprod ( ( rngunel2 ( X := A ) ) # 0 ) ( forall a b : A, ( a # 0 ) -> ( b # 0 ) -> ( ( a * b ) # 0 ) ) ). Definition aintdomconstr := aintdompair. Definition pr1aintdom : aintdom -> acommrng := @pr1 _ _. Coercion pr1aintdom : aintdom >-> acommrng. Definition aintdomazerosubmonoid ( A : aintdom ) : @subabmonoids ( rngmultabmonoid A ). Proof. intros. split with ( fun x : A => ( x # 0 ) ). split. intros a b. simpl in *. apply A. apply a. apply b. apply A. Defined. Definition isaafield ( A : acommrng ) := dirprod ( ( rngunel2 ( X := A ) ) # 0 ) ( forall x : A, x # 0 -> multinvpair A x ). Definition afld := total2 ( fun A : acommrng => isaafield A ). Definition afldpair ( A : acommrng ) ( is : isaafield A ) : afld := tpair A is . Definition pr1afld : afld -> acommrng := @pr1 _ _ . Coercion pr1afld : afld >-> acommrng. Lemma afldinvertibletoazero ( A : afld ) ( a : A ) ( p : multinvpair A a ) : a # 0. Proof. intros. destruct p as [ a' p ]. assert ( a' * a # 0 ) as q. change ( a' * a # 0 ). assert ( a' * a ~> a * a' ) as f. apply ( rngcomm2 A ). assert ( a * a' ~> 1 ) as g. apply p. rewrite f, g. apply A. assert ( a' * a # a' * ( rngunel1 ( X := A ) ) ) as q'. assert ( ( rngunel1 ( X := A ) ) ~> ( a' * ( rngunel1 ( X := A ) ) ) ) as f. apply pathsinv0. apply ( rngmultx0 A ). rewrite <- f. assumption. apply ( ( pr1 ( acommrng_amult A ) ) a' ). assumption. Defined. Definition afldtoaintdom ( A : afld ) : aintdom . Proof. intro . split with ( pr1 A ) . split. apply A. intros a b p q. apply afldinvertibletoazero. apply multinvmultstable. apply A. assumption. apply A. assumption. Defined. Lemma timesazero { A : acommrng } { a b : A } ( p : a * b # 0 ) : dirprod ( a # 0 ) ( b # 0 ). Proof. intros. split. assert ( a * b # 0 * b ) as h. rewrite ( rngmult0x A ). assumption. apply ( ( pr2 ( acommrng_amult A ) ) b ). assumption. apply ( ( pr1 ( acommrng_amult A ) ) a ). rewrite ( rngmultx0 A ). assumption. Defined. Lemma aaminuszero { A : acommrng } { a b : A } ( p : a # b ) : ( a - b ) # 0. Proof. intros. rewrite <- ( rngrunax1 A a ) in p. rewrite <- ( rngrunax1 A b ) in p. assert ( a + 0 ~> ( a + ( b - b ) ) ) as f. rewrite <- ( rngrinvax1 A b ). apply idpath. rewrite f in p. rewrite <- ( rngmultwithminus1 A ) in p. rewrite <- ( rngassoc1 A) in p. rewrite ( rngcomm1 A a ) in p. rewrite ( rngassoc1 A b ) in p. rewrite ( rngmultwithminus1 A ) in p. apply ( ( pr1 ( acommrng_aadd A ) ) b ( a - b ) 0 ). assumption. Defined. Lemma aminuszeroa { A : acommrng } { a b : A } ( p : ( a - b ) # 0 ) : a # b. Proof. intros. change 0 with ( @rngunel1 A ) in p. rewrite <- ( rngrinvax1 A b ) in p. rewrite <- ( rngmultwithminus1 A ) in p. apply ( ( pr2 ( acommrng_aadd A ) ) ( -1 * b ) a b ). assumption. Defined. Close Scope rng_scope. (** * VI. Lemmas on logic *) Lemma horelim ( A B : UU0 ) ( P : hProp ) : dirprod ( ishinh_UU A -> P ) ( ishinh_UU B -> P ) -> ( hdisj A B -> P ). Proof. intros A B P p. intro q. apply q. intro u. destruct u as [ u | v ]. apply ( pr1 p ). intro Q. auto. apply ( pr2 p ). intro Q. auto. Defined. Lemma stronginduction { E : nat -> UU } ( p : E 0%nat ) ( q : forall n : nat, natneq n 0%nat -> ( ( forall m : nat, natlth m n -> E m ) -> E n ) ) : forall n : nat, E n. Proof. intros. destruct n. assumption. apply q. apply ( negpathssx0 n ). induction n. intros m t. rewrite ( natlth1tois0 m t ). assumption. intros m t. destruct ( natlehchoice _ _ ( natlthsntoleh _ _ t ) ) as [ left | right ]. apply IHn. assumption. apply q. rewrite right. intro f. apply ( negpathssx0 n ). assumption. intros k s. rewrite right in s. apply ( IHn k ). assumption. Defined. Lemma setquotprpathsandR { X : UU0 } ( R : eqrel X ) : forall x y : X, setquotpr R x ~> setquotpr R y -> R x y. Proof. intros. assert ( pr1 ( setquotpr R x ) y ) as i. assert ( pr1 ( setquotpr R y ) y ) as i0. unfold setquotpr. apply R. destruct X0. assumption. apply i. Defined. (* Some lemmas on decidable properties of natural numbers. *) Definition isdecnatprop ( P : nat -> hProp ) := forall m : nat, coprod ( P m ) ( neg ( P m ) ). Lemma negisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) : isdecnatprop ( fun n : nat => hneg ( P n ) ). Proof. intros P is n. destruct ( is n ) as [ l | r ]. apply ii2. intro j. assert hfalse as x. apply j. assumption. apply x. apply ii1. assumption. Defined. Lemma bndexistsisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) : isdecnatprop ( fun n : nat => hexists ( fun m : nat => dirprod ( natleh m n ) ( P m ) ) ). Proof. intros P is n. induction n. destruct ( is 0%nat ) as [ l | r ]. apply ii1. apply total2tohexists. split with 0%nat. split. apply isreflnatleh. assumption. apply ii2. intro j. assert hfalse as x. apply j. intro m. destruct m as [ m m' ]. apply r. rewrite ( natleh0tois0 m ( pr1 m' ) ) in m'. apply m'. apply x. destruct ( is ( S n ) ) as [ l | r ]. apply ii1. apply total2tohexists. split with ( S n ). split. apply ( isreflnatleh ( S n ) ). assumption. destruct IHn as [ l' | r' ]. apply ii1. apply l'. intro m. destruct m as [ m m' ]. apply total2tohexists. split with m. split. apply ( istransnatleh _ n _ ). apply m'. apply natlthtoleh. apply natlthnsn. apply m'. apply ii2. intro j. apply r'. apply j. intro m. destruct m as [ m m' ]. apply total2tohexists. split with m. split. destruct ( natlehchoice m ( S n ) ( pr1 m' ) ). apply natlthsntoleh. assumption. assert empty. apply r. rewrite <- i. apply m'. contradiction. apply m'. Defined. Lemma isdecisbndqdec ( P : nat -> hProp ) ( is : isdecnatprop P ) ( n : nat ) : coprod ( forall m : nat, natleh m n -> P m ) ( hexists ( fun m : nat => dirprod ( natleh m n ) ( neg ( P m ) ) ) ). Proof. intros P is n. destruct ( bndexistsisdecnatprop _ ( negisdecnatprop P is ) n ) as [ l | r ]. apply ii2. assumption. apply ii1. intros m j. destruct ( is m ) as [ l' | r' ]. assumption. assert hfalse as x. apply r. apply total2tohexists. split with m. split. assumption. assumption. contradiction. Defined. Lemma leastelementprinciple ( n : nat ) ( P : nat -> hProp ) ( is : isdecnatprop P ) : P n -> hexists ( fun k : nat => dirprod ( P k ) ( forall m : nat, natlth m k -> neg ( P m ) ) ). Proof. intro n. induction n. intros P is u. apply total2tohexists. split with 0%nat. split. assumption. intros m i. assert empty. apply ( negnatgth0n m i ). contradiction. intros P is u. destruct ( is 0%nat ) as [ l | r ]. apply total2tohexists. split with 0%nat. split. assumption. intros m i. assert empty. apply ( negnatgth0n m i ). contradiction. set ( P' := fun m : nat => P ( S m ) ). assert ( forall m : nat, coprod ( P' m ) ( neg ( P' m ) ) ) as is'. intros m. unfold P'. apply ( is ( S m ) ). set ( c := IHn P' is' u ). apply c. intros k. destruct k as [ k v ]. destruct v as [ v0 v1 ]. apply total2tohexists. split with ( S k ). split. assumption. intros m. destruct m. intros i. assumption. intros i. apply v1. apply i. Defined. (** END OF FILE *) Pelayo-Coq/._padics.v000777 000765 000024 00000000324 12104265236 015315 0ustar00nicolastaff000000 000000 Mac OS X  2¢ÔATTRÔ˜<˜<com.apple.quarantineq/0002;53a854a1;Safari;5085629F-B604-4322-A539-1F4796CB8AB1Pelayo-Coq/padics.v000777 000765 000024 00000203146 12104265236 015107 0ustar00nicolastaff000000 000000 (** *p adic numbers *) (** By Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren *) (** 2012 *) (** Settings *) Add Rec LoadPath "../Generalities". Add Rec LoadPath "../hlevel1". Add Rec LoadPath "../hlevel2". Add Rec LoadPath "../Proof_of_Extensionality". Add Rec LoadPath "../Algebra". Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *) (** Imports *) Require Export lemmas. Require Export fps. Require Export frac. Require Export z_mod_p. (** * I. Several basic lemmas *) Open Scope hz_scope. Lemma hzqrandnatsummation0r ( m : hz ) ( x : hzneq 0 m ) ( a : nat -> hz ) ( upper : nat ) : hzremaindermod m x ( natsummation0 upper a ) ~> hzremaindermod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ). Proof. intros. induction upper. simpl. rewrite hzremaindermoditerated. apply idpath. change ( hzremaindermod m x ( natsummation0 upper a + a ( S upper ) ) ~> hzremaindermod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) + hzremaindermod m x ( a ( S upper ) ) ) ). rewrite hzremaindermodandplus. rewrite IHupper. rewrite <- ( hzremaindermoditerated m x ( a ( S upper ) ) ). rewrite <- hzremaindermodandplus. rewrite hzremaindermoditerated. apply idpath. Defined. Lemma hzqrandnatsummation0q ( m : hz ) ( x : hzneq 0 m ) ( a : nat -> hz ) ( upper : nat ) : hzquotientmod m x ( natsummation0 upper a ) ~> ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) + hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ). Proof. intros. induction upper. simpl. rewrite <- hzqrandremainderq. rewrite hzplusr0. apply idpath. change ( natsummation0 ( S upper ) a ) with ( natsummation0 upper a + a ( S upper ) ). rewrite hzquotientmodandplus. rewrite IHupper. rewrite ( hzplusassoc ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) ) _ ( hzquotientmod m x ( a ( S upper ) ) ) ). rewrite ( hzpluscomm ( hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ) ( hzquotientmod m x ( a ( S upper ) ) ) ). rewrite <- ( hzplusassoc ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) ) ( hzquotientmod m x ( a ( S upper ) ) ) _ ). change ( natsummation0 upper ( fun n : nat => hzquotientmod m x ( a n ) ) + hzquotientmod m x ( a ( S upper ) ) ) with ( natsummation0 ( S upper ) ( fun n : nat => hzquotientmod m x ( a n ) ) ). rewrite hzqrandnatsummation0r. rewrite hzquotientmodandplus. rewrite <- hzqrandremainderq. rewrite hzplusl0. rewrite hzremaindermoditerated. rewrite ( hzplusassoc (natsummation0 ( S upper ) ( fun n : nat => hzquotientmod m x ( a n ) ) ) ( hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ) _ ). rewrite <- ( hzplusassoc ( hzquotientmod m x ( natsummation0 upper ( fun n : nat => hzremaindermod m x ( a n ) ) ) ) _ _ ). rewrite <- ( hzquotientmodandplus ) . apply idpath. Defined. Lemma hzquotientandtimesl ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : hzquotientmod m x ( a * b ) ~> ( ( hzquotientmod m x a ) * b + ( hzremaindermod m x a ) * ( hzquotientmod m x b ) + hzquotientmod m x ( ( hzremaindermod m x a ) * ( hzremaindermod m x b ) ) ). Proof. intros. rewrite hzquotientmodandtimes. rewrite ( hzmultcomm ( hzremaindermod m x b ) ( hzquotientmod m x a ) ). rewrite hzmultassoc. rewrite <- ( hzldistr ( hzquotientmod m x b * m ) _ ( hzquotientmod m x a )). rewrite ( hzmultcomm _ m ). rewrite <- ( hzdivequationmod m x b ). rewrite hzplusassoc. apply idpath. Defined. Lemma hzquotientandfpstimesl ( m : hz ) ( x : hzneq 0 m ) ( a b : nat -> hz ) ( upper : nat ) : hzquotientmod m x ( fpstimes hz a b upper ) ~> ( natsummation0 upper ( fun i : nat => ( hzquotientmod m x ( a i ) ) * b ( minus upper i ) ) + hzquotientmod m x ( natsummation0 upper ( fun i : nat => ( hzremaindermod m x ( a i ) ) * b ( minus upper i ) ) ) ). Proof. intros. destruct upper. simpl. unfold fpstimes. simpl. rewrite hzquotientandtimesl. rewrite hzplusassoc. apply ( maponpaths ( fun v : _ => hzquotientmod m x ( a 0%nat ) * b 0%nat + v ) ). rewrite ( hzquotientmodandtimes m x ( hzremaindermod m x ( a 0%nat ) ) ( b 0%nat ) ). rewrite <- hzqrandremainderq. rewrite hzmultx0. rewrite 2! hzmult0x. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. unfold fpstimes. rewrite hzqrandnatsummation0q. assert ( forall n : nat, hzquotientmod m x (a n * b ( minus ( S upper ) n)%nat) ~> ( ( hzquotientmod m x ( a n ) ) * b ( minus ( S upper ) n ) + ( hzremaindermod m x ( a n ) ) * ( hzquotientmod m x ( b ( minus ( S upper ) n ) ) ) + hzquotientmod m x ( ( hzremaindermod m x ( a n ) ) * ( hzremaindermod m x ( b ( minus ( S upper ) n ) ) ) ) ) ) as f. intro k. rewrite hzquotientandtimesl. apply idpath. rewrite ( natsummationpathsupperfixed _ _ ( fun x0 p => f x0 ) ). rewrite ( natsummationplusdistr ( S upper ) ( fun x0 : nat => hzquotientmod m x (a x0) * b ( minus ( S upper ) x0)%nat + hzremaindermod m x (a x0) * hzquotientmod m x (b (S upper - x0)%nat) ) ). rewrite ( natsummationplusdistr ( S upper ) ( fun x0 : nat => hzquotientmod m x (a x0) * b (S upper - x0)%nat ) ). rewrite 2! hzplusassoc. apply ( maponpaths ( fun v : _ => natsummation0 ( S upper ) ( fun i : nat => hzquotientmod m x ( a i ) * b ( minus ( S upper ) i ) ) + v ) ). rewrite ( hzqrandnatsummation0q m x ( fun i : nat => hzremaindermod m x ( a i ) * b ( minus ( S upper ) i ) ) ). assert ( (natsummation0 (S upper) (fun n : nat => hzremaindermod m x (hzremaindermod m x (a n) * b (S upper - n)%nat))) ~> ( natsummation0 ( S upper ) ( fun n : nat => hzremaindermod m x ( a n * b ( minus ( S upper ) n ) ) ) ) ) as g. apply natsummationpathsupperfixed. intros j p. rewrite hzremaindermodandtimes. rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. apply idpath. rewrite g. rewrite <- hzplusassoc. assert ( natsummation0 (S upper) (fun x0 : nat => hzremaindermod m x (a x0) * hzquotientmod m x (b (S upper - x0)%nat)) + natsummation0 (S upper) (fun x0 : nat => hzquotientmod m x (hzremaindermod m x (a x0) * hzremaindermod m x (b (S upper - x0)%nat))) ~> natsummation0 (S upper) (fun n : nat => hzquotientmod m x (hzremaindermod m x (a n) * b (S upper - n)%nat)) ) as h. rewrite <- ( natsummationplusdistr ( S upper ) ( fun x0 : nat => hzremaindermod m x ( a x0 ) * hzquotientmod m x ( b ( minus ( S upper ) x0 ) ) ) ). apply natsummationpathsupperfixed. intros j p. rewrite ( hzquotientmodandtimes m x ( hzremaindermod m x ( a j ) ) ( ( b ( minus ( S upper ) j ) ) ) ). rewrite <- hzqrandremainderq. rewrite 2! hzmult0x. rewrite hzmultx0. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. rewrite h. apply idpath. Defined. Close Scope hz_scope. (** * II. The carrying operation and induced equivalence relation on formal power series *) Open Scope rng_scope. Fixpoint precarry ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) ( n : nat ) : hz := match n with | 0%nat => a 0%nat | S n => a ( S n ) + ( hzquotientmod m is ( precarry m is a n ) ) end. Definition carry ( m : hz ) ( is : hzneq 0 m ) : fpscommrng hz -> fpscommrng hz := fun a : fpscommrng hz => fun n : nat => hzremaindermod m is ( precarry m is a n ). (* precarry and carry are as described in the following example: CASE: mod 3 First we normalize the sequence as we go along: 5 6 8 4 (13) 2 2 ( remainder 2 mod 3 = 2 ) 4 1 ( remainder 13 mod 3 = 1, quotient 13 mod 3 = 4 ) 2 2 ( remainder 8 mod 3 = 2, quotient 8 mod 3 = 2 ) 3 1 ( remainder 10 mod 3 = 1, quotient 10 mod 3 = 3 ) 3 0 ( remainder 9 mod 3 = 0, quotient 9 mod 3 = 3 ) 2 2 ( remainder 8 mod 3 = 2, quotient 8 mod 3 = 2 ) 2 2 0 1 2 1 2 Next we first precarry and then carry: 5 6 8 4 (13) 2 2 4 13 2 8 3 (10) 3 9 2 8 2 8 9 (10) 8 (13) 2 <--- precarried sequence 2 2 0 1 2 1 2 <--- carried sequence *) Lemma isapropcarryequiv ( m : hz ) ( is : hzneq 0 m ) ( a b : fpscommrng hz ) : isaprop ( ( carry m is a ) ~> ( carry m is b ) ). Proof. intros. apply ( fps hz ). Defined. Definition carryequiv0 ( m : hz ) ( is : hzneq 0 m ) : hrel ( fpscommrng hz ) := fun a b : fpscommrng hz => hProppair _ ( isapropcarryequiv m is a b ). Lemma carryequiviseqrel ( m : hz ) ( is : hzneq 0 m ) : iseqrel ( carryequiv0 m is ). Proof. intros. split. split. intros a b c i j. simpl. rewrite i. apply j. intros a. simpl. apply idpath. intros a b i. simpl. rewrite i. apply idpath. Defined. Lemma carryandremainder ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) ( n : nat ) : hzremaindermod m is ( carry m is a n ) ~> carry m is a n. Proof. intros. unfold carry. rewrite hzremaindermoditerated. apply idpath. Defined. Definition carryequiv ( m : hz ) ( is : hzneq 0 m ) : eqrel ( fpscommrng hz ) := eqrelpair _ ( carryequiviseqrel m is ). Lemma precarryandcarry ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) : precarry m is ( carry m is a ) ~> carry m is a. Proof. intros. assert ( forall n : nat, ( precarry m is ( carry m is a ) ) n ~> ( ( carry m is a ) n ) ) as f. intros n. induction n. simpl. apply idpath. simpl. rewrite IHn. unfold carry at 2. rewrite <- hzqrandremainderq. rewrite hzplusr0. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma hzqrandcarryeq ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) ( n : nat ) : carry m is a n ~> ( ( m * 0 ) + carry m is a n ). Proof. intros. rewrite hzmultx0. rewrite hzplusl0. apply idpath. Defined. Lemma hzqrandcarryineq ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) ( n : nat ) : dirprod ( hzleh 0 ( carry m is a n ) ) ( hzlth ( carry m is a n ) ( nattohz ( hzabsval m ) ) ). Proof. intros. split. unfold carry. apply ( pr2 ( pr1 ( divalgorithm ( precarry m is a n ) m is ) ) ). unfold carry. apply ( pr2 ( pr1 ( divalgorithm ( precarry m is a n ) m is ) ) ). Defined. Lemma hzqrandcarryq ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) ( n : nat ) : 0 ~> hzquotientmod m is ( carry m is a n ). Proof. intros. apply ( hzqrtestq m is ( carry m is a n ) 0 ( carry m is a n ) ). split. apply hzqrandcarryeq. apply hzqrandcarryineq. Defined. Lemma hzqrandcarryr ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) ( n : nat ) : carry m is a n ~> hzremaindermod m is ( carry m is a n ). Proof. intros. apply ( hzqrtestr m is ( carry m is a n ) 0 ( carry m is a n ) ). split. apply hzqrandcarryeq. apply hzqrandcarryineq. Defined. Lemma doublecarry ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) : carry m is ( carry m is a ) ~> carry m is a. Proof. intros. assert ( forall n : nat, ( carry m is ( carry m is a ) ) n ~> ( ( carry m is a ) n ) ) as f. intros. induction n. unfold carry. simpl. apply hzremaindermoditerated. unfold carry. simpl. change (precarry m is (fun n0 : nat => hzremaindermod m is (precarry m is a n0)) n) with ( ( precarry m is ( carry m is a ) ) n ). rewrite precarryandcarry. rewrite <- hzqrandcarryq. rewrite hzplusr0. rewrite hzremaindermoditerated. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma carryandcarryequiv ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) : carryequiv m is ( carry m is a ) a. Proof. intros. simpl. rewrite doublecarry. apply idpath. Defined. Lemma quotientprecarryplus ( m : hz ) ( is : hzneq 0 m ) ( a b : fpscommrng hz ) ( n : nat ) : hzquotientmod m is ( precarry m is ( a + b ) n ) ~> ( hzquotientmod m is ( precarry m is a n ) + hzquotientmod m is ( precarry m is b n ) + hzquotientmod m is ( precarry m is ( carry m is a + carry m is b ) n ) ). Proof. intros. induction n. simpl. change ( hzquotientmod m is ( a 0%nat + b 0%nat ) ~> (hzquotientmod m is (a 0%nat) + hzquotientmod m is (b 0%nat) + hzquotientmod m is ( hzremaindermod m is ( a 0%nat ) + hzremaindermod m is ( b 0%nat ) ) ) ). rewrite hzquotientmodandplus. apply idpath. change ( hzquotientmod m is ( a ( S n ) + b ( S n ) + hzquotientmod m is ( precarry m is (a + b) n ) ) ~> (hzquotientmod m is (precarry m is a (S n)) + hzquotientmod m is (precarry m is b (S n)) + hzquotientmod m is (carry m is a ( S n ) + carry m is b ( S n ) + hzquotientmod m is ( precarry m is (carry m is a + carry m is b) n)) ) ). rewrite IHn. rewrite ( rngassoc1 hz ( a ( S n ) ) ( b ( S n ) ) _ ). rewrite <- ( rngassoc1 hz ( b ( S n ) ) ). rewrite ( rngcomm1 hz ( b ( S n ) ) _ ). rewrite <- 3! ( rngassoc1 hz ( a ( S n ) ) _ _ ). change ( a ( S n ) + hzquotientmod m is ( precarry m is a n ) ) with ( precarry m is a ( S n ) ). set ( pa := precarry m is a ( S n ) ). rewrite ( rngassoc1 hz pa _ ( b ( S n ) ) ). rewrite ( rngcomm1 hz _ ( b ( S n ) ) ). change ( b ( S n ) + hzquotientmod m is ( precarry m is b n ) ) with ( precarry m is b ( S n ) ). set ( pb := precarry m is b ( S n ) ). set ( ab := precarry m is ( carry m is a + carry m is b ) ). rewrite ( rngassoc1 hz ( carry m is a ( S n ) ) ( carry m is b ( S n ) ) ( hzquotientmod m is ( ab n ) ) ). rewrite ( hzquotientmodandplus m is ( carry m is a ( S n ) ) _ ). unfold carry at 1. rewrite <- hzqrandremainderq. rewrite hzplusl0. rewrite ( hzquotientmodandplus m is ( carry m is b ( S n ) ) _ ). unfold carry at 1. rewrite <- hzqrandremainderq. rewrite hzplusl0. rewrite ( rngassoc1 hz pa pb _ ). rewrite ( hzquotientmodandplus m is pa _ ). change (pb + hzquotientmod m is (ab n)) with (pb + hzquotientmod m is (ab n))%hz. rewrite ( hzquotientmodandplus m is pb ( hzquotientmod m is ( ab n ) ) ). rewrite <- 2! ( rngassoc1 hz ( hzquotientmod m is pa ) _ _ ). rewrite <- 2! ( rngassoc1 hz ( hzquotientmod m is pa + hzquotientmod m is pb ) _ ). rewrite 2! ( rngassoc1 hz ( hzquotientmod m is pa + hzquotientmod m is pb + hzquotientmod m is (hzquotientmod m is (ab n)) ) _ _ ). apply ( maponpaths ( fun x : hz => ( hzquotientmod m is pa + hzquotientmod m is pb + hzquotientmod m is (hzquotientmod m is (ab n)) ) + x ) ). unfold carry at 1 2. rewrite 2! hzremaindermoditerated. change ( precarry m is b ( S n ) ) with pb. change ( precarry m is a ( S n ) ) with pa. apply ( maponpaths ( fun x : hz => ( hzquotientmod m is (hzremaindermod m is pb + hzremaindermod m is (hzquotientmod m is (ab n)))%hz ) + x ) ). apply maponpaths. apply ( maponpaths ( fun x : hz => hzremaindermod m is pa + x ) ). rewrite ( hzremaindermodandplus m is ( carry m is b ( S n ) ) _ ). unfold carry. rewrite hzremaindermoditerated. rewrite <- ( hzremaindermodandplus m is ( precarry m is b ( S n ) ) _ ). apply idpath. Defined. Lemma carryandplus ( m : hz ) ( is : hzneq 0 m ) ( a b : fpscommrng hz ) : carry m is ( a + b ) ~> carry m is ( carry m is a + carry m is b ). Proof. intros. assert ( forall n : nat, carry m is ( a + b ) n ~> ( carry m is ( carry m is a + carry m is b ) n ) ) as f. intros n. destruct n. change ( hzremaindermod m is ( a 0%nat + b 0%nat ) ~> hzremaindermod m is ( hzremaindermod m is ( a 0%nat ) + hzremaindermod m is ( b 0%nat ) ) ). rewrite hzremaindermodandplus. apply idpath. change ( hzremaindermod m is ( a ( S n ) + b ( S n ) + hzquotientmod m is ( precarry m is ( a + b ) n ) ) ~> hzremaindermod m is ( hzremaindermod m is ( a ( S n ) + hzquotientmod m is ( precarry m is a n ) ) + hzremaindermod m is ( b ( S n ) + hzquotientmod m is ( precarry m is b n ) ) + hzquotientmod m is ( precarry m is ( carry m is a + carry m is b ) n ) ) ). rewrite quotientprecarryplus. rewrite ( hzremaindermodandplus m is ( hzremaindermod m is (a (S n) + hzquotientmod m is (precarry m is a n)) + hzremaindermod m is (b (S n) + hzquotientmod m is (precarry m is b n)) ) _ ). change (hzremaindermod m is (a (S n) + hzquotientmod m is (precarry m is a n)) + hzremaindermod m is (b (S n) + hzquotientmod m is (precarry m is b n))) with (hzremaindermod m is (a (S n) + hzquotientmod m is (precarry m is a n))%rng + hzremaindermod m is (b (S n) + hzquotientmod m is (precarry m is b n))%rng)%hz. rewrite <- (hzremaindermodandplus m is (a (S n) + hzquotientmod m is (precarry m is a n)) (b (S n) + hzquotientmod m is (precarry m is b n)) ). rewrite <- hzremaindermodandplus. change ( ((a (S n) + hzquotientmod m is (precarry m is a n))%rng + (b (S n) + hzquotientmod m is (precarry m is b n))%rng + hzquotientmod m is (precarry m is (carry m is a + carry m is b)%rng n))%hz ) with ((a (S n) + hzquotientmod m is (precarry m is a n))%rng + (b (S n) + hzquotientmod m is (precarry m is b n))%rng + hzquotientmod m is (precarry m is (carry m is a + carry m is b)%rng n))%rng. rewrite <- ( rngassoc1 hz ( a ( S n ) + hzquotientmod m is ( precarry m is a n ) ) (b (S n) ) ( hzquotientmod m is (precarry m is b n)) ). rewrite ( rngassoc1 hz ( a ( S n ) ) ( hzquotientmod m is ( precarry m is a n ) ) ( b ( S n ) ) ). rewrite ( rngcomm1 hz ( hzquotientmod m is ( precarry m is a n ) ) ( b ( S n ) ) ). rewrite <- 3! ( rngassoc1 hz ). apply idpath. apply ( funextfun _ _ f ). Defined. Definition quotientprecarry ( m : hz ) ( is : hzneq 0 m ) ( a : fpscommrng hz ) : fpscommrng hz := fun x : nat => hzquotientmod m is ( precarry m is a x ). Lemma quotientandtimesrearrangel ( m : hz ) ( is : hzneq 0 m ) ( x y : hz ) : hzquotientmod m is ( x * y ) ~> ( ( hzquotientmod m is x ) * y + hzquotientmod m is ( ( hzremaindermod m is x ) * y ) ). Proof. intros. rewrite hzquotientmodandtimes. change (hzquotientmod m is x * hzquotientmod m is y * m + hzremaindermod m is y * hzquotientmod m is x + hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y))%hz with (hzquotientmod m is x * hzquotientmod m is y * m + hzremaindermod m is y * hzquotientmod m is x + hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y))%rng. rewrite ( rngcomm2 hz ( hzremaindermod m is y ) ( hzquotientmod m is x ) ). rewrite ( rngassoc2 hz ). rewrite <- ( rngldistr hz ). rewrite ( rngcomm2 hz ( hzquotientmod m is y ) m ). change (m * hzquotientmod m is y + hzremaindermod m is y)%rng with (m * hzquotientmod m is y + hzremaindermod m is y)%hz. rewrite <- ( hzdivequationmod m is y ). change (hzremaindermod m is x * y)%rng with (hzremaindermod m is x * y)%hz. rewrite ( hzquotientmodandtimes m is ( hzremaindermod m is x ) y ). rewrite hzremaindermoditerated. rewrite <- hzqrandremainderq. rewrite hzmultx0. rewrite 2! hzmult0x. rewrite hzplusl0. rewrite ( rngassoc1 hz ). change (hzquotientmod m is x * y + (hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y))%hz) with (hzquotientmod m is x * y + (hzremaindermod m is x * hzquotientmod m is y + hzquotientmod m is (hzremaindermod m is x * hzremaindermod m is y)))%rng. apply idpath. Defined. Lemma natsummationplusshift { R : commrng } ( upper : nat ) ( f g : nat -> R ) : ( natsummation0 ( S upper ) f ) + ( natsummation0 upper g ) ~> ( f 0%nat + ( natsummation0 upper ( fun x : nat => f ( S x ) + g x ) ) ). Proof. intros. destruct upper. unfold natsummation0. simpl. apply ( rngassoc1 R ). rewrite ( natsummationshift0 ( S upper ) f ). rewrite ( rngcomm1 R _ ( f 0%nat ) ). rewrite ( rngassoc1 R ). rewrite natsummationplusdistr. apply idpath. Defined. Lemma precarryandtimesl ( m : hz ) ( is: hzneq 0 m ) ( a b : fpscommrng hz ) ( n : nat ) : hzquotientmod m is ( precarry m is (a * b ) n ) ~> ( ( quotientprecarry m is a * b ) n + hzquotientmod m is ( precarry m is ( ( carry m is a ) * b ) n ) ). Proof. intros. induction n. unfold precarry. change ( ( a * b ) 0%nat ) with ( a 0%nat * b 0%nat ). change ( ( quotientprecarry m is a * b ) 0%nat ) with ( hzquotientmod m is ( a 0%nat ) * b 0%nat ). rewrite quotientandtimesrearrangel. change ( ( carry m is a * b ) 0%nat ) with ( hzremaindermod m is ( a 0%nat ) * b 0%nat ). apply idpath. change ( precarry m is ( a * b ) ( S n ) ) with ( ( a * b ) ( S n ) + hzquotientmod m is ( precarry m is ( a * b ) n ) ). rewrite IHn. rewrite <- ( rngassoc1 hz ). assert ( ( ( a * b ) ( S n ) + ( quotientprecarry m is a * b ) n ) ~> ( @op2 ( fpscommrng hz ) ( precarry m is a ) b ) ( S n ) ) as f. change ( ( a * b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun x : nat => a x * b ( minus ( S n ) x ) ) ). change ( ( quotientprecarry m is a * b ) n ) with ( natsummation0 n ( fun x : nat => quotientprecarry m is a x * b ( minus n x ) ) ). rewrite natsummationplusshift. change ( ( @op2 ( fpscommrng hz ) ( precarry m is a ) b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun x : nat => ( precarry m is a ) x * b ( minus ( S n ) x ) ) ). rewrite natsummationshift0. unfold precarry at 2. simpl. rewrite <- ( rngcomm1 hz ( a 0%nat * b ( S n ) ) _ ). apply ( maponpaths ( fun x : hz => a 0%nat * b ( S n ) + x ) ). apply natsummationpathsupperfixed. intros k j. unfold quotientprecarry. rewrite ( rngrdistr hz ). apply idpath. rewrite f. rewrite hzquotientmodandplus. change ( @op2 ( fpscommrng hz ) ( precarry m is a ) b ) with ( fpstimes hz ( precarry m is a ) b ). rewrite ( hzquotientandfpstimesl m is ( precarry m is a ) b ). change ( @op2 ( fpscommrng hz ) ( carry m is a ) b ) with ( fpstimes hz ( carry m is a ) b ) at 1. unfold fpstimes at 1. unfold carry at 1. change (fun n0 : nat => let t' := fun m0 : nat => b (n0 - m0)%nat in natsummation0 n0 (fun x : nat => (hzremaindermod m is (precarry m is a x) * t' x)%rng)) with ( carry m is a * b ). change ( ( quotientprecarry m is a * b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun i : nat => hzquotientmod m is ( precarry m is a i ) * b ( S n - i )%nat ) ). rewrite 2! hzplusassoc. apply ( maponpaths ( fun v : _ => natsummation0 ( S n ) ( fun i : nat => hzquotientmod m is ( precarry m is a i ) * b ( S n - i )%nat ) + v ) ). change ( precarry m is ( carry m is a * b ) ( S n ) ) with ( ( carry m is a * b ) ( S n ) + hzquotientmod m is ( precarry m is ( carry m is a * b ) n ) ). change ((carry m is a * b) (S n) + hzquotientmod m is (precarry m is (carry m is a * b) n)) with ((carry m is a * b)%rng (S n) + hzquotientmod m is (precarry m is (carry m is a * b) n)%rng)%hz. rewrite ( hzquotientmodandplus m is ( ( carry m is a * b ) ( S n ) ) ( hzquotientmod m is ( precarry m is ( carry m is a * b ) n ) ) ). change ( ( carry m is a * b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun i : nat => hzremaindermod m is ( precarry m is a i ) * b ( S n - i )%nat ) ). rewrite hzplusassoc. apply ( maponpaths ( fun v : _ => ( hzquotientmod m is ( natsummation0 ( S n ) ( fun i : nat => hzremaindermod m is ( precarry m is a i ) * b ( S n - i )%nat ) ) ) + v ) ). apply ( maponpaths ( fun v : _ => hzquotientmod m is ( hzquotientmod m is ( precarry m is ( carry m is a * b )%rng n ) ) + v ) ). apply maponpaths. apply ( maponpaths ( fun v : _ => v + hzremaindermod m is ( hzquotientmod m is ( precarry m is ( carry m is a * b )%rng n ) ) ) ). unfold fpstimes. rewrite hzqrandnatsummation0r. rewrite ( hzqrandnatsummation0r m is ( fun i : nat => hzremaindermod m is ( precarry m is a i ) * b ( S n - i )%nat ) ). apply maponpaths. apply natsummationpathsupperfixed. intros j p. change ( hzremaindermod m is (hzremaindermod m is (precarry m is a j) * b ( minus ( S n ) j)) ) with ( hzremaindermod m is (hzremaindermod m is (precarry m is a j) * b (S n - j)%nat)%hz ). rewrite ( hzremaindermodandtimes m is ( hzremaindermod m is ( precarry m is a j ) ) ( b ( minus ( S n ) j ) ) ). rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. apply idpath. Defined. Lemma carryandtimesl ( m : hz ) ( is : hzneq 0 m ) ( a b : fpscommrng hz ) : carry m is ( a * b ) ~> carry m is ( carry m is a * b ). Proof. intros. assert ( forall n : nat, carry m is ( a * b ) n ~> carry m is ( carry m is a * b ) n ) as f. intros n. destruct n. unfold carry at 1 2. change ( precarry m is ( a * b ) 0%nat ) with ( a 0%nat * b 0%nat ). change ( precarry m is ( carry m is a * b ) 0%nat ) with ( carry m is a 0%nat * b 0%nat ). unfold carry. change (hzremaindermod m is (precarry m is a 0) * b 0%nat) with (hzremaindermod m is (precarry m is a 0) * b 0%nat )%hz. rewrite ( hzremaindermodandtimes m is ( hzremaindermod m is ( precarry m is a 0%nat ) ) ( b 0%nat ) ). rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. change ( precarry m is a 0%nat ) with ( a 0%nat ). apply idpath. unfold carry at 1 2. change ( precarry m is ( a * b ) ( S n ) ) with ( ( a * b ) ( S n ) + hzquotientmod m is ( precarry m is ( a * b ) n ) ). rewrite precarryandtimesl. rewrite <- ( rngassoc1 hz ). rewrite hzremaindermodandplus. assert ( hzremaindermod m is ( ( a * b ) ( S n ) + ( quotientprecarry m is a * b ) n ) ~> hzremaindermod m is ( ( carry m is a * b ) ( S n ) ) ) as g. change ( hzremaindermod m is ( ( natsummation0 ( S n ) ( fun u : nat => a u * b ( minus ( S n ) u ) ) ) + ( natsummation0 n ( fun u : nat => ( quotientprecarry m is a ) u * b ( minus n u ) ) ) ) ~> hzremaindermod m is ( natsummation0 ( S n ) ( fun u : nat => ( carry m is a ) u * b ( minus ( S n ) u ) ) ) ). rewrite ( natsummationplusshift n ). rewrite ( natsummationshift0 n ( fun u : nat => carry m is a u * b ( minus ( S n ) u ) ) ). assert ( hzremaindermod m is ( natsummation0 n ( fun x : nat => a ( S x ) * b ( minus ( S n ) ( S x ) ) + quotientprecarry m is a x * b ( minus n x ) ) ) ~> hzremaindermod m is (natsummation0 n ( fun x : nat => carry m is a ( S x ) * b ( minus ( S n ) ( S x ) ) ) ) ) as h. rewrite hzqrandnatsummation0r. rewrite ( hzqrandnatsummation0r m is ( fun x : nat => carry m is a ( S x ) * b ( minus ( S n ) ( S x ) ) ) ). apply maponpaths. apply natsummationpathsupperfixed. intros j p. unfold quotientprecarry. simpl. change (a (S j) * b ( minus n j) + hzquotientmod m is (precarry m is a j) * b ( minus n j)) with (a (S j) * b ( minus n j) + hzquotientmod m is (precarry m is a j) * b ( minus n j) )%hz. rewrite <- ( hzrdistr ( a ( S j ) ) ( hzquotientmod m is ( precarry m is a j ) ) ( b ( minus n j ) ) ). rewrite hzremaindermodandtimes. change ( hzremaindermod m is (hzremaindermod m is (a (S j) + hzquotientmod m is (precarry m is a j)) * hzremaindermod m is (b ( minus n j))) ~> hzremaindermod m is (carry m is a (S j) * b (minus n j)) )%rng. rewrite <- ( hzremaindermoditerated m is (a (S j) + hzquotientmod m is (precarry m is a j)) ). unfold carry. rewrite <- hzremaindermodandtimes. apply idpath. rewrite hzremaindermodandplus. rewrite h. rewrite <- hzremaindermodandplus. unfold carry at 3. rewrite ( hzremaindermodandplus m is _ ( hzremaindermod m is ( precarry m is a 0%nat ) * b ( minus ( S n ) 0%nat ) ) ). rewrite hzremaindermodandtimes. rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. change ( precarry m is a 0%nat ) with ( a 0%nat ). rewrite <- hzremaindermodandplus. rewrite hzpluscomm. apply idpath. rewrite g. rewrite <- hzremaindermodandplus. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma carryandtimesr ( m : hz ) ( is : hzneq 0 m ) ( a b : fpscommrng hz ) : carry m is ( a * b ) ~> carry m is ( a * carry m is b ). Proof. intros. rewrite ( @rngcomm2 ( fpscommrng hz ) ). rewrite carryandtimesl. rewrite ( @rngcomm2 ( fpscommrng hz ) ). apply idpath. Defined. Lemma carryandtimes ( m : hz ) ( is : hzneq 0 m ) ( a b : fpscommrng hz ) : carry m is ( a * b ) ~> carry m is ( carry m is a * carry m is b ). Proof. intros. rewrite carryandtimesl. rewrite carryandtimesr. apply idpath. Defined. Lemma rngcarryequiv ( m : hz ) ( is : hzneq 0 m ) : @rngeqrel ( fpscommrng hz ). Proof. intros. split with ( carryequiv m is ). split. split. intros a b c q. simpl. simpl in q. rewrite carryandplus. rewrite q. rewrite <- carryandplus. apply idpath. intros a b c q. simpl. rewrite carryandplus. rewrite q. rewrite <- carryandplus. apply idpath. split. intros a b c q. simpl. rewrite carryandtimes. rewrite q. rewrite <- carryandtimes. apply idpath. intros a b c q. simpl. rewrite carryandtimes. rewrite q. rewrite <- carryandtimes. apply idpath. Defined. Definition commrngofpadicints ( p : hz ) ( is : isaprime p ) := commrngquot ( rngcarryequiv p ( isaprimetoneq0 is ) ). Definition padicplus ( p : hz ) ( is : isaprime p ) := @op1 ( commrngofpadicints p is ). Definition padictimes ( p : hz ) ( is : isaprime p ) := @op2 ( commrngofpadicints p is ). (** * III. The apartness relation on p-adic integers *) Definition padicapart0 ( p : hz ) ( is : isaprime p ) : hrel ( fpscommrng hz ) := fun a b : _ => ( hexists ( fun n : nat => ( neq _ ( carry p ( isaprimetoneq0 is) a n ) ( carry p ( isaprimetoneq0 is ) b n ) ) ) ). Lemma padicapartiscomprel ( p : hz ) ( is : isaprime p ) : iscomprelrel ( carryequiv p ( isaprimetoneq0 is ) ) ( padicapart0 p is ). Proof. intros p is a a' b b' i j. apply uahp. intro k. apply k. intros u. destruct u as [ n u ]. apply total2tohexists. split with n. rewrite <- i , <- j. assumption. intro k. apply k. intros u. destruct u as [ n u ]. apply total2tohexists. split with n. rewrite i, j. assumption. Defined. Definition padicapart1 ( p : hz ) ( is : isaprime p ) : hrel ( commrngofpadicints p is ) := quotrel ( padicapartiscomprel p is ). Lemma isirreflpadicapart0 ( p : hz ) ( is : isaprime p ) : isirrefl ( padicapart0 p is ). Proof. intros. intros a f. simpl in f. assert hfalse as x. apply f. intros u. destruct u as [ n u ]. apply u. apply idpath. apply x. Defined. Lemma issymmpadicapart0 ( p : hz ) ( is : isaprime p ) : issymm ( padicapart0 p is ). Proof. intros. intros a b f. apply f. intros u. destruct u as [ n u ]. apply total2tohexists. split with n. intros g. apply u. rewrite g. apply idpath. Defined. Lemma iscotranspadicapart0 ( p : hz ) ( is : isaprime p ) : iscotrans ( padicapart0 p is ). Proof. intros. intros a b c f. apply f. intros u. destruct u as [ n u ]. intros P j. apply j. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) a n ) ( carry p ( isaprimetoneq0 is ) b n ) ) as [ l | r ]. apply ii2. intros Q k. apply k. split with n. intros g. apply u. rewrite l, g. apply idpath. apply ii1. intros Q k. apply k. split with n. intros g. apply r. assumption. Defined. Definition padicapart ( p : hz ) ( is : isaprime p ) : apart ( commrngofpadicints p is ). Proof. intros. split with ( padicapart1 p is ). split. unfold padicapart1. apply ( isirreflquotrel ( padicapartiscomprel p is ) ( isirreflpadicapart0 p is ) ). split. apply ( issymmquotrel ( padicapartiscomprel p is ) ( issymmpadicapart0 p is ) ). apply ( iscotransquotrel ( padicapartiscomprel p is ) ( iscotranspadicapart0 p is ) ). Defined. Lemma precarryandzero ( p : hz ) ( is : isaprime p ) : precarry p ( isaprimetoneq0 is ) 0 ~> ( @rngunel1 ( fpscommrng hz ) ). Proof. intros. assert ( forall n : nat, precarry p ( isaprimetoneq0 is ) 0 n ~> ( @rngunel1 (fpscommrng hz ) ) n ) as f. intros n. induction n. unfold precarry. change ( ( @rngunel1 ( fpscommrng hz ) ) 0%nat ) with 0%hz. apply idpath. change ( ( ( @rngunel1 ( fpscommrng hz ) ( S n ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( @rngunel1 ( fpscommrng hz ) ) n ) ) ) ~> 0%hz ). rewrite IHn. change ( ( @rngunel1 ( fpscommrng hz ) ) n ) with 0%hz. change ( ( @rngunel1 ( fpscommrng hz ) ) ( S n ) ) with 0%hz. rewrite hzqrand0q. rewrite hzplusl0. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma carryandzero ( p : hz ) ( is : isaprime p ) : carry p ( isaprimetoneq0 is ) 0 ~> 0. Proof. intros. unfold carry. rewrite precarryandzero. assert ( forall n : nat, (fun n : nat => hzremaindermod p (isaprimetoneq0 is) ( ( @rngunel1 ( fpscommrng hz ) ) n)) n ~> ( @rngunel1 ( fpscommrng hz ) ) n ) as f. intros n. rewrite hzqrand0r. unfold carry. change ( ( @rngunel1 ( fpscommrng hz ) n ) ) with 0%hz. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma precarryandone ( p : hz ) ( is : isaprime p ) : precarry p ( isaprimetoneq0 is ) 1 ~> ( @rngunel2 ( fpscommrng hz ) ). Proof. intros. assert ( forall n : nat, precarry p ( isaprimetoneq0 is ) 1 n ~> ( @rngunel2 (fpscommrng hz ) ) n ) as f. intros n. induction n. unfold precarry. apply idpath. simpl. rewrite IHn. destruct n. change ( ( @rngunel2 ( fpscommrng hz ) ) 0%nat ) with 1%hz. rewrite hzqrand1q. rewrite hzplusr0. apply idpath. change ( ( @rngunel2 ( fpscommrng hz ) ) ( S n ) ) with 0%hz. rewrite hzqrand0q. rewrite hzplusr0. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma carryandone ( p : hz ) ( is : isaprime p ) : carry p ( isaprimetoneq0 is ) 1 ~> 1. Proof. intros. unfold carry. rewrite precarryandone. assert ( forall n : nat, (fun n : nat => hzremaindermod p (isaprimetoneq0 is) ( ( @rngunel2 ( fpscommrng hz ) ) n)) n ~> ( @rngunel2 ( fpscommrng hz ) ) n ) as f. intros n. destruct n. change ( ( @rngunel2 ( fpscommrng hz ) ) 0%nat ) with 1%hz. rewrite hzqrand1r. apply idpath. change ( ( @rngunel2 ( fpscommrng hz ) ) ( S n ) ) with 0%hz. rewrite hzqrand0r. apply idpath. apply ( funextfun _ _ f ). Defined. Lemma padicapartcomputation ( p : hz ) ( is : isaprime p ) ( a b : fpscommrng hz ) : ( pr1 ( padicapart p is ) ) ( setquotpr (carryequiv p ( isaprimetoneq0 is ) ) a ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) b ) ~> padicapart0 p is a b. Proof. intros. apply uahp. intros i. apply i. intro u. apply u. Defined. Lemma padicapartandplusprecarryl ( p : hz ) ( is : isaprime p ) ( a b c : fpscommrng hz ) ( n : nat ) ( x : neq _ ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) b ) n ) ( ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) c ) ) n ) ) : ( padicapart0 p is ) b c. Proof. intros. set ( P := fun x : nat => neq hz (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a + carry p (isaprimetoneq0 is) b) x) (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a + carry p (isaprimetoneq0 is) c) x) ). assert ( isdecnatprop P ) as isdec. intros m. destruct ( isdeceqhz (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a + carry p (isaprimetoneq0 is) b) m) (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a + carry p (isaprimetoneq0 is) c) m) ) as [ l | r ]. apply ii2. intros j. apply j. assumption. apply ii1. assumption. set ( leexists := leastelementprinciple n P isdec x ). apply leexists. intro k. destruct k as [ k k' ]. destruct k' as [ k' k'' ]. destruct k. apply total2tohexists. split with 0%nat. intros i. apply k'. change (carry p (isaprimetoneq0 is) a 0%nat + carry p (isaprimetoneq0 is) b 0%nat ~> (carry p (isaprimetoneq0 is) a 0%nat + carry p (isaprimetoneq0 is) c 0%nat) ). rewrite i. apply idpath. apply total2tohexists. split with ( S k ). intro i. apply ( k'' k ). apply natlthnsn. intro j. apply k'. change ( carry p ( isaprimetoneq0 is ) a ( S k ) + carry p ( isaprimetoneq0 is ) b ( S k ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) b ) k ) ~> ( carry p ( isaprimetoneq0 is ) a ( S k ) + carry p ( isaprimetoneq0 is ) c ( S k ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) c ) k ) ) ). rewrite i. rewrite j. apply idpath. Defined. Lemma padicapartandplusprecarryr ( p : hz ) ( is : isaprime p ) ( a b c : fpscommrng hz ) ( n : nat ) ( x : neq _ ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) b + carry p ( isaprimetoneq0 is ) a ) n ) ( ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) c + carry p ( isaprimetoneq0 is ) a ) ) n ) ) : ( padicapart0 p is ) b c. Proof. intros. rewrite 2! ( rngcomm1 ( fpscommrng hz ) _ ( carry p ( isaprimetoneq0 is ) a ) ) in x. apply ( padicapartandplusprecarryl p is a b c n x ). Defined. Lemma commrngquotprandop1 { A : commrng } ( R : @rngeqrel A ) ( a b : A ) : ( @op1 ( commrngquot R ) ) ( setquotpr ( pr1 R ) a ) ( setquotpr ( pr1 R ) b ) ~> setquotpr ( pr1 R ) ( a + b ). Proof. intros. change ( @op1 ( commrngquot R ) ) with ( setquotfun2 R R ( @op1 A ) ( pr1 ( iscomp2binoptransrel ( pr1 R ) ( eqreltrans _ ) ( pr2 R ) ) ) ). unfold setquotfun2. rewrite setquotuniv2comm. apply idpath. Defined. Lemma commrngquotprandop2 { A : commrng } ( R : @rngeqrel A ) ( a b : A ) : ( @op2 ( commrngquot R ) ) ( setquotpr ( pr1 R ) a ) ( setquotpr ( pr1 R ) b ) ~> setquotpr ( pr1 R ) ( a * b ). Proof. intros. change ( @op2 ( commrngquot R ) ) with ( setquotfun2 R R ( @op2 A ) ( pr2 ( iscomp2binoptransrel ( pr1 R ) ( eqreltrans _ ) ( pr2 R ) ) ) ). unfold setquotfun2. rewrite setquotuniv2comm. apply idpath. Defined. Lemma setquotprandpadicplus ( p : hz ) ( is : isaprime p ) ( a b : fpscommrng hz ) : ( @op1 ( commrngofpadicints p is ) ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) a ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) b ) ~> setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( a + b ). Proof. intros. apply commrngquotprandop1. Defined. Lemma setquotprandpadictimes ( p : hz ) ( is : isaprime p ) ( a b : fpscommrng hz ) : ( @op2 ( commrngofpadicints p is ) ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) a ) ( setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) b ) ~> setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( a * b ). Proof. intros. apply commrngquotprandop2. Defined. Lemma padicplusisbinopapart0 ( p : hz ) ( is : isaprime p ) ( a b c : fpscommrng hz ) ( u : padicapart0 p is ( a + b ) ( a + c ) ) : padicapart0 p is b c. Proof. intros. apply u. intros n. destruct n as [ n n' ]. set ( P := fun x : nat => neq hz ( carry p ( isaprimetoneq0 is ) ( a + b) x) ( carry p ( isaprimetoneq0 is ) ( a + c) x) ). assert ( isdecnatprop P ) as isdec. intros m. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) ( a + b) m) ( carry p ( isaprimetoneq0 is ) ( a + c) m) ) as [ l | r ]. apply ii2. intros j. apply j. assumption. apply ii1. assumption. set ( le := leastelementprinciple n P isdec n'). apply le. intro k. destruct k as [ k k' ]. destruct k' as [ k' k'' ]. destruct k. apply total2tohexists. split with 0%nat. intros j. apply k'. unfold carry. unfold precarry. change ( ( a + b ) 0%nat ) with ( a 0%nat + b 0%nat ). change ( ( a + c ) 0%nat ) with ( a 0%nat + c 0%nat ). unfold carry in j. unfold precarry in j. rewrite hzremaindermodandplus. rewrite j. rewrite <- hzremaindermodandplus. apply idpath. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b ( S k ) ) ( carry p ( isaprimetoneq0 is ) c ( S k ) ) ) as [ l | r ]. apply ( padicapartandplusprecarryl p is a b c k ). intros j. apply k'. rewrite ( carryandplus ). unfold carry at 1. change ( hzremaindermod p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a ( S k ) + carry p ( isaprimetoneq0 is ) b ( S k ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) b ) k ) ) ~> carry p ( isaprimetoneq0 is ) ( a + c ) ( S k ) ). rewrite l. rewrite j. rewrite ( carryandplus p ( isaprimetoneq0 is ) a c ). unfold carry at 5. change ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) c ) ( S k ) ) with ( carry p ( isaprimetoneq0 is ) a ( S k ) + carry p ( isaprimetoneq0 is ) c ( S k ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a + carry p ( isaprimetoneq0 is ) c ) k ) ). apply idpath. apply total2tohexists. split with ( S k ). assumption. Defined. Lemma padicplusisbinopapartl ( p : hz ) ( is : isaprime p ) : isbinopapartl ( padicapart p is ) ( padicplus p is ). Proof. intros. unfold isbinopapartl. assert ( forall x x' x'' : commrngofpadicints p is, isaprop ( ( pr1 ( padicapart p is ) ) ( padicplus p is x x' ) ( padicplus p is x x'' ) -> ( ( pr1 ( padicapart p is ) ) x' x'' ) ) ) as int. intros. apply impred. intros. apply ( pr1 ( padicapart p is ) ). apply ( setquotuniv3prop _ ( fun x x' x'' => hProppair _ ( int x x' x'' ) ) ). intros a b c. change (pr1 (padicapart p is) (padicplus p is (setquotpr (rngcarryequiv p (isaprimetoneq0 is)) a) (setquotpr (rngcarryequiv p (isaprimetoneq0 is)) b)) (padicplus p is (setquotpr (rngcarryequiv p (isaprimetoneq0 is)) a) (setquotpr (rngcarryequiv p (isaprimetoneq0 is)) c)) -> pr1 (padicapart p is) (setquotpr (rngcarryequiv p (isaprimetoneq0 is)) b) (setquotpr (rngcarryequiv p (isaprimetoneq0 is)) c)). unfold padicplus. rewrite 2! setquotprandpadicplus. rewrite 2! padicapartcomputation. apply padicplusisbinopapart0. Defined. Lemma padicplusisbinopapartr ( p : hz ) ( is : isaprime p ) : isbinopapartr ( padicapart p is ) ( padicplus p is ). Proof. intros. unfold isbinopapartr. intros a b c. unfold padicplus. rewrite ( @rngcomm1 ( commrngofpadicints p is ) b a ). rewrite ( @rngcomm1 ( commrngofpadicints p is ) c a ). apply padicplusisbinopapartl. Defined. Lemma padicapartandtimesprecarryl ( p : hz ) ( is : isaprime p ) ( a b c : fpscommrng hz ) ( n : nat ) ( x : neq _ ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) n ) ( ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) c ) ) n ) ) : ( padicapart0 p is ) b c. Proof. intros. set ( P := fun x : nat => neq hz (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a * carry p (isaprimetoneq0 is) b) x) (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a * carry p (isaprimetoneq0 is) c) x) ). assert ( isdecnatprop P ) as isdec. intros m. destruct ( isdeceqhz (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a * carry p (isaprimetoneq0 is) b) m) (precarry p (isaprimetoneq0 is) (carry p (isaprimetoneq0 is) a * carry p (isaprimetoneq0 is) c) m) ) as [ l | r ]. apply ii2. intros j. apply j. assumption. apply ii1. assumption. set ( leexists := leastelementprinciple n P isdec x ). apply leexists. intro k. destruct k as [ k k' ]. destruct k' as [ k' k'' ]. induction k. apply total2tohexists. split with 0%nat. intros i. apply k'. change (carry p (isaprimetoneq0 is) a 0%nat * carry p (isaprimetoneq0 is) b 0%nat ~> (carry p (isaprimetoneq0 is) a 0%nat * carry p (isaprimetoneq0 is) c 0%nat) ). rewrite i. apply idpath. set ( Q := ( fun o : nat => hProppair ( carry p ( isaprimetoneq0 is ) b o ~> carry p ( isaprimetoneq0 is ) c o ) ( isasethz _ _ ) ) ). assert ( isdecnatprop Q ) as isdec'. intro o. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b o ) ( carry p ( isaprimetoneq0 is ) c o ) ) as [ l | r ]. apply ii1. assumption. apply ii2. assumption. destruct ( isdecisbndqdec Q isdec' ( S k ) ) as [ l | r ]. assert hfalse as xx. apply ( k'' k ). apply natlthnsn. intro j. apply k'. change ( ( natsummation0 ( S k ) ( fun x : nat => carry p ( isaprimetoneq0 is ) a x * carry p ( isaprimetoneq0 is ) b ( minus ( S k ) x ) ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) k ) ~> (( natsummation0 ( S k ) ( fun x : nat => carry p ( isaprimetoneq0 is ) a x * carry p ( isaprimetoneq0 is ) c ( minus ( S k ) x ) ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) c ) k ) ) ). assert ( natsummation0 ( S k ) (fun x0 : nat => carry p (isaprimetoneq0 is) a x0 * carry p (isaprimetoneq0 is) b ( minus ( S k ) x0)) ~> natsummation0 ( S k ) (fun x0 : nat => carry p (isaprimetoneq0 is) a x0 * carry p (isaprimetoneq0 is) c ( minus ( S k ) x0)) ) as f. apply natsummationpathsupperfixed. intros m y. rewrite ( l ( minus ( S k ) m ) ). apply idpath. apply minusleh. rewrite f. rewrite j. apply idpath. contradiction. apply r. intros o. destruct o as [ o o' ]. apply total2tohexists. split with o. apply o'. Defined. Lemma padictimesisbinopapart0 ( p : hz ) ( is : isaprime p ) ( a b c : fpscommrng hz ) ( u : padicapart0 p is ( a * b ) ( a * c ) ) : padicapart0 p is b c. Proof. intros. apply u. intros n. destruct n as [ n n' ]. destruct n. apply total2tohexists. split with 0%nat. intros j. apply n'. rewrite carryandtimes. rewrite ( carryandtimes p ( isaprimetoneq0 is ) a c ). change ( hzremaindermod p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a 0%nat * carry p ( isaprimetoneq0 is ) b 0%nat ) ~> hzremaindermod p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a 0%nat * carry p ( isaprimetoneq0 is ) c 0%nat ) ). rewrite j. apply idpath. set ( Q := ( fun o : nat => hProppair ( carry p ( isaprimetoneq0 is ) b o ~> carry p ( isaprimetoneq0 is ) c o ) ( isasethz _ _ ) ) ). assert ( isdecnatprop Q ) as isdec'. intro o. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b o ) ( carry p ( isaprimetoneq0 is ) c o ) ) as [ l | r ]. apply ii1. assumption. apply ii2. assumption. destruct ( isdecisbndqdec Q isdec'( S n ) ) as [ l | r ]. apply ( padicapartandtimesprecarryl p is a b c n ). intros j. assert hfalse as xx. apply n'. rewrite carryandtimes. rewrite ( carryandtimes p ( isaprimetoneq0 is ) a c ). change ( hzremaindermod p ( isaprimetoneq0 is ) ( natsummation0 ( S n ) ( fun x : nat => carry p ( isaprimetoneq0 is ) a x * carry p ( isaprimetoneq0 is ) b ( minus ( S n ) x ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) n ) ) ~> ( hzremaindermod p ( isaprimetoneq0 is ) ( natsummation0 ( S n ) ( fun x : nat => carry p ( isaprimetoneq0 is ) a x * carry p ( isaprimetoneq0 is ) c ( minus ( S n ) x ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) c ) n ) ) ) ). rewrite j. assert ( natsummation0 ( S n ) (fun x0 : nat => carry p (isaprimetoneq0 is) a x0 * carry p (isaprimetoneq0 is) b ( minus ( S n ) x0)) ~> natsummation0 ( S n ) (fun x0 : nat => carry p (isaprimetoneq0 is) a x0 * carry p (isaprimetoneq0 is) c ( minus ( S n ) x0)) ) as f. apply natsummationpathsupperfixed. intros m y. rewrite ( l ( minus ( S n ) m ) ). apply idpath. apply minusleh. rewrite f. apply idpath. contradiction. apply r. intros k. destruct k as [ k k' ]. apply total2tohexists. split with k. apply k'. Defined. Lemma padictimesisbinopapartl ( p : hz ) ( is : isaprime p ) : isbinopapartl ( padicapart p is ) ( padictimes p is ). Proof. intros. unfold isbinopapartl. assert ( forall x x' x'' : commrngofpadicints p is, isaprop ( ( pr1 ( padicapart p is ) ) ( padictimes p is x x' ) ( padictimes p is x x'' ) -> ( ( pr1 ( padicapart p is ) ) x' x'' ) ) ) as int. intros. apply impred. intros. apply ( pr1 ( padicapart p is ) ). apply ( setquotuniv3prop _ ( fun x x' x'' => hProppair _ ( int x x' x'' ) ) ). intros a b c. change (pr1 (padicapart p is) (padictimes p is (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (setquotpr (carryequiv p (isaprimetoneq0 is)) b)) (padictimes p is (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (setquotpr (carryequiv p (isaprimetoneq0 is)) c)) -> pr1 (padicapart p is) (setquotpr (carryequiv p (isaprimetoneq0 is)) b) (setquotpr (carryequiv p (isaprimetoneq0 is)) c)). unfold padictimes. rewrite 2! setquotprandpadictimes. rewrite 2! padicapartcomputation. intros j. apply ( padictimesisbinopapart0 p is a b c j ). Defined. Lemma padictimesisbinopapartr ( p : hz ) ( is : isaprime p ) : isbinopapartr ( padicapart p is ) ( padictimes p is ). Proof. intros. unfold isbinopapartr. intros a b c. unfold padictimes. rewrite ( @rngcomm2 ( commrngofpadicints p is ) b a ). rewrite ( @rngcomm2 ( commrngofpadicints p is ) c a ). apply padictimesisbinopapartl. Defined. Definition acommrngofpadicints ( p : hz ) ( is : isaprime p ) : acommrng. Proof. intros. split with ( commrngofpadicints p is ). split with ( padicapart p is ). split. split. apply ( padicplusisbinopapartl p is ). apply ( padicplusisbinopapartr p is ). split. apply ( padictimesisbinopapartl p is ). apply ( padictimesisbinopapartr p is ). Defined. (** * IV. The apartness domain of p-adic integers and the Heyting field of p-adic numbers *) Lemma precarryandzeromultl ( p : hz ) ( is : isaprime p ) ( a b : fpscommrng hz ) ( n : nat ) ( x : forall m : nat, natlth m n -> ( carry p ( isaprimetoneq0 is ) a m ~> 0%hz ) ) : forall m : nat, natlth m n -> precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ~> 0%hz. Proof. intros p is a b n x m y. induction m. simpl. unfold fpstimes. simpl. rewrite ( x 0%nat y ). rewrite hzmult0x. apply idpath. change ( natsummation0 ( S m ) ( fun z : nat => ( carry p ( isaprimetoneq0 is ) a z ) * ( carry p ( isaprimetoneq0 is ) b ( minus ( S m ) z ) ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ) ~> 0%hz ). assert ( natlth m n ) as u. apply ( istransnatlth _ ( S m ) _ ). apply natlthnsn. assumption. rewrite ( IHm u ). rewrite hzqrand0q. rewrite hzplusr0. assert ( natsummation0 (S m) (fun z : nat => carry p (isaprimetoneq0 is) a z * carry p (isaprimetoneq0 is) b ( minus ( S m ) z)) ~> ( natsummation0 ( S m ) ( fun z : nat => 0%hz ) ) ) as f. apply natsummationpathsupperfixed. intros k v. assert ( natlth k n ) as uu. apply ( natlehlthtrans _ ( S m ) _ ). assumption. assumption. rewrite ( x k uu ). rewrite hzmult0x. apply idpath. rewrite f. rewrite natsummationae0bottom. apply idpath. intros k l. apply idpath. Defined. Lemma precarryandzeromultr ( p : hz ) ( is : isaprime p ) ( a b : fpscommrng hz ) ( n : nat ) ( x : forall m : nat, natlth m n -> ( carry p ( isaprimetoneq0 is ) b m ~> 0%hz ) ) : forall m : nat, natlth m n -> precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ~> 0%hz. Proof. intros p is a b n x m y. change (fpstimes hz (carry p (isaprimetoneq0 is) a) (carry p (isaprimetoneq0 is) b)) with ( (carry p (isaprimetoneq0 is) a) * (carry p (isaprimetoneq0 is) b)). rewrite ( ( @rngcomm2 ( fpscommrng hz ) ) ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ). apply ( precarryandzeromultl p is b a n x m y ). Defined. Lemma hzfpstimesnonzero ( a : fpscommrng hz ) ( k : nat ) ( is : dirprod ( neq hz ( a k ) 0%hz ) ( forall m : nat, natlth m k -> ( a m ) ~> 0%hz ) ) : forall k' : nat, forall b : fpscommrng hz , forall is' : dirprod ( neq hz ( b k' ) 0%hz ) ( forall m : nat, natlth m k' -> ( b m ) ~> 0%hz ), ( a * b ) ( k + k' )%nat ~> ( a k ) * ( b k' ). Proof. intros a k is k'. induction k'. intros. destruct k. simpl. apply idpath. rewrite natplusr0. change ( natsummation0 k ( fun x : nat => a x * b ( minus ( S k ) x ) ) + a ( S k ) * b ( minus ( S k ) ( S k ) ) ~> a ( S k ) * b 0%nat ). assert ( natsummation0 k ( fun x : nat => a x * b ( minus ( S k ) x ) ) ~> natsummation0 k ( fun x : nat => 0%hz ) ) as f. apply natsummationpathsupperfixed. intros m i. assert ( natlth m ( S k ) ) as i0. apply ( natlehlthtrans _ k _ ). assumption. apply natlthnsn. rewrite ( ( pr2 is ) m i0 ). rewrite hzmult0x. apply idpath. rewrite f. rewrite natsummationae0bottom. rewrite hzplusl0. rewrite minusnn0. apply idpath. intros m i. apply idpath. intros. rewrite natplusnsm. change ( natsummation0 ( k + k' )%nat ( fun x : nat => a x * b ( minus ( S k + k' ) x ) ) + a ( S k + k' )%nat * b ( minus ( S k + k' ) ( S k + k' ) ) ~> a k * b ( S k' ) ). set ( b' := fpsshift b ). rewrite minusnn0. rewrite ( ( pr2 is' ) 0%nat ( natlehlthtrans 0 k' ( S k' ) ( natleh0n k' ) ( natlthnsn k' ) ) ). rewrite hzmultx0. rewrite hzplusr0. assert ( natsummation0 ( k + k' )%nat ( fun x : nat => a x * b ( minus ( S k + k' ) x ) ) ~> fpstimes hz a b' ( k + k' )%nat ) as f. apply natsummationpathsupperfixed. intros m v. change ( S k + k' )%nat with ( S ( k + k' ) ). rewrite <-( pathssminus ( k + k' )%nat m ). apply idpath. apply ( natlehlthtrans _ ( k + k' )%nat _ ). assumption. apply natlthnsn. rewrite f. apply ( IHk' b' ). split. apply is'. intros m v. unfold b'. unfold fpsshift. apply is'. assumption. Defined. Lemma hzfpstimeswhenzero ( a : fpscommrng hz ) ( m k : nat ) ( is : ( forall m : nat, natlth m k -> ( a m ) ~> 0%hz ) ) : forall b : fpscommrng hz, forall k' : nat, forall is' : ( forall m : nat, natlth m k' -> ( b m ) ~> 0%hz ) , natlth m ( k + k' )%nat -> ( a * b ) m ~> 0%hz. Proof. intros a m. induction m. intros k. intros is b k' is' j. change ( a 0%nat * b 0%nat ~> 0%hz ). destruct k. rewrite ( is' 0%nat j ). rewrite hzmultx0. apply idpath. assert ( natlth 0 ( S k ) ) as i. apply ( natlehlthtrans _ k _ ). apply natleh0n. apply natlthnsn. rewrite ( is 0%nat i ). rewrite hzmult0x. apply idpath. intros k is b k' is' j. change ( natsummation0 ( S m ) ( fun x : nat => a x * b ( minus ( S m ) x ) ) ~> 0%hz ). change ( natsummation0 m ( fun x : nat => a x * b ( minus ( S m ) x ) ) + a ( S m ) * b ( minus ( S m ) ( S m ) ) ~> 0%hz ). assert ( a ( S m ) * b ( minus ( S m ) ( S m ) ) ~> 0%hz ) as g. destruct k. destruct k'. assert empty. apply ( negnatgth0n ( S m ) j ). contradiction. rewrite minusnn0. rewrite ( is' 0%nat ( natlehlthtrans 0%nat k' ( S k' ) ( natleh0n k' ) ( natlthnsn k' ) ) ). rewrite hzmultx0. apply idpath. destruct k'. rewrite natplusr0 in j. rewrite ( is ( S m ) j ). rewrite hzmult0x. apply idpath. rewrite minusnn0. rewrite ( is' 0%nat ( natlehlthtrans 0%nat k' ( S k' ) ( natleh0n k' ) ( natlthnsn k' ) ) ). rewrite hzmultx0. apply idpath. rewrite g. rewrite hzplusr0. set ( b' := fpsshift b ). assert ( natsummation0 m ( fun x : nat => a x * b ( minus ( S m ) x ) ) ~> natsummation0 m ( fun x : nat => a x * b' ( minus m x ) ) ) as f. apply natsummationpathsupperfixed. intros n i. unfold b'. unfold fpsshift. rewrite pathssminus. apply idpath. apply ( natlehlthtrans _ m _ ). assumption. apply natlthnsn. rewrite f. change ( ( a * b' ) m ~> 0%hz ). assert ( natlth m ( k + k' ) ) as one. apply ( istransnatlth _ ( S m ) _ ). apply natlthnsn. assumption. destruct k'. assert ( forall m : nat, natlth m 0%nat -> b' m ~> 0%hz ) as two. intros m0 j0. assert empty. apply ( negnatgth0n m0). assumption. contradiction. apply ( IHm k is b' 0%nat two one ). assert ( forall m : nat, natlth m k' -> b' m ~> 0%hz ) as two. intros m0 j0. change ( b ( S m0 ) ~> 0%hz ). apply is'. assumption. assert ( natlth m ( k + k' )%nat ) as three. rewrite natplusnsm in j. apply j. apply ( IHm k is b' k' two three ). Defined. Lemma precarryandzeromult ( p : hz ) ( is : isaprime p ) ( a b : fpscommrng hz ) ( k k' : nat ) ( x : forall m : nat, natlth m k -> carry p ( isaprimetoneq0 is ) a m ~> 0%hz ) ( x' : forall m : nat, natlth m k' -> carry p ( isaprimetoneq0 is ) b m ~> 0%hz ) : forall m : nat, natlth m ( k + k' )%nat -> precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ~> 0%hz. Proof. intros p is a b k k' x x' m i. induction m. apply ( hzfpstimeswhenzero ( carry p ( isaprimetoneq0 is ) a ) 0%nat k x ( carry p ( isaprimetoneq0 is ) b ) k' x' i ). change ( ( ( carry p ( isaprimetoneq0 is ) a ) * ( carry p ( isaprimetoneq0 is ) b ) ) ( S m ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ) ~> 0%hz ). rewrite ( hzfpstimeswhenzero ( carry p ( isaprimetoneq0 is ) a ) ( S m ) k x ( carry p ( isaprimetoneq0 is ) b ) k' x' i ). rewrite hzplusl0. assert ( natlth m ( k + k' )%nat ) as one. apply ( istransnatlth _ ( S m ) _ ). apply natlthnsn. assumption. rewrite ( IHm one ). rewrite hzqrand0q. apply idpath. Defined. Lemma primedivorcoprime ( p a : hz ) ( is : isaprime p ) : hdisj ( hzdiv p a ) ( gcd p a ( isaprimetoneq0 is ) ~> 1 ). Proof. intros. intros P i. apply ( pr2 is ( gcd p a ( isaprimetoneq0 is ) ) ( pr1 ( gcdiscommondiv p a ( isaprimetoneq0 is ) ) ) ). intro t. apply i. destruct t as [ t0 | t1 ]. apply ii2. assumption. apply ii1. rewrite <- t1. exact ( pr2 ( gcdiscommondiv p a ( isaprimetoneq0 is ) ) ). Defined. Lemma primeandtimes ( p a b : hz ) ( is : isaprime p ) ( x : hzdiv p ( a * b ) ) : hdisj ( hzdiv p a ) ( hzdiv p b ). Proof. intros. apply ( primedivorcoprime p a is ). intros j. intros P i. apply i. destruct j as [ j0 | j1 ]. apply ii1. assumption. apply ii2. apply x. intro u. destruct u as [ k u ]. unfold hzdiv0 in u. set ( cd := bezoutstrong a p ( isaprimetoneq0 is ) ). destruct cd as [ cd f ]. destruct cd as [ c d ]. rewrite j1 in f. simpl in f. assert ( b ~> ( ( b * c + d * k ) * p ) ) as g. assert ( b ~> b * 1 ) as g0. rewrite hzmultr1. apply idpath. rewrite g0. rewrite ( rngrdistr hz ( b * 1 * c ) ( d * k ) p ). assert ( b * ( c * p + d * a ) ~> ( b * 1 * c * p + d * k * p ) ) as h. rewrite ( rngldistr hz ( c * p ) ( d * a ) b ). rewrite hzmultr1. rewrite 2! ( @rngassoc2 hz ). rewrite ( @rngcomm2 hz k p ). change ( p * k )%hz with ( p * k )%rng in u. rewrite u. rewrite ( @rngcomm2 hz b ( d * a ) ). rewrite ( @rngassoc2 hz ). apply idpath. rewrite <- h. rewrite f. apply idpath. intros Q uu. apply uu. split with ( b * c + d * k ). rewrite ( @rngcomm2 hz _ p ) in g. unfold hzdiv0. apply pathsinv0. assumption. Defined. Lemma hzremaindermodprimeandtimes ( p : hz ) ( is : isaprime p ) ( a b : hz ) ( x : hzremaindermod p ( isaprimetoneq0 is ) ( a * b ) ~> 0 ) : hdisj ( hzremaindermod p ( isaprimetoneq0 is ) a ~> 0) ( hzremaindermod p ( isaprimetoneq0 is ) b ~> 0). Proof. intros. assert ( hzdiv p ( a * b ) ) as i. intros P i'. apply i'. split with ( hzquotientmod p ( isaprimetoneq0 is ) ( a * b ) ). unfold hzdiv0. apply pathsinv0. rewrite <- ( hzplusr0 (p * hzquotientmod p (isaprimetoneq0 is) (a * b)%rng) )%hz. change (a * b ~> (p * hzquotientmod p (isaprimetoneq0 is) (a * b)%rng + 0)%rng). rewrite <- x. change (p * hzquotientmod p (isaprimetoneq0 is) (a * b) + hzremaindermod p (isaprimetoneq0 is) a * b) with (p * hzquotientmod p (isaprimetoneq0 is) (a * b)%rng + ( hzremaindermod p (isaprimetoneq0 is) a * b )%rng )%hz. apply ( hzdivequationmod p ( isaprimetoneq0 is ) ( a * b ) ). apply ( primeandtimes p a b is i ). intro t. destruct t as [ t0 | t1 ]. apply t0. intros k. destruct k as [ k k' ]. intros Q j. apply j. apply ii1. apply pathsinv0. apply ( hzqrtestr p ( isaprimetoneq0 is ) a k ). split. rewrite hzplusr0. unfold hzdiv0 in k'. rewrite k'. apply idpath. split. apply isreflhzleh. rewrite hzabsvalgth0. apply ( istranshzlth _ 1 _ ). apply hzlthnsn. apply is. apply ( istranshzlth _ 1 _ ). apply hzlthnsn. apply is. apply t1. intros k. destruct k as [ k k' ]. intros Q j. apply j. apply ii2. apply pathsinv0. apply ( hzqrtestr p ( isaprimetoneq0 is ) b k ). split. rewrite hzplusr0. unfold hzdiv0 in k'. rewrite k'. apply idpath. split. apply isreflhzleh. rewrite hzabsvalgth0. apply ( istranshzlth _ 1 _ ). apply hzlthnsn. apply is. apply ( istranshzlth _ 1 _ ). apply hzlthnsn. apply is. Defined. Definition padiczero ( p : hz ) ( is : isaprime p ) := @rngunel1 ( commrngofpadicints p is ). Definition padicone ( p : hz ) ( is : isaprime p ) := @rngunel2 ( commrngofpadicints p is ). Lemma padiczerocomputation ( p : hz ) ( is : isaprime p ) : padiczero p is ~> setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( @rngunel1 ( fpscommrng hz ) ). Proof. intros. apply idpath. Defined. Lemma padiconecomputation ( p : hz ) ( is : isaprime p ) : padicone p is ~> setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( @rngunel2 ( fpscommrng hz ) ). Proof. intros. apply idpath. Defined. Lemma padicintsareintdom ( p : hz ) ( is : isaprime p ) ( a b : acommrngofpadicints p is ) : a # 0 -> b # 0 -> a * b # 0. Proof. intros p is. assert ( forall a b : commrngofpadicints p is, isaprop ( ( pr1 ( padicapart p is ) ) a ( padiczero p is ) -> ( pr1 ( padicapart p is ) ) b ( padiczero p is ) -> ( pr1 ( padicapart p is ) ) ( padictimes p is a b ) ( padiczero p is ) ) ) as int. intros. apply impred. intros. apply impred. intros. apply ( pr1 ( padicapart p is ) ). apply ( setquotuniv2prop _ ( fun x y => hProppair _ ( int x y ) ) ). intros a b. change (pr1 (padicapart p is) (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (padiczero p is) -> pr1 (padicapart p is) (setquotpr (carryequiv p (isaprimetoneq0 is)) b) (padiczero p is) -> pr1 (padicapart p is) (padictimes p is (setquotpr (carryequiv p (isaprimetoneq0 is)) a) (setquotpr (carryequiv p (isaprimetoneq0 is)) b)) (padiczero p is)). unfold padictimes. rewrite padiczerocomputation. rewrite setquotprandpadictimes. rewrite 3! padicapartcomputation. intros i j. apply i. intros i0. destruct i0 as [ i0 i1 ]. apply j. intros j0. destruct j0 as [ j0 j1 ]. rewrite carryandzero in i1, j1. change ( ( @rngunel1 ( fpscommrng hz ) ) i0 ) with 0%hz in i1. change ( ( @rngunel1 ( fpscommrng hz ) ) j0 ) with 0%hz in j1. set ( P := fun x : nat => neq hz ( carry p ( isaprimetoneq0 is ) a x ) 0 ). set ( P' := fun x : nat => neq hz ( carry p ( isaprimetoneq0 is ) b x ) 0 ). assert ( isdecnatprop P ) as isdec1. intros m. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) a m ) 0%hz ) as [ l | r ]. apply ii2. intro v. apply v. assumption. apply ii1. assumption. assert ( isdecnatprop P' ) as isdec2. intros m. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b m ) 0%hz ) as [ l | r ]. apply ii2. intro v. apply v. assumption. apply ii1. assumption. set ( le1 := leastelementprinciple i0 P isdec1 i1 ). set ( le2 := leastelementprinciple j0 P' isdec2 j1 ). apply le1. intro k. destruct k as [ k k' ]. apply le2. intro o. destruct o as [ o o' ]. apply total2tohexists. split with ( k + o )%nat. assert ( forall m : nat, natlth m k -> carry p ( isaprimetoneq0 is ) a m ~> 0%hz ) as one. intros m m0. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) a m ) 0%hz ) as [ left0 | right0 ]. assumption. assert empty. apply ( ( pr2 k' ) m m0 ). assumption. contradiction. assert ( forall m : nat, natlth m o -> carry p ( isaprimetoneq0 is ) b m ~> 0%hz ) as two. intros m m0. destruct ( isdeceqhz ( carry p ( isaprimetoneq0 is ) b m ) 0%hz ) as [ left0 | right0 ]. assumption. assert empty. apply ( ( pr2 o' ) m m0 ). assumption. contradiction. assert ( dirprod ( neq hz ( carry p ( isaprimetoneq0 is ) a k ) 0%hz ) ( forall m : nat, natlth m k -> ( carry p ( isaprimetoneq0 is ) a m ) ~> 0%hz ) ) as three. split. apply k'. assumption. assert ( dirprod ( neq hz ( carry p ( isaprimetoneq0 is ) b o ) 0%hz ) ( forall m : nat, natlth m o -> ( carry p ( isaprimetoneq0 is ) b m ) ~> 0%hz ) ) as four. split. apply o'. assumption. set ( f := hzfpstimesnonzero ( carry p ( isaprimetoneq0 is ) a ) k three o ( carry p ( isaprimetoneq0 is ) b ) four ). rewrite carryandzero. change ( ( @rngunel1 ( fpscommrng hz ) ) ( k + o )%nat ) with 0%hz. rewrite carryandtimes. destruct k. destruct o. rewrite <- carryandtimes. intros v. change ( hzremaindermod p ( isaprimetoneq0 is ) ( a 0%nat * b 0%nat ) ~> 0%hz ) in v. assert hfalse. apply ( hzremaindermodprimeandtimes p is ( a 0%nat ) ( b 0%nat ) v ). intros t. destruct t as [ t0 | t1 ]. apply ( pr1 k' ). apply t0. apply ( pr1 o' ). apply t1. assumption. intros v. unfold carry at 1 in v. change ( 0 + S o )%nat with ( S o ) in v. change ( hzremaindermod p ( isaprimetoneq0 is ) ( ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) ( S o ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) o ) ) ~> 0%hz ) in v. change ( 0 + S o )%nat with ( S o) in f. rewrite f in v. change ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) with ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) in v. rewrite ( precarryandzeromult p is a b 0%nat ( S o ) ) in v. rewrite hzqrand0q in v. rewrite hzplusr0 in v. assert hfalse. apply ( hzremaindermodprimeandtimes p is ( carry p ( isaprimetoneq0 is ) a 0%nat ) ( carry p ( isaprimetoneq0 is ) b ( S o ) ) ). assumption. intros s. destruct s as [ l | r ]. apply k'. rewrite hzqrandcarryr. assumption. apply o'. rewrite hzqrandcarryr. assumption. assumption. apply one. apply two. apply natlthnsn. intros v. unfold carry at 1 in v. change ( hzremaindermod p ( isaprimetoneq0 is ) ( ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) ( S k + o )%nat + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) ( k + o )%nat ) ) ~> 0%hz ) in v. rewrite f in v. change ( carry p ( isaprimetoneq0 is ) a * carry p ( isaprimetoneq0 is ) b ) with ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) in v. rewrite ( precarryandzeromult p is a b ( S k ) o ) in v. rewrite hzqrand0q in v. rewrite hzplusr0 in v. assert hfalse. apply ( hzremaindermodprimeandtimes p is ( carry p ( isaprimetoneq0 is ) a ( S k ) ) ( carry p ( isaprimetoneq0 is ) b (o ) ) ). assumption. intros s. destruct s as [ l | r ]. apply k'. rewrite hzqrandcarryr. assumption. apply o'. rewrite hzqrandcarryr. assumption. assumption. apply one. apply two. apply natlthnsn. Defined. Definition padicintegers ( p : hz ) ( is : isaprime p ) : aintdom. Proof. intros. split with ( acommrngofpadicints p is ). split. change ( ( pr1 ( padicapart p is ) ) ( padicone p is ) ( padiczero p is ) ). rewrite ( padiczerocomputation p is ). rewrite ( padiconecomputation p is ). rewrite padicapartcomputation. apply total2tohexists. split with 0%nat. unfold carry. unfold precarry. rewrite hzqrand1r. rewrite hzqrand0r. apply isnonzerornghz. apply padicintsareintdom. Defined. Definition padics ( p : hz ) ( is : isaprime p ) : afld := afldfrac ( padicintegers p is ). Close Scope rng_scope. (** END OF FILE*)Pelayo-Coq/._z_mod_p.v000777 000765 000024 00000000324 12104265254 015501 0ustar00nicolastaff000000 000000 Mac OS X  2¢ÔATTRÔ˜<˜<com.apple.quarantineq/0002;53a854a1;Safari;5085629F-B604-4322-A539-1F4796CB8AB1Pelayo-Coq/z_mod_p.v000777 000765 000024 00000173274 12104265254 015303 0ustar00nicolastaff000000 000000 (** *Integers mod p *) (** By Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren *) (** December 2011 *) (** Settings *) Add Rec LoadPath "../Generalities". Add Rec LoadPath "../hlevel1". Add Rec LoadPath "../hlevel2". Add Rec LoadPath "../Proof_of_Extensionality". Add Rec LoadPath "../Algebra". Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *) (** Imports *) Require Export lemmas. Open Scope hz_scope. (** * I. Divisibility and the division algorithm *) Definition hzdiv0 : hz -> hz -> hz -> UU := fun n m k => ( n * k ~> m ). Definition hzdiv : hz -> hz -> hProp := fun n m => hexists ( fun k : hz => hzdiv0 n m k ). Lemma hzdivisrefl : isrefl ( hzdiv ). Proof. unfold isrefl. intro. unfold hzdiv. apply total2tohexists. split with 1. apply hzmultr1. Defined. Lemma hzdivistrans : istrans ( hzdiv ). Proof. intros a b c p q. apply p. intro k. destruct k as [ k f ]. apply q. intro l. destruct l as [ l g ]. intros P s. apply s. unfold hzdiv0 in f,g. split with ( k * l ). unfold hzdiv0. rewrite <- hzmultassoc. rewrite f. assumption. Defined. Lemma hzdivlinearcombleft ( a b c d : hz ) ( f : a ~> ( b + c ) ) ( x : hzdiv d a ) ( y : hzdiv d b ) : hzdiv d c. Proof. intros a b c d f x y P s. apply x. intro x'. apply y. intro y'. destruct x' as [ k g ]. destruct y' as [ l h ]. unfold hzdiv0 in *. apply s. split with ( k + - l ). rewrite hzldistr. rewrite g. rewrite ( rngrmultminus hz ). change ( ( a + ( - ( d * l ) ) )%hz ~> c ). rewrite h. apply ( hzplusrcan _ _ b ). rewrite hzplusassoc. rewrite hzlminus. rewrite hzplusr0. rewrite hzpluscomm. assumption. Defined. Lemma hzdivlinearcombright ( a b c d : hz ) ( f : a ~> ( b + c ) ) ( x : hzdiv d b ) ( y : hzdiv d c ) : hzdiv d a. Proof. intros a b c d f x y P s. apply x. intro x'. apply y. intro y'. destruct x' as [ k g ]. destruct y' as [ l h ]. unfold hzdiv0 in *. apply s. split with ( k + l ). rewrite hzldistr. change ( (d * k + d * l)%hz ~> a ). rewrite g, h, f. apply idpath. Defined. Lemma divalgorithmnonneg ( n : nat ) ( m : nat ) ( p : hzlth 0 ( nattohz m ) ) : total2 ( fun qr : dirprod hz hz => ( ( dirprod ( nattohz n ~> ( ( ( nattohz m ) * ( pr1 qr ) ) + ( pr2 qr ) ) ) ( dirprod ( hzleh 0 ( pr2 qr ) ) ( hzlth ( pr2 qr ) ( nattohz ( m ) ) ) ) ) ) ). Proof. intro. intro. induction n. intros. split with ( dirprodpair 0 0 ). split. simpl. rewrite ( rngrunax1 hz ). rewrite ( rngmultx0 hz ). rewrite nattohzand0. change ( 0 ~> 0%hz ). apply idpath. split. apply isreflhzleh. assumption. intro p. set ( q' := pr1 ( pr1 ( IHn p ) ) ). set ( r' := pr2 ( pr1 ( IHn p ) ) ). set ( f := pr1 ( pr2 ( IHn p ) ) ). assert ( hzleh ( r' + 1 ) ( nattohz m ) ) as p'. assert ( hzlth ( r' + 1 ) ( nattohz m + 1 ) ) as p''. apply hzlthandplusr. apply ( pr2 ( pr2 ( pr2 ( IHn p ) ) ) ). apply hzlthsntoleh. assumption. set ( choice := hzlehchoice ( r' + 1 ) ( nattohz m ) p' ). destruct choice as [ k | h ]. split with ( dirprodpair q' ( r' + 1 ) ). split. rewrite (nattohzandS _ ). rewrite hzpluscomm. rewrite f. change ( nattohz m * q' + r' + 1 ~> ( nattohz m * q' + ( r' + 1 ) ) ). apply rngassoc1. split. apply ( istranshzleh 0 r' ( r' + 1 ) ). apply ( ( pr2 ( pr2 ( IHn p ) ) ) ). apply hzlthtoleh. apply hzlthnsn. assumption. split with ( dirprodpair ( q' + 1 ) 0 ). split. rewrite ( nattohzandS _ ). rewrite hzpluscomm. rewrite f. change ( nattohz m * q' + r' + 1 ~> ( nattohz m * ( q' + 1 ) + 0 ) ). rewrite ( hzplusassoc ). rewrite h. rewrite ( rngldistr _ q' _ ). rewrite rngrunax2. rewrite hzplusr0. apply idpath. split. apply isreflhzleh. assumption. Defined. (* A test of the division algorithm for non-negative integers: Lemma testlemma1 : ( hzneq 0 ( 1 ) ). Proof. change 0 with ( nattohz 0%nat ). rewrite <- nattohzand1. apply nattohzandneq. intro f. apply ( isirreflnatlth 1 ). assert ( natlth 0 1 ) as i. apply natlthnsn. rewrite <- f in *. assumption. Defined. Lemma testlemma2 : ( hzneq 0 ( 1 + 1 ) ). Proof. change 0 with ( nattohz 0%nat ). rewrite <- nattohzand1. rewrite <- nattohzandplus. apply nattohzandneq. assert ( natneq ( 1 + 1 ) 0 ) as x. apply ( natgthtoneq ( 1 + 1 ) 0 ). simpl. auto. intro f. apply x. apply pathsinv0. assumption. Defined. Lemma testlemma21 : hzlth 0 ( nattohz 2 ). Proof. change 0 with ( nattohz 0%nat ). apply nattohzandlth. apply ( istransnatlth _ 1 ). apply natlthnsn. apply natlthnsn. Defined. Lemma testlemma3 : hzlth 0 ( nattohz 3 ). Proof. apply ( istranshzlth _ ( nattohz 2 ) ). apply testlemma21. change 0 with ( nattohz 0%nat ). apply nattohzandlth. apply natlthnsn. Defined. Lemma testlemma9 : hzlth 0 ( nattohz 9 ). Proof. apply ( istranshzlth _ ( nattohz 3 ) ). apply testlemma3. apply ( istranshzlth _ ( nattohz 6 ) ). apply testlemma3. apply testlemma3. Defined. Eval lazy in hzabsval ( pr1 ( pr1 ( divalgorithmnonneg 1 ( 1 + 1 ) testlemma21 ) ) ). Eval lazy in hzabsval ( pr1 ( pr1 ( divalgorithmnonneg ( 5 ) ( 1 + 1 ) testlemma21 ) ) ). Eval lazy in hzabsval ( pr2 ( pr1 ( divalgorithmnonneg ( 5 ) ( 1 + 1 ) testlemma21 ) ) ). Eval lazy in hzabsval ( pr1 ( pr1 ( divalgorithmnonneg 16 3 testlemma3 ) ) ). Eval lazy in hzabsval ( pr2 ( pr1 ( divalgorithmnonneg 16 3 testlemma3 ) ) ). Eval lazy in hzabsval ( pr1 ( pr1 ( divalgorithmnonneg 18 9 testlemma9 ) ) ). Eval lazy in hzabsval ( pr2 ( pr1 ( divalgorithmnonneg 18 9 testlemma9 ) ) ). *) Theorem divalgorithmexists ( n m : hz ) ( p : hzneq 0 m ) : total2 ( fun qr : dirprod hz hz => ( ( dirprod ( n ~> ( ( m * ( pr1 qr ) ) + ( pr2 qr ) ) ) ( dirprod ( hzleh 0 ( pr2 qr ) ) ( hzlth ( pr2 qr ) ( nattohz ( hzabsval m ) ) ) ) ) ) ). Proof. intros. destruct ( hzlthorgeh n 0 ) as [ n_neg | n_nonneg ]. destruct ( hzlthorgeh m 0 ) as [ m_neg | m_nonneg ]. (*Case I: n<0, m<0:*) set ( n' := hzabsval n ). set ( m' := hzabsval m ). assert ( nattohz m' ~> ( - m ) ) as f. apply hzabsvallth0. assumption. assert ( - - n ~> - ( nattohz n' ) ) as f0. rewrite <- ( hzabsvallth0 n_neg ). rewrite ( hzabsvallth0 n_neg ). unfold n'. rewrite ( hzabsvallth0 n_neg ). apply idpath. assert ( hzlth 0 ( nattohz m' ) ) as p'. assert ( hzlth 0 ( - m ) ) as q. apply hzlth0andminus. assumption. rewrite f. assumption. set ( a := divalgorithmnonneg n' m' p' ). set ( q := pr1 ( pr1 a ) ). set ( r := pr2 ( pr1 a ) ). set ( Q := q + 1 ). set ( R := - m - r ). destruct ( hzlehchoice 0 r ( pr1 ( pr2 ( pr2 a ) ) )) as [ less | equal ]. split with ( dirprodpair Q R ). split. rewrite ( pathsinv0( rngminusminus hz n) ). assert ( - nattohz n' ~> ( m * Q + R ) ) as f1. unfold Q. unfold R. rewrite ( pr1 ( ( pr2 a ) ) ). change ( pr1 ( pr1 a ) ) with q. change ( pr2 ( pr1 a ) ) with r. rewrite hzaddinvplus. rewrite <- ( rnglmultminus hz ). rewrite f. rewrite ( rngminusminus ). rewrite ( rngldistr _ q _ _ ). rewrite ( hzmultr1 ). change ( ( m * q ) + - r ~> ( ( m * q + m ) + ( - m + - r ) ) ). rewrite ( hzplusassoc ). rewrite <- ( hzplusassoc m _ _ ). change ( m + - m ) with ( m - m ). rewrite ( hzrminus ). rewrite ( hzplusl0 ). apply idpath. exact ( pathscomp0 f0 f1 ). split. unfold R. assert ( hzlth r ( - m ) ) as u. rewrite <- hzabsvalleh0. apply ( pr2 ( pr2 ( pr2 ( a ) ) ) ). apply hzlthtoleh. assumption. rewrite <- ( hzlminus m ). change ( pr2 ( dirprodpair Q ( - m - r ) ) ) with ( - m - r ). apply hzlehandplusl. apply hzlthtoleh. rewrite <- ( rngminusminus hz m ). apply hzlthminusswap. assumption. unfold R. unfold m'. rewrite hzabsvalleh0. change ( hzlth ( - m + - r ) ( - m ) ). assert ( hzlth ( - m - r ) ( - m + 0 ) ) as u. apply hzlthandplusl. apply hzgth0andminus. apply less. assert ( - m + 0 ~> ( - m ) ) as f'. apply hzplusr0. exact ( transportf ( fun x : _ => hzlth ( - m + - r ) x ) f' u ). apply hzlthtoleh. assumption. split with (dirprodpair q 0 ). split. rewrite <- ( rngminusminus hz n ). assert ( - nattohz n' ~> ( m * q + 0 ) ) as f1. rewrite ( pr1 ( pr2 (a ) ) ). change ( pr1 (pr1 a ) ) with q. change ( pr2 ( pr1 a ) ) with r. rewrite hzplusr0. rewrite ( pathsinv0 equal ). rewrite ( hzplusr0 ). assert ( - ( nattohz m' * q ) ~> ( ( - ( nattohz m' ) ) * q ) ) as f2. apply pathsinv0. apply rnglmultminus. rewrite f2. unfold m'. rewrite hzabsvalleh0. apply ( maponpaths ( fun x : _ => x * q ) ). apply rngminusminus. apply hzlthtoleh. assumption. exact ( pathscomp0 f0 f1 ). split. change ( pr2 ( dirprodpair q 0 ) ) with 0. apply ( isreflhzleh ). rewrite equal. change ( pr2 ( dirprodpair q r ) ) with r. apply ( pr2 ( pr2 ( pr2 ( a ) ) ) ). destruct ( hzgehchoice m 0 m_nonneg ) as [ h | k ]. (*====*) (*Case II: n<0, m>0. *) assert ( hzlth 0 ( nattohz ( hzabsval m ) ) ) as p'. rewrite ( hzabsvalgth0 ). apply h. assumption. set ( a := divalgorithmnonneg ( hzabsval n ) ( hzabsval m ) p' ). set ( q' := pr1 ( pr1 a ) ). set ( r' := pr2 ( pr1 a ) ). assert ( n ~> - - n ) as f0. apply pathsinv0. apply rngminusminus. assert ( - - n ~> - ( nattohz ( hzabsval n ) ) ) as f1. apply pathsinv0. apply maponpaths. apply ( hzabsvalleh0 ). apply hzlthtoleh. assumption. destruct ( hzlehchoice 0 r' ( pr1 ( pr2 ( pr2 ( a ) ) ) ) ) as [ less | equal ]. split with (dirprodpair ( - q' - 1 ) ( m - r' ) ). split. change ( pr1 ( dirprodpair ( - q' - 1 ) ( m - r' ) ) ) with ( - q' - 1 ). change ( pr2 ( dirprodpair ( - q' - 1 ) ( m - r' ) ) ) with ( m - r' ). change ( - q' - 1 ) with ( - q' + ( - 1%hz ) ). rewrite hzldistr. assert ( - nattohz ( hzabsval n ) ~> ( ( m * ( - q' ) + m * ( - 1%hz ) ) + ( m - r' ) ) ) as f2. rewrite ( pr1 ( pr2 ( a ) ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. rewrite hzabsvalgth0. rewrite hzaddinvplus. rewrite ( rngrmultminus hz ). rewrite ( hzplusassoc _ ( m * ( - 1%hz ) ) _ ). apply ( maponpaths ( fun x : _ => - ( m * q' ) + x ) ). assert ( - m + ( m - r' ) ~> ( m * ( - 1%hz ) + ( m - r' ) ) ) as f3. apply ( maponpaths ( fun x : _ => x + ( m - r' ) ) ). apply pathsinv0. assert ( m * ( - 1%hz ) ~> ( - ( m * 1%hz ) ) ) as f30. apply ( rngrmultminus ). assert ( - ( m * 1 ) ~> - m ) as f31. rewrite hzmultr1. apply idpath. rewrite f30. assumption. assert ( - r' ~> ( - m + ( m - r' ) ) ) as f4. change ( - r' ~> ( -m + ( m + - r' ) ) ). rewrite <- ( hzplusassoc ). rewrite ( hzlminus ), ( hzplusl0 ). apply idpath. rewrite f4. assumption. assumption. rewrite f0, f1. assumption. split. change ( pr2 ( dirprodpair ( - q' - 1 ) ( m - r' ) ) ) with ( m - r' ). apply hzlthtoleh. rewrite <- ( hzrminus r' ). apply hzlthandplusr. rewrite <- ( hzabsvalgeh0 m_nonneg ). apply ( pr2 ( pr2 ( a ) ) ). rewrite ( hzabsvalgeh0 m_nonneg ). assert ( hzlth ( m - r' ) ( m + 0 ) ) as u. apply ( hzlthandplusl ). apply ( hzgth0andminus ). apply less. rewrite hzplusr0 in u. assumption. split with ( dirprodpair ( - q' ) 0 ). split. change ( pr1 ( dirprodpair ( - q' ) 0 ) ) with ( - q' ). change ( pr2 ( dirprodpair ( - q' ) 0 ) ) with 0. assert ( - nattohz ( hzabsval n ) ~> ( m * - q' + 0 ) ) as f2. rewrite ( hzplusr0 ). rewrite ( pr1 ( pr2 ( a ) ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. rewrite <- equal. rewrite hzplusr0. rewrite hzabsvalgeh0. apply pathsinv0. apply rngrmultminus. assumption. rewrite f0, f1. assumption. split. apply ( isreflhzleh ). rewrite equal. apply ( pr2 ( pr2 ( pr2 ( a ) ) ) ). assert empty. apply p. apply pathsinv0. assumption. contradiction. set ( choice2 := hzlthorgeh m 0 ). destruct choice2 as [ m_neg | m_nonneg ]. (*Case III. Assume n>=0, m<0:*) assert ( hzlth 0 ( nattohz ( hzabsval m ) ) ) as p'. rewrite ( hzabsvallth0 ). rewrite <- ( rngminusminus hz m ) in m_neg. set ( d:= hzlth0andminus m_neg ). rewrite rngminusminus in d. apply d. assumption. set ( a := divalgorithmnonneg ( hzabsval n ) ( hzabsval m ) p' ). set ( q' := pr1 ( pr1 a ) ). set ( r' := pr2 ( pr1 a ) ). split with ( dirprodpair ( - q' ) r' ). split. rewrite <- ( hzabsvalgeh0 ). rewrite ( pr1 ( pr2 ( a ) ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. change ( pr1 ( dirprodpair ( - q' ) r' ) ) with ( - q' ). change ( pr2 ( dirprodpair ( - q' ) r' ) ) with r'. rewrite ( hzabsvalleh0 ). apply ( maponpaths ( fun x : _ => x + r' ) ). assert ( - m * q' ~> - ( m * q' ) ) as f0. apply rnglmultminus. assert ( - ( m * q' ) ~> m * ( - q' ) ) as f1. apply pathsinv0. apply rngrmultminus. exact ( pathscomp0 f0 f1 ). apply hzlthtoleh. assumption. assumption. split. apply ( pr1 ( pr2 ( pr2 ( a ) ) ) ). apply ( pr2 ( pr2 ( pr2 ( a ) ) ) ). (*Case IV: n>=0, m>0.*) assert ( hzlth 0 ( nattohz ( hzabsval m ) ) ) as p'. rewrite ( hzabsvalgeh0 ). destruct ( hzneqchoice 0 m ) as [ l | r ]. apply p. assert empty. apply ( isirreflhzgth 0 ). apply ( hzgthgehtrans 0 m 0 ). assumption. assumption. contradiction. assumption. assumption. set ( a := divalgorithmnonneg ( hzabsval n ) ( hzabsval m ) p' ). set ( q' := pr1 ( pr1 a ) ). set ( r' := pr2 ( pr1 a ) ). split with ( dirprodpair q' r' ). split. rewrite <- hzabsvalgeh0. rewrite ( pr1 ( pr2 ( a ) ) ). change ( pr1 ( pr1 a ) ) with q'. change ( pr2 ( pr1 a ) ) with r'. change ( pr1 ( dirprodpair q' r' ) ) with q'. change ( pr2 ( dirprodpair q' r' ) ) with r'. rewrite hzabsvalgeh0. apply idpath. assumption. assumption. split. apply ( pr1 ( pr2 ( pr2 ( a ) ) ) ). apply ( pr2 ( pr2 ( pr2 ( a ) ) ) ). Defined. Lemma hzdivhzabsval ( a b : hz ) ( p : hzdiv a b ) : hdisj ( natleh ( hzabsval a ) ( hzabsval b ) ) ( hzabsval b ~> 0%nat ). Proof. intros a b p P q. apply ( p P ). intro t. destruct t as [ k f ]. unfold hzdiv0 in f. apply q. apply natdivleh with ( hzabsval k ). rewrite ( hzabsvalandmult ). rewrite f. apply idpath. Defined. Lemma divalgorithm ( n m : hz ) ( p : hzneq 0 m ) : iscontr ( total2 ( fun qr : dirprod hz hz => ( ( dirprod ( n ~> ( ( m * ( pr1 qr ) ) + ( pr2 qr ) ) ) ( dirprod ( hzleh 0 ( pr2 qr ) ) ( hzlth ( pr2 qr ) ( nattohz ( hzabsval m ) ) ) ) ) ) ) ). Proof. intros. split with ( divalgorithmexists n m p ). intro t. destruct t as [ qr' t' ]. destruct qr' as [ q' r' ]. simpl in t'. destruct t' as [ f' p2p2t ]. destruct p2p2t as [ p1p2p2t p2p2p2t ]. destruct divalgorithmexists as [ qr v ]. destruct qr as [ q r ]. destruct v as [ f p2p2dae ]. destruct p2p2dae as [ p1p2p2dae p2p2p2dae ]. simpl in f. simpl in p1p2p2dae. simpl in p2p2p2dae. assert ( r' ~> r ) as h. (*Proof that r' ~> r :*) assert ( m * ( q - q' ) ~> ( r' - r ) ) as h0. change ( q - q' ) with ( q + - q' ). rewrite ( hzldistr ). rewrite <- ( hzplusr0 ( r' - r ) ). rewrite <- ( hzrminus ( m * q' ) ). change ( r' - r ) with ( r' + ( - r ) ). rewrite ( hzplusassoc r' ). change ( ( m * q' ) - ( m * q' ) ) with ( ( m * q' ) + ( - ( m * q' ) ) ). rewrite <- ( hzplusassoc ( - r ) ). rewrite ( hzpluscomm ( -r ) ). rewrite <- ( hzplusassoc r' ). rewrite <- ( hzplusassoc r' ). rewrite ( hzpluscomm r' ). rewrite <- f'. rewrite f. rewrite ( hzplusassoc ( m * q ) ). change ( r + - r ) with ( r - r ). rewrite ( hzrminus ). rewrite ( hzplusr0 ). rewrite ( rngrmultminus hz ). change ( m * q + - ( m * q' ) ) with ( ( m * q + - ( m * q' ) )%rng ). apply idpath. assert ( hdisj ( natleh ( hzabsval m ) ( hzabsval ( r' - r ) ) ) ( hzabsval ( r' - r ) ~> 0%nat ) ) as v. apply hzdivhzabsval. intro P. intro s. apply s. split with ( q - q' ). unfold hzdiv0. assumption. assert ( isaprop ( r' ~> r ) ) as P. apply ( isasethz ). apply ( v ( hProppair ( r' ~> r ) P ) ). intro s. destruct s as [ left | right ]. assert ( hzlth ( nattohz ( hzabsval ( r' - r ) ) ) ( nattohz ( hzabsval m ) ) ) as u. destruct ( hzgthorleh r' r ) as [ greater | lesseq ]. assert ( hzlth 0 ( r' - r ) ) as e. rewrite <- ( hzrminus r ). apply hzlthandplusr. assumption. rewrite ( hzabsvalgth0 ). apply hzlthminus. apply ( p2p2p2t ). apply ( p2p2p2dae ). apply ( p1p2p2dae ). apply e. destruct ( hzlehchoice r' r lesseq ) as [ less | equal ]. rewrite hzabsvalandminuspos. rewrite hzabsvalgth0. apply hzlthminus. apply ( p2p2p2dae ). apply ( p2p2p2t ). apply ( p1p2p2t). apply hzlthminusequiv. assumption. apply ( p1p2p2t ). apply p1p2p2dae. rewrite equal. rewrite hzrminus. rewrite hzabsval0. rewrite nattohzand0. apply hzabsvalneq0. intro Q. apply p. assumption. assert empty. apply ( isirreflhzlth ( nattohz ( hzabsval m ) ) ). apply ( hzlehlthtrans _ ( nattohz ( hzabsval ( r' - r ) ) ) _ ). apply nattohzandleh. assumption. assumption. contradiction. assert ( r' ~> r ) as i. assert ( r' - r ~> 0 ) as i0. apply hzabsvaleq0. assumption. rewrite <- ( hzplusl0 r ). rewrite <- ( hzplusr0 r' ). assert ( r' + ( r - r ) ~> ( 0 + r ) ) as i00. change ( r - r ) with ( r + - r ). rewrite ( hzpluscomm _ ( - r ) ). rewrite <- hzplusassoc. apply ( maponpaths ( fun x : _ => x + r ) ). apply i0. exact ( transportf ( fun x : _ => ( r' + x ~> ( 0 + r ) ) ) ( ( hzrminus r ) ) i00 ). apply i. assert ( q' ~> q ) as g. (* Proof that q' ~> q:*) rewrite h in f'. rewrite f in f'. apply ( hzmultlcan q' q m ). intro i. apply p. apply pathsinv0. assumption. apply ( hzplusrcan ( m * q' ) ( m * q ) r ). apply pathsinv0. apply f'. (* Path in direct product: *) assert ( dirprodpair q' r' ~> ( dirprodpair q r ) ) as j. apply pathsdirprod. assumption. assumption. (* Proof of general path: *) apply pathintotalfiber with ( p0 := j ). assert ( iscontr ( dirprod ( n ~> ( m * q + r ) ) ( dirprod ( hzleh 0 r ) ( hzlth r ( nattohz ( hzabsval m ) ) ) ) ) ) as contract. change iscontr with ( isofhlevel 0 ). apply isofhleveldirprod. split with f. intro t. apply isasethz. apply isofhleveldirprod. split with p1p2p2dae. intro t. apply hzleh. split with p2p2p2dae. intro t. apply hzlth. apply proofirrelevancecontr. assumption. Defined. Definition hzquotientmod ( p : hz ) ( x : hzneq 0 p ) : hz -> hz := fun n : hz => ( pr1 ( pr1 ( divalgorithmexists n p x ) ) ). Definition hzremaindermod ( p : hz ) ( x : hzneq 0 p ) : hz -> hz := fun n : hz => ( pr2 ( pr1 ( divalgorithmexists n p x ) ) ). Definition hzdivequationmod ( p : hz ) ( x : hzneq 0 p ) ( n : hz ) : n ~> ( p * ( hzquotientmod p x n ) + ( hzremaindermod p x n ) ) := ( pr1 ( pr2 ( divalgorithmexists n p x ) ) ). Definition hzleh0remaindermod ( p : hz ) ( x : hzneq 0 p ) ( n : hz ) : hzleh 0 ( hzremaindermod p x n ) := ( pr1 ( pr2 ( pr2 ( divalgorithmexists n p x ) ) ) ). Definition hzlthremaindermodmod ( p : hz ) ( x : hzneq 0 p ) ( n : hz ) : hzlth ( hzremaindermod p x n ) ( nattohz ( hzabsval p ) ) := ( pr2 ( pr2 ( pr2 ( divalgorithmexists n p x ) ) ) ). (* Eval lazy in hzabsval ( ( ( hzquotientmod ( 1 + 1 ) testlemma2 ( 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ) ) ) ). Eval lazy in hzabsval ( ( ( hzremaindermod ( 1 + 1 ) testlemma2 ( 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ) ) ) ). *) (** * II. QUOTIENTS AND REMAINDERS *) Definition isaprime ( p : hz ) : UU := dirprod ( hzlth 1 p ) ( forall m : hz, ( hzdiv m p ) -> ( hdisj ( m ~> 1 ) ( m ~> p ) ) ). Lemma isapropisaprime ( p : hz ) : isaprop ( isaprime p ). Proof. intros. apply isofhleveldirprod. apply ( hzlth 1 p ). apply impred. intro m. apply impredfun. apply ( hdisj ( m ~> 1 ) ( m ~> p ) ). Defined. Lemma isaprimetoneq0 { p : hz } ( x : isaprime p ) : hzneq 0 p. Proof. intros. intros f. apply ( isirreflhzlth 0 ). apply ( istranshzlth _ 1 _ ). apply hzlthnsn. rewrite f. apply ( pr1 x ). Defined. Lemma hzqrtest ( m : hz ) ( x : hzneq 0 m ) ( a q r : hz ) : dirprod ( a ~> ( ( m * q ) + r ) ) ( dirprod ( hzleh 0 r ) ( hzlth r ( nattohz (hzabsval m ) ) ) ) -> dirprod ( q ~> hzquotientmod m x a ) ( r ~> hzremaindermod m x a ). Proof. intros m x a q r d. set ( k := tpair ( P := ( fun qr : dirprod hz hz => dirprod ( a ~> ( m * ( pr1 qr ) + pr2 qr ) ) ( dirprod ( hzleh 0 ( pr2 qr ) ) ( hzlth ( pr2 qr ) ( nattohz ( hzabsval m ) ) ) ) ) ) ( dirprodpair q r ) d ). assert ( k ~> ( pr1 ( divalgorithm a m x ) ) ) as f. apply ( pr2 ( divalgorithm a m x ) ). split. change q with ( pr1 ( pr1 k ) ). rewrite f. apply idpath. change r with ( pr2 ( pr1 k ) ). rewrite f. apply idpath. Defined. Definition hzqrtestq ( m : hz ) ( x : hzneq 0 m ) ( a q r : hz ) ( d : dirprod ( a ~> ( ( m * q ) + r ) ) ( dirprod ( hzleh 0 r ) ( hzlth r ( nattohz (hzabsval m ) ) ) ) ) := pr1 ( hzqrtest m x a q r d ). Definition hzqrtestr ( m : hz ) ( x : hzneq 0 m ) ( a q r : hz ) ( d : dirprod ( a ~> ( ( m * q ) + r ) ) ( dirprod ( hzleh 0 r ) ( hzlth r ( nattohz (hzabsval m ) ) ) ) ) := pr2 ( hzqrtest m x a q r d ). Lemma hzqrand0eq ( p : hz ) ( x : hzneq 0 p ) : 0 ~> ( ( p * 0 ) + 0 ). Proof. intros. rewrite hzmultx0. rewrite hzplusl0. apply idpath. Defined. Lemma hzqrand0ineq ( p : hz ) ( x : hzneq 0 p ) : dirprod ( hzleh 0 0 ) ( hzlth 0 ( nattohz ( hzabsval p ) ) ). Proof. intros. split. apply isreflhzleh. apply hzabsvalneq0. assumption. Defined. Lemma hzqrand0q ( p : hz ) ( x : hzneq 0 p ) : hzquotientmod p x 0 ~> 0. Proof. intros. apply pathsinv0. apply ( hzqrtestq p x 0 0 0 ). split. apply ( hzqrand0eq p x ). apply ( hzqrand0ineq p x ). Defined. Lemma hzqrand0r ( p : hz ) ( x : hzneq 0 p ) : hzremaindermod p x 0 ~> 0. Proof. intros. apply pathsinv0. apply ( hzqrtestr p x 0 0 0 ). split. apply ( hzqrand0eq p x ). apply ( hzqrand0ineq p x ). Defined. Lemma hzqrand1eq ( p : hz ) ( is : isaprime p ) : 1 ~> ( ( p * 0 ) + 1 ). Proof. intros. rewrite hzmultx0. rewrite hzplusl0. apply idpath. Defined. Lemma hzqrand1ineq ( p : hz ) ( is : isaprime p ) : dirprod ( hzleh 0 1 ) ( hzlth 1 ( nattohz ( hzabsval p ) ) ). Proof. intros. split. apply hzlthtoleh. apply hzlthnsn. rewrite ( hzabsvalgth0 ). apply is. apply ( istranshzgth _ 1 _ ). apply is. apply ( hzgthsnn 0 ). Defined. Lemma hzqrand1q ( p : hz ) ( is : isaprime p ) : hzquotientmod p ( isaprimetoneq0 is ) 1 ~> 0. Proof. intros. apply pathsinv0. apply ( hzqrtestq p ( isaprimetoneq0 is ) 1 0 1 ). split. apply ( hzqrand1eq p is ). apply ( hzqrand1ineq p is ). Defined. Lemma hzqrand1r ( p : hz ) ( is : isaprime p ) : hzremaindermod p ( isaprimetoneq0 is ) 1 ~> 1. Proof. intros. apply pathsinv0. apply ( hzqrtestr p ( isaprimetoneq0 is ) 1 0 1 ). split. apply ( hzqrand1eq p is ). apply ( hzqrand1ineq p is ). Defined. Lemma hzqrandselfeq ( p : hz ) ( x : hzneq 0 p ) : p ~> ( p * 1 + 0 ). Proof. intros. rewrite hzmultr1. rewrite hzplusr0. apply idpath. Defined. Lemma hzqrandselfineq ( p : hz ) ( x : hzneq 0 p ) : dirprod ( hzleh 0 0 ) ( hzlth 0 ( nattohz ( hzabsval p ) ) ). Proof. split. apply isreflhzleh. apply hzabsvalneq0. assumption. Defined. Lemma hzqrandselfq ( p : hz ) ( x : hzneq 0 p ) : hzquotientmod p x p ~> 1. Proof. intros. apply pathsinv0. apply ( hzqrtestq p x p 1 0 ). split. apply ( hzqrandselfeq p x ). apply ( hzqrandselfineq p x ). Defined. Lemma hzqrandselfr ( p : hz ) ( x : hzneq 0 p ) : hzremaindermod p x p ~> 0. Proof. intros. apply pathsinv0. apply ( hzqrtestr p x p 1 0 ). split. apply ( hzqrandselfeq p x ). apply ( hzqrandselfineq p x ). Defined. Lemma hzqrandpluseq ( p : hz ) ( x : hzneq 0 p ) ( a c : hz ) : ( a + c ) ~> ( ( p * ( hzquotientmod p x a + hzquotientmod p x c + hzquotientmod p x ( hzremaindermod p x a + hzremaindermod p x c ) ) ) + hzremaindermod p x ( ( hzremaindermod p x a ) + ( hzremaindermod p x c ) ) ). Proof. intros. rewrite 2! ( hzldistr ). rewrite ( hzplusassoc ). rewrite <- ( hzdivequationmod p x ( hzremaindermod p x a + hzremaindermod p x c ) ). rewrite hzplusassoc. rewrite ( hzpluscomm ( hzremaindermod p x a ) ). rewrite <- ( hzplusassoc ( p * hzquotientmod p x c ) ). rewrite <- ( hzdivequationmod p x c ). rewrite ( hzpluscomm c ). rewrite <- hzplusassoc. rewrite <- ( hzdivequationmod p x a ). apply idpath. Defined. Lemma hzqrandplusineq ( p : hz ) ( x : hzneq 0 p ) ( a c : hz ) : dirprod ( hzleh 0 ( hzremaindermod p x ( hzremaindermod p x a + hzremaindermod p x c ) ) ) ( hzlth ( hzremaindermod p x ( hzremaindermod p x a + hzremaindermod p x c ) ) ( nattohz ( hzabsval p ) ) ). Proof. intros. split. apply hzleh0remaindermod. apply hzlthremaindermodmod. Defined. Lemma hzremaindermodandplus ( p : hz ) ( x : hzneq 0 p ) ( a c : hz ) : hzremaindermod p x ( a + c ) ~> hzremaindermod p x ( hzremaindermod p x a + hzremaindermod p x c ). Proof. intros. apply pathsinv0. apply ( hzqrtest p x ( a + c ) _ _ ( dirprodpair ( hzqrandpluseq p x a c ) ( hzqrandplusineq p x a c ) ) ). Defined. Lemma hzquotientmodandplus ( p : hz ) ( x : hzneq 0 p ) ( a c : hz ) : hzquotientmod p x ( a + c ) ~> ( hzquotientmod p x a + hzquotientmod p x c + hzquotientmod p x ( hzremaindermod p x a + hzremaindermod p x c ) ). Proof. intros. apply pathsinv0. apply ( hzqrtest p x ( a + c ) _ _ ( dirprodpair ( hzqrandpluseq p x a c ) ( hzqrandplusineq p x a c ) ) ). Defined. Lemma hzqrandtimeseq ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : ( a * b ) ~> ( ( m * ( ( hzquotientmod m x ) a * ( hzquotientmod m x ) b * m + (hzremaindermod m x b ) * ( hzquotientmod m x a ) + ( hzremaindermod m x a ) * ( hzquotientmod m x b ) + ( hzquotientmod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ) ) + hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ). Proof. intros. rewrite 3! ( hzldistr ). rewrite ( hzplusassoc _ _ ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ). rewrite <- hzdivequationmod. rewrite ( hzmultassoc _ _ m ). rewrite <- ( hzmultassoc m _ ( hzquotientmod m x b * m ) ). rewrite ( hzmultcomm _ m ). change ( ((m * hzquotientmod m x a * (m * hzquotientmod m x b))%hz + m * (hzremaindermod m x b * hzquotientmod m x a)%hz)%rng ) with ((m * hzquotientmod m x a * (m * hzquotientmod m x b)) + m * (hzremaindermod m x b * hzquotientmod m x a) )%hz. change ( a * b ~> (((m * hzquotientmod m x a * (m * hzquotientmod m x b) + m * (hzremaindermod m x b * hzquotientmod m x a))%hz + m * (hzremaindermod m x a * hzquotientmod m x b)%hz)%rng + hzremaindermod m x a * hzremaindermod m x b) ) with ( a * b ~> (((m * hzquotientmod m x a * (m * hzquotientmod m x b) + m * (hzremaindermod m x b * hzquotientmod m x a)) + m * (hzremaindermod m x a * hzquotientmod m x b))%hz + hzremaindermod m x a * hzremaindermod m x b) ). rewrite ( hzplusassoc ( m * hzquotientmod m x a * ( m * hzquotientmod m x b ) ) _ _ ). rewrite ( hzpluscomm ( m * ( hzremaindermod m x b * hzquotientmod m x a ) ) ( m * ( hzremaindermod m x a * hzquotientmod m x b ) ) ). rewrite <- ( hzmultassoc m ( hzremaindermod m x a ) ( hzquotientmod m x b ) ). rewrite ( hzmultcomm m ( hzremaindermod m x a ) ). rewrite ( hzmultassoc ( hzremaindermod m x a ) m ( hzquotientmod m x b ) ). rewrite <- ( hzplusassoc ( m * hzquotientmod m x a * ( m * hzquotientmod m x b ) ) ( hzremaindermod m x a * ( m * hzquotientmod m x b ) ) _ ). rewrite <- ( hzrdistr). rewrite <- hzdivequationmod. rewrite hzplusassoc. rewrite ( hzmultcomm ( hzremaindermod m x b ) ( hzquotientmod m x a ) ). rewrite <- ( hzmultassoc m ( hzquotientmod m x a ) ( hzremaindermod m x b ) ). rewrite <- ( hzrdistr ). rewrite <- hzdivequationmod. rewrite <- hzldistr. rewrite <- hzdivequationmod. apply idpath. Defined. Lemma hzqrandtimesineq ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : dirprod ( hzleh 0 ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ) ( hzlth ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ( nattohz ( hzabsval m ) ) ). Proof. intros. split. apply hzleh0remaindermod. apply hzlthremaindermodmod. Defined. Lemma hzquotientmodandtimes ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : hzquotientmod m x ( a * b ) ~> ( ( hzquotientmod m x ) a * ( hzquotientmod m x ) b * m + (hzremaindermod m x b ) * ( hzquotientmod m x a ) + ( hzremaindermod m x a ) * ( hzquotientmod m x b ) + ( hzquotientmod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ). Proof. intros. apply pathsinv0. apply ( hzqrtestq m x ( a * b ) _ ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ). split. apply hzqrandtimeseq. apply hzqrandtimesineq. Defined. Lemma hzremaindermodandtimes ( m : hz ) ( x : hzneq 0 m ) ( a b : hz ) : hzremaindermod m x ( a * b ) ~> ( hzremaindermod m x ( hzremaindermod m x a * hzremaindermod m x b ) ). Proof. intros. apply pathsinv0. apply ( hzqrtestr m x ( a * b ) ( ( hzquotientmod m x ) a * ( hzquotientmod m x ) b * m + (hzremaindermod m x b ) * ( hzquotientmod m x a ) + ( hzremaindermod m x a ) * ( hzquotientmod m x b ) + ( hzquotientmod m x ( hzremaindermod m x a * hzremaindermod m x b ) ) ) _ ). split. apply hzqrandtimeseq. apply hzqrandtimesineq. Defined. Lemma hzqrandremaindereq ( m : hz ) ( is : hzneq 0 m ) ( n : hz ) : ( hzremaindermod m is n ~> ( ( m * ( pr1 ( dirprodpair 0 ( hzremaindermod m is n ) ) ) + ( pr2 ( dirprodpair (@rngunel1 hz ) ( hzremaindermod m is n ) ) ) ) ) ). Proof. intros. simpl. rewrite hzmultx0. rewrite hzplusl0. apply idpath. Defined. Lemma hzqrandremainderineq ( m : hz ) ( is : hzneq 0 m ) ( n : hz ) : dirprod ( hzleh ( @rngunel1 hz ) ( hzremaindermod m is n ) ) ( hzlth ( hzremaindermod m is n ) ( nattohz ( hzabsval m ) ) ). Proof. intros. split. apply hzleh0remaindermod. apply hzlthremaindermodmod. Defined. Lemma hzremaindermoditerated ( m : hz ) ( is : hzneq 0 m ) ( n : hz ) : hzremaindermod m is ( hzremaindermod m is n ) ~> ( hzremaindermod m is n ). Proof. intros. apply pathsinv0. apply ( hzqrtestr m is ( hzremaindermod m is n ) 0 ( hzremaindermod m is n ) ). split. apply hzqrandremaindereq. apply hzqrandremainderineq. Defined. Lemma hzqrandremainderq ( m : hz ) ( is : hzneq 0 m ) ( n : hz ) : 0 ~> hzquotientmod m is ( hzremaindermod m is n ). Proof. intros. apply ( hzqrtestq m is ( hzremaindermod m is n ) 0 ( hzremaindermod m is n ) ). split. apply hzqrandremaindereq. apply hzqrandremainderineq. Defined. (** * III. THE EUCLIDEAN ALGORITHM *) Definition iscommonhzdiv ( k n m : hz ) := dirprod ( hzdiv k n ) ( hzdiv k m ). Lemma isapropiscommonhzdiv ( k n m : hz ) : isaprop ( iscommonhzdiv k n m ). Proof. intros. unfold isaprop. apply isofhleveldirprod. apply hzdiv. apply hzdiv. Defined. Definition hzgcd ( n m : hz ) : UU := total2 ( fun k : hz => dirprod ( iscommonhzdiv k n m ) ( forall l : hz, iscommonhzdiv l n m -> hzleh l k ) ). Lemma isaprophzgcd0 ( k n m : hz ) : isaprop ( dirprod ( iscommonhzdiv k n m ) ( forall l : hz, iscommonhzdiv l n m -> hzleh l k ) ). Proof. intros. apply isofhleveldirprod. apply isapropiscommonhzdiv. apply impred. intro t. apply impredfun. apply hzleh. Defined. Lemma isaprophzgcd ( n m : hz ) : isaprop ( hzgcd n m ). Proof. intros. intros k l. assert ( isofhlevel 2 ( hzgcd n m ) ) as aux. apply isofhleveltotal2. apply isasethz. intros x. apply hlevelntosn. apply isofhleveldirprod. apply isapropiscommonhzdiv. apply impred. intro t. apply impredfun. apply ( hzleh t x ). assert ( k ~> l ) as f. destruct k as [ k pq ]. destruct pq as [ p q ]. destruct l as [ l pq ]. destruct pq as [ p' q' ]. assert ( k ~> l ) as f0. apply isantisymmhzleh. apply q'. assumption. apply q. assumption. apply pathintotalfiber with ( p0 := f0 ). assert ( isaprop ( dirprod ( iscommonhzdiv l n m ) ( forall x : hz, iscommonhzdiv x n m -> hzleh x l ) ) ) as is. apply isofhleveldirprod. apply isapropiscommonhzdiv. apply impred. intro t. apply impredfun. apply ( hzleh t l ). apply is. split with f. intro g. destruct k as [ k pq ]. destruct pq as [ p q ]. destruct l as [ l pq ]. destruct pq as [ p' q' ]. apply aux. Defined. (* Euclidean algorithm for calculating the GCD of two numbers (here assumed to be natural numbers ( m <= n )): gcd ( n , m ) := 1. if m = 0, then take n. 2. if m \neq 0, then divide n = q * m + r and take g := gcd ( m , r ). *) Lemma hzdivandmultl ( a c d : hz ) ( p : hzdiv d a ) : hzdiv d ( c * a ). Proof. intros. intros P s. apply p. intro k. destruct k as [ k f ]. apply s. unfold hzdiv0. split with ( c * k ). rewrite ( hzmultcomm d ). rewrite ( hzmultassoc ). unfold hzdiv0 in f. rewrite ( hzmultcomm k ). rewrite f. apply idpath. Defined. Lemma hzdivandmultr ( a c d : hz ) ( p : hzdiv d a ) : hzdiv d ( a * c ). Proof. intros. rewrite hzmultcomm. apply hzdivandmultl. assumption. Defined. Lemma hzdivandminus ( a d : hz ) ( p : hzdiv d a ) : hzdiv d ( - a ). Proof. intros. intros P s. apply p. intro k. destruct k as [ k f ]. apply s. split with ( - k ). unfold hzdiv0. unfold hzdiv0 in f. rewrite ( rngrmultminus hz ). apply maponpaths. assumption. Defined. Definition natgcd ( m n : nat ) : ( natneq 0%nat n ) -> ( natleh m n ) -> ( hzgcd ( nattohz n ) ( nattohz m ) ). Proof. set ( E := ( fun m : nat => forall n : nat, ( natneq 0%nat n ) -> ( natleh m n ) -> ( hzgcd ( nattohz n ) ( nattohz m ) ) ) ). assert ( forall x : nat, E x ) as goal. apply stronginduction. (* BASE CASE: *) intros n x0 x1. split with ( nattohz n ). split. unfold iscommonhzdiv. split. unfold hzdiv. intros P s. apply s. unfold hzdiv0. split with 1. rewrite hzmultr1. apply idpath. unfold hzdiv. intros P s. apply s. unfold hzdiv0. split with 0. rewrite hzmultx0. rewrite nattohzand0. apply idpath. intros l t. destruct t as [ t0 t1 ]. destruct ( hzgthorleh l 0 ) as [ left | right ]. rewrite <- hzabsvalgth0. apply nattohzandleh. unfold hzdiv in t0. apply t0. intro t2. destruct t2 as [ k t2 ]. unfold hzdiv0 in t2. assert ( coprod ( natleh ( hzabsval l ) n ) ( n ~> 0%nat ) ) as C. apply ( natdivleh ( hzabsval l ) ( n ) ( hzabsval k ) ). apply ( isinclisinj isinclnattohz ). rewrite nattohzandmult. rewrite 2! hzabsvalgeh0. assumption. assert ( hzgeh ( l * k ) ( l * 0 ) ) as i. rewrite hzmultx0. rewrite t2. change 0 with ( nattohz 0%nat ). apply nattohzandgeh. apply x1. apply ( hzgehandmultlinv _ _ l ). assumption. assumption. apply hzgthtogeh. assumption. destruct C as [ C0 | C1 ]. assumption. assert empty. apply x0. apply pathsinv0. assumption. contradiction. assumption. apply ( istranshzleh _ 0 _ ). assumption. change 0 with ( nattohz 0%nat ). apply nattohzandleh. assumption. (* INDUCTION CASE: *) intros m p q. intros n i j. assert ( hzlth 0 ( nattohz m ) ) as p'. change 0 with ( nattohz 0%nat ). apply nattohzandlth. apply natneq0togth0. apply p. set ( a := divalgorithmnonneg n m p' ). destruct a as [ qr a ]. destruct qr as [ quot rem ]. destruct a as [ f a ]. destruct a as [ a b ]. simpl in b. simpl in f. assert ( natlth ( hzabsval rem ) m ) as p''. rewrite <- ( hzabsvalandnattohz m ). apply nattohzandlthinv. rewrite 2! hzabsvalgeh0. assumption. apply hzgthtogeh. apply ( hzgthgehtrans _ rem ). assumption. assumption. assumption. assert ( natleh ( hzabsval rem ) n ) as i''. apply natlthtoleh. apply nattohzandlthinv. rewrite hzabsvalgeh0. apply ( hzlthlehtrans _ ( nattohz m ) _ ). assumption. apply nattohzandleh. assumption. assumption. assert ( natneq 0%nat m ) as p'''. intro ff. apply p. apply pathsinv0. assumption. destruct ( q ( hzabsval rem ) p'' m p''' ( natlthtoleh _ _ p'' ) ) as [ rr c ]. destruct c as [ c0 c1 ]. split with rr. split. split. apply ( hzdivlinearcombright ( nattohz n ) ( nattohz m * quot ) ( rem ) rr f ). apply hzdivandmultr. exact ( pr1 c0 ). rewrite hzabsvalgeh0 in c0. exact ( pr2 c0 ). assumption. exact ( pr1 c0 ). intros l o. apply c1. split. exact ( pr2 o ). rewrite hzabsvalgeh0. apply ( hzdivlinearcombleft ( nattohz n ) ( nattohz m * quot ) ( rem ) l f ). exact ( pr1 o ). apply hzdivandmultr. exact ( pr2 o ). assumption. assumption. Defined. Lemma hzgcdandminusl ( m n : hz ) : hzgcd m n ~> hzgcd ( - m ) n. Proof. intros. assert ( hProppair ( hzgcd m n ) ( isaprophzgcd _ _ ) ~> ( hProppair ( hzgcd ( - m ) n ) ( isaprophzgcd _ _ ) ) ) as x. apply uahp. intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. split. apply j0. intro k. destruct k as [ k f ]. unfold hzdiv0 in f. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite ( rngrmultminus hz ). apply maponpaths. assumption. assumption. intros l f. apply i1. split. apply ( pr1 f ). intro k. destruct k as [ k g ]. unfold hzdiv0 in g. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite ( rngrmultminus hz ). rewrite <- ( rngminusminus hz m). apply maponpaths. assumption. exact ( pr2 f ). intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. split. apply j0. intro k. destruct k as [ k f ]. unfold hzdiv0 in f. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite ( rngrmultminus hz ). rewrite <- ( rngminusminus hz m ). apply maponpaths. assumption. assumption. intros l f. apply i1. split. apply ( pr1 f ). intro k. destruct k as [ k g ]. unfold hzdiv0 in g. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite (rngrmultminus hz ). apply maponpaths. assumption. exact ( pr2 f ). apply ( pathintotalpr1 x ). Defined. Lemma hzgcdsymm ( m n : hz ) : hzgcd m n ~> hzgcd n m. Proof. intros. assert ( hProppair ( hzgcd m n ) ( isaprophzgcd _ _ ) ~> ( hProppair ( hzgcd n m ) ( isaprophzgcd _ _ ) ) ) as x. apply uahp. intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. split. assumption. assumption. intros l o. apply i1. split. exact ( pr2 o ). exact ( pr1 o ). intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. split. assumption. assumption. intros l o. apply i1. split. exact ( pr2 o ). exact ( pr1 o ). apply ( pathintotalpr1 x ). Defined. Lemma hzgcdandminusr ( m n : hz ) : hzgcd m n ~> hzgcd m ( - n ). Proof. intros. rewrite 2! ( hzgcdsymm m ). rewrite hzgcdandminusl. apply idpath. Defined. Definition euclidean ( n m : hz ) ( i : hzneq 0 n ) ( p : natleh ( hzabsval m ) ( hzabsval n ) ) : hzgcd n m. Proof. intros. assert ( natneq 0%nat ( hzabsval n ) ) as j. intro x. apply i. assert ( hzabsval n ~> 0%nat ) as f. apply pathsinv0. assumption. rewrite ( hzabsvaleq0 f ). apply idpath. set ( a := natgcd ( hzabsval m ) ( hzabsval n ) j p ). destruct ( hzlthorgeh 0 n ) as [ left_n | right_n ]. destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. rewrite 2! ( hzabsvalgth0 ) in a. assumption. assumption. assumption. rewrite hzabsvalgth0 in a. rewrite hzabsvalleh0 in a. rewrite hzgcdandminusr. assumption. assumption. assumption. destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. rewrite ( hzabsvalgth0 left_m ) in a. rewrite hzabsvalleh0 in a. rewrite hzgcdandminusl. assumption. assumption. rewrite 2! hzabsvalleh0 in a. rewrite hzgcdandminusl. rewrite hzgcdandminusr. assumption. assumption. assumption. Defined. Theorem euclideanalgorithm ( n m : hz ) ( i : hzneq 0 n ) : iscontr ( hzgcd n m ). Proof. intros. destruct ( natgthorleh ( hzabsval m ) ( hzabsval n ) ) as [ left | right ]. assert ( hzneq 0 m ) as i'. intro f. apply ( negnatlthn0 ( hzabsval n ) ). rewrite <- f in left. rewrite hzabsval0 in left. assumption. set ( a := ( euclidean m n i' ( natlthtoleh _ _ left ) ) ). rewrite hzgcdsymm in a. split with a. intro. apply isaprophzgcd. split with ( euclidean n m i right ). intro. apply isaprophzgcd. Defined. Definition gcd ( n m : hz ) ( i : hzneq 0 n ) : hz := pr1 ( pr1 ( euclideanalgorithm n m i ) ). Definition gcdiscommondiv ( n m : hz ) ( i : hzneq 0 n ) := pr1 ( pr2 ( pr1 ( euclideanalgorithm n m i ) ) ). Definition gcdisgreatest ( n m : hz ) ( i : hzneq 0 n ) := pr2 ( pr2 ( pr1 ( euclideanalgorithm n m i ) ) ). Lemma hzdivand0 ( n : hz ) : hzdiv n 0. Proof. intros. intros P s. apply s. split with 0. unfold hzdiv0. apply hzmultx0. Defined. Lemma nozerodiv ( n : hz ) ( i : hzneq 0 n ) : neg ( hzdiv 0 n ). Proof. intros. intro p. apply i. apply ( p ( hProppair ( 0 ~> n ) ( isasethz 0 n ) ) ). intro t. destruct t as [ k f ]. unfold hzdiv0 in f. rewrite ( hzmult0x ) in f. assumption. Defined. (** * IV. Bezout's lemma and the commutative ring Z/pZ *) Lemma commonhzdivsignswap ( k n m : hz ) ( p : iscommonhzdiv k n m ) : iscommonhzdiv ( - k ) n m . Proof. intros. destruct p as [ p0 p1 ]. split. apply p0. intro t. intros P s. apply s. destruct t as [ l f ]. unfold hzdiv0 in f. split with ( - l ). unfold hzdiv0. change ( k * l ) with ( k * l )%rng in f. rewrite <- rngmultminusminus in f. assumption. apply p1. intro t. destruct t as [ l f ]. unfold hzdiv0 in f. intros P s. apply s. split with ( - l ). unfold hzdiv0. change ( k * l ) with ( k * l )%rng in f. rewrite <- rngmultminusminus in f. assumption. Defined. Lemma gcdneq0 ( n m : hz ) ( i : hzneq 0 n ) : hzneq 0 ( gcd n m i ). Proof. intros. intro f. apply ( nozerodiv n ). assumption. rewrite f. exact ( pr1 ( gcdiscommondiv n m i ) ). Defined. Lemma gcdpositive ( n m : hz ) ( i : hzneq 0 n ) : hzlth 0 ( gcd n m i ). Proof. intros. destruct ( hzneqchoice 0 ( gcd n m i ) ( gcdneq0 n m i ) ) as [ left | right ]. assert empty. assert ( hzleh ( - ( gcd n m i ) ) ( gcd n m i ) ) as i0. apply ( gcdisgreatest n m i ). apply commonhzdivsignswap. exact ( gcdiscommondiv n m i ). apply ( isirreflhzlth 0 ). apply ( istranshzlth _ ( - ( gcd n m i ) ) _ ). apply hzlth0andminus. assumption. apply ( hzlehlthtrans _ ( gcd n m i ) _ ). assumption. assumption. contradiction. assumption. Defined. Lemma gcdanddiv ( n m : hz ) ( i : hzneq 0 n ) ( p : hzdiv n m ) : coprod ( gcd n m i ~> n ) ( gcd n m i ~> - n ). Proof. intros. destruct ( hzneqchoice 0 n i ) as [ left | right ]. apply ii2. apply isantisymmhzleh. apply ( hzdivhzabsval ( gcd n m i ) n ( pr1 ( gcdiscommondiv n m i ) ) ). intro c'. destruct c' as [ c0 | c1 ]. rewrite <- ( hzabsvalgeh0 ). rewrite <- ( hzabsvallth0 ). apply nattohzandleh. assumption. assumption. apply hzgthtogeh. apply ( gcdpositive n m i). assert empty. assert ( n ~> 0 ) as f. rewrite hzabsvaleq0. apply idpath. assumption. apply i. apply pathsinv0. assumption. contradiction. apply ( pr2 ( pr2 ( pr1 ( euclideanalgorithm n m i ) ) ) ). apply commonhzdivsignswap. split. apply hzdivisrefl. assumption. apply ii1. apply isantisymmhzleh. apply ( hzdivhzabsval ( gcd n m i ) n ( pr1 ( gcdiscommondiv n m i ) ) ). intro c'. destruct c' as [ c0 | c1 ]. rewrite <- hzabsvalgth0. assert ( n ~> nattohz ( hzabsval n ) ) as f. apply pathsinv0. apply hzabsvalgth0. assumption. assert ( hzleh ( nattohz ( hzabsval ( gcd n m i ) ) ) ( nattohz ( hzabsval n ) ) ) as j. apply nattohzandleh. assumption. exact ( transportf ( fun x : _ => hzleh ( nattohz ( hzabsval ( gcd n m i ) ) ) x ) ( pathsinv0 f ) j ). apply gcdpositive. assert empty. apply i. apply pathsinv0. rewrite hzabsvaleq0. apply idpath. assumption. contradiction. apply ( gcdisgreatest n m i ). split. apply hzdivisrefl. assumption. Defined. Lemma gcdand0 ( n : hz ) ( i : hzneq 0 n ) : coprod ( gcd n 0 i ~> n ) ( gcd n 0 i ~> - n ). Proof. intros. apply gcdanddiv. apply hzdivand0. Defined. Lemma natbezoutstrong ( m n : nat ) ( i : hzneq 0 ( nattohz n ) ) : total2 ( fun ab : dirprod hz hz => ( gcd ( nattohz n ) ( nattohz m ) i ~> ( ( pr1 ab ) * ( nattohz n ) + ( pr2 ab ) * ( nattohz m ) ) ) ). Proof. set ( E := ( fun m : nat => forall n : nat, forall i : hzneq 0 ( nattohz n ), total2 ( fun ab : dirprod hz hz => gcd ( nattohz n ) ( nattohz m ) i ~> ( ( pr1 ab ) * ( nattohz n ) + ( pr2 ab ) * ( nattohz m ) ) ) ) ). assert ( forall x : nat, E x ) as goal. apply stronginduction. (* Base Case: *) unfold E. intros. split with ( dirprodpair 1 0 ). simpl. rewrite nattohzand0. destruct ( gcdand0 ( nattohz n ) i ) as [ left | right ]. rewrite hzmultl1. rewrite hzplusr0. assumption. assert empty. apply ( isirreflhzlth ( gcd ( nattohz n ) 0 i ) ). apply ( istranshzlth _ 0 _ ). rewrite right. apply hzgth0andminus. change 0 with ( nattohz 0%nat ). apply nattohzandgth. apply natneq0togth0. intro f. apply i. rewrite f. apply idpath. apply gcdpositive. contradiction. (* Induction Case: *) intros m x y. intros n i. assert ( hzneq 0 ( nattohz m ) ) as p. intro f. apply x. apply pathsinv0. rewrite <- hzabsvalandnattohz. change 0%nat with ( hzabsval ( nattohz 0%nat ) ). apply maponpaths. assumption. set ( r := hzremaindermod ( nattohz m ) p ( nattohz n ) ). set ( q := hzquotientmod ( nattohz m ) p ( nattohz n ) ). assert ( natlth (hzabsval r ) m ) as p'. rewrite <- ( hzabsvalandnattohz m ). apply hzabsvalandlth. exact ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ). unfold r. unfold hzremaindermod. rewrite <- ( hzabsvalgeh0 ( pr1 ( pr2 ( pr2 ( divalgorithmexists ( nattohz n ) ( nattohz m ) p ) ) ) ) ). apply nattohzandlth. assert ( natlth ( hzabsval (pr2 (pr1 (divalgorithmexists (nattohz n) (nattohz m) p))) ) ( ( hzabsval ( nattohz m ) ) ) ) as ii. apply hzabsvalandlth. exact ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ). assert ( nattohz ( hzabsval ( nattohz m ) ) ~> ( nattohz m ) ) as f. apply maponpaths. apply hzabsvalandnattohz. exact ( transportf ( fun x : _ => hzlth (pr2 (pr1 (divalgorithmexists (nattohz n) (nattohz m) p))) x ) f ( pr2 ( pr2 ( pr2 ( divalgorithmexists ( nattohz n ) ( nattohz m ) p ) ) ) ) ). exact ( transportf ( fun x : _ => natlth ( hzabsval (pr2 (pr1 (divalgorithmexists (nattohz n) (nattohz m) p))) ) x ) ( hzabsvalandnattohz m ) ii ). set ( c := y ( hzabsval r ) p' m p ). destruct c as [ ab f ]. destruct ab as [ a b ]. simpl in f. (* split with ( dirprodpair ( ( nattohz n ) - q * ( nattohz m ) ) ( a - b * q ) ).*) split with ( dirprodpair b ( a - b * q ) ). assert ( gcd ( nattohz m ) ( nattohz ( hzabsval r ) ) p ~> ( gcd ( nattohz n ) ( nattohz m ) i ) ) as g. apply isantisymmhzleh. apply ( gcdisgreatest ( nattohz n ) ( nattohz m ) i ). split. apply ( hzdivlinearcombright ( nattohz n ) ( ( nattohz m ) * ( hzquotientmod ( nattohz m ) p ( nattohz n ) ) ) r ). exact ( hzdivequationmod ( nattohz m ) p ( nattohz n ) ). apply hzdivandmultr. apply gcdiscommondiv. unfold r. rewrite ( hzabsvalgeh0 ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ) ) . apply ( pr2 ( gcdiscommondiv ( nattohz m ) ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) p ) ). apply gcdiscommondiv. apply gcdisgreatest. split. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). apply ( hzdivlinearcombleft ( nattohz n ) ( ( nattohz m ) * ( hzquotientmod ( nattohz m ) p ( nattohz n ) ) ) ( nattohz ( hzabsval r ) ) ). unfold r. rewrite ( hzabsvalgeh0 ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ) ). exact ( hzdivequationmod ( nattohz m ) p ( nattohz n ) ). apply gcdiscommondiv. apply ( hzdivandmultr ). apply ( pr2 ( gcdiscommondiv _ _ _ ) ). rewrite <- g. rewrite f. simpl. assert ( nattohz ( hzabsval r ) ~> ( ( nattohz n ) - ( q * nattohz m ) ) ) as h. rewrite ( hzdivequationmod ( nattohz m ) p ( nattohz n ) ). change ( hzquotientmod ( nattohz m ) p ( nattohz n ) ) with q. change ( hzremaindermod ( nattohz m ) p ( nattohz n ) ) with r. rewrite hzpluscomm. change (r + nattohz m * q - q * nattohz m) with ( ( r + nattohz m * q ) + ( - ( q * nattohz m ) ) ). rewrite hzmultcomm. rewrite hzplusassoc. change (q * nattohz m + - (q * nattohz m)) with ( (q * nattohz m - (q * nattohz m))). rewrite hzrminus. rewrite hzplusr0. apply hzabsvalgeh0. apply ( hzleh0remaindermod ( nattohz m ) p ( nattohz n ) ). rewrite h. change ( (nattohz n - q * nattohz m) ) with ( (nattohz n + ( - ( q * nattohz m) ) ) ) at 1. rewrite ( rngldistr hz ). rewrite <- ( hzplusassoc ). rewrite ( hzpluscomm ( a * nattohz m ) ). rewrite rngrmultminus. rewrite <- hzmultassoc. rewrite <- rnglmultminus. rewrite hzplusassoc. rewrite <- ( rngrdistr hz ). change (b * nattohz n + (a - b * q) * nattohz m) with ((b * nattohz n)%rng + ((a + - (b * q)%hz) * nattohz m)%rng). apply idpath. apply goal. Defined. Lemma divandhzabsval ( n : hz ) : hzdiv n ( nattohz ( hzabsval n ) ). Proof. intros. destruct ( hzlthorgeh 0 n ) as [ left | right ]. intros P s. apply s. split with 1. unfold hzdiv0. rewrite hzmultr1. rewrite hzabsvalgth0. apply idpath. assumption. intros P s. apply s. split with ( - 1%hz ). unfold hzdiv0. rewrite ( rngrmultminus hz ). rewrite hzmultr1. rewrite hzabsvalleh0. apply idpath. assumption. Defined. Lemma bezoutstrong ( m n : hz ) ( i : hzneq 0 n ) : total2 ( fun ab : dirprod hz hz => ( gcd n m i ~> ( ( pr1 ab ) * n + ( pr2 ab ) * m ) ) ). Proof. intros. assert ( hzneq 0 ( nattohz ( hzabsval n ) ) ) as i'. intro f. apply i. destruct ( hzneqchoice 0 n i ) as [ left | right ]. rewrite hzabsvallth0 in f. rewrite <- ( rngminusminus hz ). change 0 with ( - - 0 ). apply maponpaths. assumption. assumption. rewrite hzabsvalgth0 in f. assumption. assumption. set ( c := (natbezoutstrong (hzabsval m) (hzabsval n) i')). destruct c as [ ab f ]. destruct ab as [ a b ]. simpl in f. assert ( gcd n m i ~> gcd ( nattohz ( hzabsval n ) ) ( nattohz ( hzabsval m ) ) i' ) as g. destruct ( hzneqchoice 0 n i ) as [ left_n | right_n ]. apply isantisymmhzleh. apply gcdisgreatest. split. rewrite hzabsvallth0. apply hzdivandminus. apply gcdiscommondiv. assumption. destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. rewrite hzabsvalgth0. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). assumption. rewrite hzabsvalleh0. apply hzdivandminus. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). assumption. apply gcdisgreatest. split. apply ( hzdivistrans _ ( nattohz ( hzabsval n ) ) _ ). apply gcdiscommondiv. rewrite hzabsvallth0. rewrite <- ( rngminusminus hz n ). apply hzdivandminus. rewrite ( rngminusminus hz n ). apply hzdivisrefl. assumption. apply ( hzdivistrans _ ( nattohz ( hzabsval m ) ) _ ). apply ( pr2 ( gcdiscommondiv _ _ _ ) ). destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. rewrite hzabsvalgth0. apply hzdivisrefl. assumption. rewrite hzabsvalleh0. rewrite <- ( rngminusminus hz m ). apply hzdivandminus. rewrite ( rngminusminus hz m ). apply hzdivisrefl. assumption. apply isantisymmhzleh. apply gcdisgreatest. split. rewrite hzabsvalgth0. apply gcdiscommondiv. assumption. apply ( hzdivistrans _ ( nattohz ( hzabsval m ) ) _ ). destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. rewrite hzabsvalgth0. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). assumption. rewrite hzabsvalleh0. apply hzdivandminus. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). assumption. apply hzdivisrefl. apply gcdisgreatest. split. apply ( hzdivistrans _ ( nattohz ( hzabsval n ) ) _ ). apply gcdiscommondiv. rewrite hzabsvalgth0. apply hzdivisrefl. assumption. apply ( hzdivistrans _ ( nattohz ( hzabsval m ) ) _ ). apply ( pr2 ( gcdiscommondiv _ _ _ ) ). destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. rewrite hzabsvalgth0. apply hzdivisrefl. assumption. rewrite hzabsvalleh0. rewrite <- ( rngminusminus hz m ). apply hzdivandminus. rewrite ( rngminusminus hz m ). apply hzdivisrefl. assumption. destruct ( hzneqchoice 0 n i ) as [ left_n | right_n ]. destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. split with ( dirprodpair ( - a ) b ). simpl. assert ( - a * n + b * m ~> ( a * ( nattohz ( hzabsval n ) ) + b * ( nattohz ( hzabsval m ) ) ) ) as l. rewrite hzabsvallth0. rewrite hzabsvalgth0. rewrite ( rnglmultminus hz ). rewrite <- ( rngrmultminus hz ). apply idpath. assumption. assumption. rewrite l. rewrite g. exact f. split with ( dirprodpair ( - a ) ( - b ) ). simpl. rewrite 2! ( rnglmultminus hz ). rewrite <- 2! ( rngrmultminus hz ). rewrite <- ( hzabsvallth0 ). rewrite <- ( hzabsvalleh0 ). rewrite g. exact f. assumption. assumption. destruct ( hzlthorgeh 0 m ) as [ left_m | right_m ]. split with ( dirprodpair a b ). simpl. rewrite g. rewrite f. rewrite 2! hzabsvalgth0. apply idpath. assumption. assumption. split with ( dirprodpair a ( - b ) ). rewrite g. rewrite f. simpl. rewrite hzabsvalgth0. rewrite hzabsvalleh0. rewrite ( rngrmultminus hz ). rewrite <- ( rnglmultminus hz ). apply idpath. assumption. assumption. Defined. (** * V. Z/nZ *) Lemma hzmodisaprop ( p : hz ) ( x : hzneq 0 p ) ( n m : hz ) : isaprop ( hzremaindermod p x n ~> ( hzremaindermod p x m ) ). Proof. intros. apply isasethz. Defined. Definition hzmod ( p : hz ) ( x : hzneq 0 p ) : hz -> hz -> hProp. Proof. intros p x n m. exact ( hProppair ( hzremaindermod p x n ~> ( hzremaindermod p x m ) ) ( hzmodisaprop p x n m ) ). Defined. Lemma hzmodisrefl ( p : hz ) ( x : hzneq 0 p ) : isrefl ( hzmod p x ). Proof. intros. unfold isrefl. intro n. unfold hzmod. assert ( hzremaindermod p x n ~> ( hzremaindermod p x n ) ) as a. auto. apply a. Defined. Lemma hzmodissymm ( p : hz ) ( x : hzneq 0 p ) : issymm ( hzmod p x ). Proof. intros. unfold issymm. intros n m. unfold hzmod. intro v. assert ( hzremaindermod p x m ~> hzremaindermod p x n ) as a. exact ( pathsinv0 ( v ) ). apply a. Defined. Lemma hzmodistrans ( p : hz ) ( x : hzneq 0 p ) : istrans ( hzmod p x ). Proof. intros. unfold istrans. intros n m k. intros u v. unfold hzmod. unfold hzmod in u. unfold hzmod in v. assert ( hzremaindermod p x n ~> hzremaindermod p x k ) as a. exact ( pathscomp0 u v ). apply a. Defined. Lemma hzmodiseqrel ( p : hz ) ( x : hzneq 0 p ) : iseqrel ( hzmod p x ). Proof. intros. apply iseqrelconstr. exact ( hzmodistrans p x ). exact ( hzmodisrefl p x ). exact ( hzmodissymm p x ). Defined. Lemma hzmodcompatmultl ( p : hz ) ( x : hzneq 0 p ) : forall a b c : hz, hzmod p x a b -> hzmod p x ( c * a ) ( c * b ). Proof. intros p x a b c v. unfold hzmod. change (hzremaindermod p x (c * a) ~> hzremaindermod p x (c * b)). rewrite hzremaindermodandtimes. rewrite v. rewrite <- hzremaindermodandtimes. apply idpath. Defined. Lemma hzmodcompatmultr ( p : hz ) ( x : hzneq 0 p ) : forall a b c : hz, hzmod p x a b -> hzmod p x ( a * c ) ( b * c ). Proof. intros p x a b c v. rewrite hzmultcomm. rewrite ( hzmultcomm b ). apply hzmodcompatmultl. assumption. Defined. Lemma hzmodcompatplusl ( p : hz ) ( x : hzneq 0 p ) : forall a b c : hz, hzmod p x a b -> hzmod p x ( c + a ) ( c + b ). Proof. intros p x a b c v. unfold hzmod. change ( hzremaindermod p x ( c + a ) ~> hzremaindermod p x ( c + b ) ). rewrite hzremaindermodandplus. rewrite v. rewrite <- hzremaindermodandplus. apply idpath. Defined. Lemma hzmodcompatplusr ( p : hz ) ( x : hzneq 0 p ) : forall a b c : hz, hzmod p x a b -> hzmod p x ( a + c ) ( b + c ). Proof. intros p x a b c v. rewrite hzpluscomm. rewrite ( hzpluscomm b ). apply hzmodcompatplusl. assumption. Defined. Lemma hzmodisrngeqrel ( p : hz ) ( x : hzneq 0 p ) : rngeqrel ( X := hz ). Proof. intros. split with ( tpair ( hzmod p x ) ( hzmodiseqrel p x ) ). split. split. apply hzmodcompatplusl. apply hzmodcompatplusr. split. apply hzmodcompatmultl. apply hzmodcompatmultr. Defined. Definition hzmodp ( p : hz ) ( x : hzneq 0 p ) := commrngquot ( hzmodisrngeqrel p x ). Lemma isdeceqhzmodp ( p : hz ) ( x : hzneq 0 p ) : isdeceq ( hzmodp p x ). Proof. intros. apply ( isdeceqsetquot ( hzmodisrngeqrel p x ) ). intros a b. unfold isdecprop. destruct ( isdeceqhz ( hzremaindermod p x a ) ( hzremaindermod p x b ) ) as [ l | r ]. unfold hzmodisrngeqrel. simpl. split with ( ii1 l ). intros t. destruct t as [ f | g ]. apply maponpaths. apply isasethz. assert empty. apply g. assumption. contradiction. split with ( ii2 r ). intros t. destruct t as [ f | g ]. assert empty. apply r. assumption. contradiction. apply maponpaths. apply isapropneg. Defined. Definition acommrng_hzmod ( p : hz ) ( x : hzneq 0 p ) : acommrng. Proof. intros. split with ( hzmodp p x ). split with ( tpair _ ( deceqtoneqapart ( isdeceqhzmodp p x ) ) ). split. split. intros a b c q. simpl. simpl in q. intro f. apply q. rewrite f. apply idpath. intros a b c q. simpl in q. simpl. intro f. apply q. rewrite f. apply idpath. split. intros a b c q. simpl in q. simpl. intros f. apply q. rewrite f. apply idpath. intros a b c q. simpl. simpl in q. intro f. apply q. rewrite f. apply idpath. Defined. Lemma hzremaindermodanddiv ( p : hz ) ( x : hzneq 0 p ) ( a : hz ) ( y : hzdiv p a ) : hzremaindermod p x a ~> 0. Proof. intros. assert ( isaprop ( hzremaindermod p x a ~> 0 ) ) as v. apply isasethz. apply ( y ( hProppair _ v ) ). intro t. destruct t as [ k f ]. unfold hzdiv0 in f. assert ( a ~> ( p * k + 0 ) ) as f'. rewrite f. rewrite hzplusr0. apply idpath. set ( e := tpair ( P := (fun qr : dirprod hz hz => dirprod (a ~> (p * pr1 qr + pr2 qr)) (dirprod (hzleh 0 (pr2 qr)) (hzlth (pr2 qr) (nattohz (hzabsval p))))) ) ( dirprodpair k 0 ) ( dirprodpair f' ( dirprodpair ( isreflhzleh 0 ) ( hzabsvalneq0 p x ) ) ) ). assert ( e ~> ( pr1 ( divalgorithm a p x ) ) ) as s. apply ( pr2 ( divalgorithm a p x ) ). set ( w := pathintotalpr1 ( pathsinv0 s ) ). unfold e in w. unfold hzremaindermod. apply ( maponpaths ( fun z : dirprod hz hz => pr2 z ) w ). Defined. Lemma gcdandprime ( p : hz ) ( x : hzneq 0 p ) ( y : isaprime p ) ( a : hz ) ( q : neg ( hzmod p x a 0 ) ) : gcd p a x ~> 1. Proof. intros. assert ( isaprop ( gcd p a x ~> 1) ) as is. apply ( isasethz ). apply ( pr2 y ( gcd p a x ) ( pr1 ( gcdiscommondiv p a x ) ) ( hProppair _ is ) ). intro t. destruct t as [ t0 | t1 ]. apply t0. assert empty. apply q. simpl. assert ( hzremaindermod p x a ~> 0 ) as f. assert ( hzdiv p a ) as u. rewrite <- t1. apply ( pr2 ( gcdiscommondiv _ _ _ ) ). rewrite hzremaindermodanddiv. apply idpath. assumption. rewrite f. rewrite hzqrand0r. apply idpath. contradiction. Defined. Lemma hzremaindermodandmultl ( p : hz ) ( x : hzneq 0 p ) ( a b : hz ) : hzremaindermod p x ( p * a + b ) ~> hzremaindermod p x b. Proof. intros. assert ( p * a + b ~> ( p * ( a + hzquotientmod p x b ) + hzremaindermod p x b ) ) as f. rewrite hzldistr. rewrite hzplusassoc. rewrite <- ( hzdivequationmod p x b ). apply idpath. rewrite hzremaindermodandplus. rewrite hzremaindermodandtimes. rewrite hzqrandselfr. rewrite hzmult0x. rewrite hzqrand0r. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. Defined. Lemma hzmodprimeinv ( p : hz ) ( x : hzneq 0 p ) ( y : isaprime p ) ( a : hz ) ( q : neg ( hzmod p x a 0 ) ) : total2 ( fun v : hz => dirprod ( hzmod p x ( a * v ) 1 ) ( hzmod p x ( v * a ) 1 ) ). Proof. intros. split with ( pr2 ( pr1 ( bezoutstrong a p x ) ) ). assert ( 1 ~> (pr1 (pr1 (bezoutstrong a p x)) * p + pr2 (pr1 (bezoutstrong a p x)) * a) ) as f'. assert ( 1 ~> gcd p a x ) as f''. apply pathsinv0. apply ( gcdandprime ). assumption. assumption. rewrite f''. apply ( bezoutstrong a p x ). split. rewrite f'. simpl. rewrite ( hzmultcomm ( pr1 ( pr1 ( bezoutstrong a p x ) ) ) _ ). rewrite ( hzremaindermodandmultl ). rewrite hzmultcomm. apply idpath. rewrite f'. simpl. rewrite hzremaindermodandplus. rewrite ( hzremaindermodandtimes p x _ p ). rewrite hzqrandselfr. rewrite hzmultx0. rewrite hzqrand0r. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. Defined. Lemma quotientrngsumdecom ( X : commrng ) ( R : rngeqrel ( X := X ) ) ( a b : X ) : @op2 ( commrngquot R ) ( setquotpr R a ) ( setquotpr R b ) ~> ( setquotpr R ( a * b )%rng ). Proof. intros. auto. Defined. Definition ahzmod ( p : hz ) ( y : isaprime p ) : afld. Proof. intros. split with ( acommrng_hzmod p ( isaprimetoneq0 y ) ). split. simpl. intro f. apply ( isirreflhzlth 0 ). assert ( hzlth 0 1 ) as i. apply hzlthnsn. change ( 1%rng ) with ( setquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) 1%hz ) in f. change ( 0%rng ) with ( setquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) 0%hz ). assert ( (hzmodisrngeqrel p ( isaprimetoneq0 y )) 1%hz 0%hz ) as o. apply ( setquotprpathsandR ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) 1%hz 0%hz ). assumption. unfold hzmodisrngeqrel in o. simpl in o. assert ( hzremaindermod p ( isaprimetoneq0 y ) 0 ~> 0 ) as o'. rewrite hzqrand0r. apply idpath. rewrite o' in o. assert ( hzremaindermod p ( isaprimetoneq0 y ) 1 ~> 1 ) as o''. assert ( hzlth 1 p ) as v. apply y. rewrite hzqrand1r. apply idpath. rewrite o'' in o. assert ( hzlth 0 1 ) as o'''. apply hzlthnsn. rewrite o in o'''. assumption. assert ( forall x0 : acommrng_hzmod p ( isaprimetoneq0 y ), isaprop ( ( x0 # 0)%rng -> multinvpair ( acommrng_hzmod p ( isaprimetoneq0 y ) ) x0 ) ) as int. intro a. apply impred. intro q. apply isapropmultinvpair. apply ( setquotunivprop _ ( fun x0 => hProppair _ ( int x0 ) ) ). intro a. simpl. intro q. assert ( neg ( hzmod p ( isaprimetoneq0 y ) a 0 ) ) as q'. intro g. unfold hzmod in g. simpl in g. apply q. change ( 0%rng ) with ( setquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) 0%hz ). apply ( iscompsetquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) ). apply g. split with ( setquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) ( pr1 ( hzmodprimeinv p ( isaprimetoneq0 y ) y a q' ) ) ). split. simpl. rewrite ( quotientrngsumdecom hz ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) ). change 1%multmonoid with ( setquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) 1%hz ). apply ( iscompsetquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) ). simpl. change (pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))) * a)%rng with (pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))) * a)%hz. exact ( ( pr2 ( pr2 ( hzmodprimeinv p ( isaprimetoneq0 y ) y a q' ) ) )). simpl. rewrite ( quotientrngsumdecom hz ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) ). change 1%multmonoid with ( setquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) 1%hz ). apply ( iscompsetquotpr ( hzmodisrngeqrel p ( isaprimetoneq0 y ) ) ). change (a * pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))))%rng with (a * pr2 (pr1 (bezoutstrong a p ( isaprimetoneq0 y ))))%hz. exact ( ( pr1 ( pr2 ( hzmodprimeinv p ( isaprimetoneq0 y ) y a q' ) ) )). Defined. Close Scope hz_scope. (** END OF FILE *)