Library UniMath.NumberSystems.Integers
Generalities on the type of integers and integer arithmetic. Vladimir Voevodsky . Aug. - Sep. 2011.
Preamble
Unset Kernel Term Sharing.
Imports
Require Export UniMath.Foundations.NaturalNumbers.
Require Import UniMath.MoreFoundations.PartA.
Require Export UniMath.MoreFoundations.NegativePropositions.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.
Require Export UniMath.Algebra.RigsAndRings.
Require Export UniMath.NumberSystems.NaturalNumbersAlgebra.
Definition hz : commring := commrigtocommring natcommrig .
Definition hzaddabgr : abgr := hz .
Definition hzmultabmonoid : abmonoid := ringmultabmonoid hz .
Definition natnattohz : nat -> nat -> hz := λ n m, setquotpr _ ( make_dirprod n m ) .
Definition hzplus : hz -> hz -> hz := @op1 hz.
Definition hzsign : hz -> hz := grinv hzaddabgr .
Definition hzminus : hz -> hz -> hz := λ x y, hzplus x ( hzsign y ) .
Definition hzzero : hz := unel hzaddabgr .
Definition hzmult : hz -> hz -> hz := @op2 hz .
Definition hzone : hz := unel hzmultabmonoid .
Declare Scope hz_scope.
Bind Scope hz_scope with hz .
Notation " x + y " := ( hzplus x y ) : hz_scope .
Notation " 0 " := hzzero : hz_scope .
Notation " 1 " := hzone : hz_scope .
Notation " - x " := ( hzsign x ) : hz_scope .
Notation " x - y " := ( hzminus x y ) : hz_scope .
Notation " x * y " := ( hzmult x y ) : hz_scope .
Delimit Scope hz_scope with hz .
Properties of equlaity on hz
Theorem isdeceqhz : isdeceq hz .
Show proof.
. change ( isdeceq ( abgrdiff ( rigaddabmonoid natcommrig ) ) ) . apply isdeceqabgrdiff . apply isinclnatplusr . apply isdeceqnat .
.Opaque isdeceqhz.
Lemma isasethz : isaset hz .
Show proof.
.
Opaque isasethz.
Definition hzeq ( x y : hz ) : hProp := make_hProp ( x = y ) ( isasethz _ _ ) .
Definition isdecrelhzeq : isdecrel hzeq := λ a b, isdeceqhz a b .
Definition hzdeceq : decrel hz := make_decrel isdecrelhzeq .
Definition hzbooleq := decreltobrel hzdeceq .
Definition hzneq ( x y : hz ) : hProp := make_hProp ( neg ( x = y ) ) ( isapropneg _ ) .
Definition isdecrelhzneq : isdecrel hzneq := isdecnegrel _ isdecrelhzeq .
Definition hzdecneq : decrel hz := make_decrel isdecrelhzneq .
Definition hzboolneq := decreltobrel hzdecneq .
Local Open Scope hz_scope .
hz is a non-zero ring
Properties of addition and subtraction on hz
Definition hzminuszero : ( - 0 ) = 0 := ringinvunel1 hz .
Lemma hzplusr0 ( x : hz ) : ( x + 0 ) = x .
Show proof.
.
Lemma hzplusl0 ( x : hz ) : ( 0 + x ) = x .
Show proof.
.
Lemma hzplusassoc ( x y z : hz ) : ( ( x + y ) + z ) = ( x + ( y + z ) ) .
Show proof.
.
Lemma hzpluscomm ( x y : hz ) : ( x + y ) = ( y + x ) .
Show proof.
.
Lemma hzlminus ( x : hz ) : ( -x + x ) = 0 .
Show proof.
.
Lemma hzrminus ( x : hz ) : ( x - x ) = 0 .
Show proof.
.
Lemma isinclhzplusr ( n : hz ) : isincl ( λ m : hz, m + n ) .
Show proof.
Lemma isinclhzplusl ( n : hz ) : isincl ( λ m : hz, n + m ) .
Show proof.
.
Lemma hzpluslcan ( a b c : hz ) ( is : ( c + a ) = ( c + b ) ) : a = b .
Show proof.
.
Lemma hzplusrcan ( a b c : hz ) ( is : ( a + c ) = ( b + c ) ) : a = b .
Show proof.
.
Definition hzinvmaponpathsminus { a b : hz } ( e : ( - a ) = ( - b ) ) : a = b := grinvmaponpathsinv hzaddabgr e .
Lemma hzrplusminus (n m : hz) : n + m - m = n.
Show proof.
unfold hzminus, hzplus, hzplus. rewrite ringassoc1.
set (tmp := hzrminus m). unfold hzminus, hzplus in tmp. rewrite tmp. clear tmp.
apply hzplusr0.
Opaque hzrplusminus.set (tmp := hzrminus m). unfold hzminus, hzplus in tmp. rewrite tmp. clear tmp.
apply hzplusr0.
Lemma hzrplusminus' (n m : hz) : n = n + m - m.
Show proof.
Opaque hzrplusminus'.
Lemma hzrminusplus (n m : hz) : n - m + m = n.
Show proof.
Opaque hzrminusplus.
Lemma hzrminusplus' (n m : hz) : n = n - m + m.
Show proof.
Opaque hzrminusplus'.
Properties of multiplication on hz
Lemma hzmultr1 ( x : hz ) : ( x * 1 ) = x .
Show proof.
.
Lemma hzmultl1 ( x : hz ) : ( 1 * x ) = x .
Show proof.
.
Lemma hzmult0x ( x : hz ) : ( 0 * x ) = 0 .
Show proof.
.
Lemma hzmultx0 ( x : hz ) : ( x * 0 ) = 0 .
Show proof.
.
Lemma hzmultassoc ( x y z : hz ) : ( ( x * y ) * z ) = ( x * ( y * z ) ) .
Show proof.
.
Lemma hzmultcomm ( x y : hz ) : ( x * y ) = ( y * x ) .
Show proof.
.
Definition hzneq0andmultlinv ( n m : hz ) ( isnm : hzneq ( n * m ) 0 ) : hzneq n 0 := ringneq0andmultlinv hz n m isnm .
Definition hzneq0andmultrinv ( n m : hz ) ( isnm : hzneq ( n * m ) 0 ) : hzneq m 0 := ringneq0andmultrinv hz n m isnm .
Definition and properties of "greater", "less", "greater or equal" and "less or equal" on hz .
Definitions and notations
Definition hzgth : hrel hz := rigtoringrel natcommrig isplushrelnatgth .
Definition hzlth : hrel hz := λ a b, hzgth b a .
Definition hzleh : hrel hz := λ a b, make_hProp ( neg ( hzgth a b ) ) ( isapropneg _ ) .
Definition hzgeh : hrel hz := λ a b, make_hProp ( neg ( hzgth b a ) ) ( isapropneg _ ) .
Lemma isdecrelhzgth : isdecrel hzgth .
Show proof.
. apply ( isdecrigtoringrel natcommrig isplushrelnatgth ) . apply isinvplushrelnatgth . apply isdecrelnatgth .
.Definition hzgthdec := make_decrel isdecrelhzgth .
Definition isdecrelhzlth : isdecrel hzlth := λ x x', isdecrelhzgth x' x .
Definition hzlthdec := make_decrel isdecrelhzlth .
Definition isdecrelhzleh : isdecrel hzleh := isdecnegrel _ isdecrelhzgth .
Definition hzlehdec := make_decrel isdecrelhzleh .
Definition isdecrelhzgeh : isdecrel hzgeh := λ x x', isdecrelhzleh x' x .
Definition hzgehdec := make_decrel isdecrelhzgeh .
Lemma istranshzgth ( n m k : hz ) : hzgth n m -> hzgth m k -> hzgth n k .
Show proof.
apply ( istransabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold istrans . apply istransnatgth .
Lemma isirreflhzgth ( n : hz ) : neg ( hzgth n n ) .
Show proof.
apply ( isirreflabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold isirrefl . apply isirreflnatgth .
.Lemma hzgthtoneq ( n m : hz ) ( g : hzgth n m ) : neg ( n = m ) .
Show proof.
.
Lemma isasymmhzgth ( n m : hz ) : hzgth n m -> hzgth m n -> empty .
Show proof.
apply ( isasymmabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold isasymm . apply isasymmnatgth .
.Lemma isantisymmneghzgth ( n m : hz ) : neg ( hzgth n m ) -> neg ( hzgth m n ) -> n = m .
Show proof.
. apply ( isantisymmnegabgrdiffrel nataddabmonoid isplushrelnatgth ) . unfold isantisymmneg . apply isantisymmnegnatgth .
.Lemma isnegrelhzgth : isnegrel hzgth .
Show proof.
.
Lemma iscoantisymmhzgth ( n m : hz ) : neg ( hzgth n m ) -> ( hzgth m n ) ⨿ ( n = m ) .
Show proof.
. revert n m. apply isantisymmnegtoiscoantisymm . apply isdecrelhzgth . intros n m . apply isantisymmneghzgth .
.Lemma iscotranshzgth ( n m k : hz ) : hzgth n k -> hdisj ( hzgth n m ) ( hzgth m k ) .
Show proof.
. intros gxz . destruct ( isdecrelhzgth n m ) as [ gxy | ngxy ] . apply ( hinhpr ( ii1 gxy ) ) . apply hinhpr . apply ii2 . destruct ( isdecrelhzgth m n ) as [ gyx | ngyx ] . apply ( istranshzgth _ _ _ gyx gxz ) . set ( e := isantisymmneghzgth _ _ ngxy ngyx ) . rewrite e in gxz . apply gxz .
.Definition istranshzlth ( n m k : hz ) : hzlth n m -> hzlth m k -> hzlth n k := λ lnm lmk, istranshzgth _ _ _ lmk lnm .
Definition isirreflhzlth ( n : hz ) : neg ( hzlth n n ) := isirreflhzgth n .
Lemma hzlthtoneq ( n m : hz ) ( g : hzlth n m ) : neg ( n = m ) .
Show proof.
.
Definition isasymmhzlth ( n m : hz ) : hzlth n m -> hzlth m n -> empty := λ lnm lmn, isasymmhzgth _ _ lmn lnm .
Definition isantisymmneghztth ( n m : hz ) : neg ( hzlth n m ) -> neg ( hzlth m n ) -> n = m := λ nlnm nlmn, isantisymmneghzgth _ _ nlmn nlnm .
Definition isnegrelhzlth : isnegrel hzlth := λ n m, isnegrelhzgth m n .
Definition iscoantisymmhzlth ( n m : hz ) : neg ( hzlth n m ) -> ( hzlth m n ) ⨿ ( n = m ) .
Show proof.
. intros nlnm . destruct ( iscoantisymmhzgth m n nlnm ) as [ l | e ] . apply ( ii1 l ) . apply ( ii2 ( pathsinv0 e ) ) .
.Definition iscotranshzlth ( n m k : hz ) : hzlth n k -> hdisj ( hzlth n m ) ( hzlth m k ) .
Show proof.
.
Definition istranshzleh ( n m k : hz ) : hzleh n m -> hzleh m k -> hzleh n k .
Show proof.
Definition isreflhzleh ( n : hz ) : hzleh n n := isirreflhzgth n .
Definition isantisymmhzleh ( n m : hz ) : hzleh n m -> hzleh m n -> n = m := isantisymmneghzgth n m .
Definition isnegrelhzleh : isnegrel hzleh .
Show proof.
.
Definition iscoasymmhzleh ( n m : hz ) ( nl : neg ( hzleh n m ) ) : hzleh m n := negf ( isasymmhzgth _ _ ) nl .
Definition istotalhzleh : istotal hzleh .
Show proof.
. intros x y . destruct ( isdecrelhzleh x y ) as [ lxy | lyx ] . apply ( hinhpr ( ii1 lxy ) ) . apply hinhpr . apply ii2 . apply ( iscoasymmhzleh _ _ lyx ) .
.
hzgeh .
Definition istranshzgeh ( n m k : hz ) : hzgeh n m -> hzgeh m k -> hzgeh n k := λ gnm gmk, istranshzleh _ _ _ gmk gnm .
Definition isreflhzgeh ( n : hz ) : hzgeh n n := isreflhzleh _ .
Definition isantisymmhzgeh ( n m : hz ) : hzgeh n m -> hzgeh m n -> n = m := λ gnm gmn, isantisymmhzleh _ _ gmn gnm .
Definition isnegrelhzgeh : isnegrel hzgeh := λ n m, isnegrelhzleh m n .
Definition iscoasymmhzgeh ( n m : hz ) ( nl : neg ( hzgeh n m ) ) : hzgeh m n := iscoasymmhzleh _ _ nl .
Definition istotalhzgeh : istotal hzgeh := λ n m, istotalhzleh m n .
Definition hzgthtogeh ( n m : hz ) : hzgth n m -> hzgeh n m .
Show proof.
.
Definition hzlthtoleh ( n m : hz ) : hzlth n m -> hzleh n m := hzgthtogeh _ _ .
Definition hzlehtoneghzgth ( n m : hz ) : hzleh n m -> neg ( hzgth n m ) .
Show proof.
intros is is' . apply ( is is' ) .
.Definition hzgthtoneghzleh ( n m : hz ) : hzgth n m -> neg ( hzleh n m ) := λ g l , hzlehtoneghzgth _ _ l g .
Definition hzgehtoneghzlth ( n m : hz ) : hzgeh n m -> neg ( hzlth n m ) := λ gnm lnm, hzlehtoneghzgth _ _ gnm lnm .
Definition hzlthtoneghzgeh ( n m : hz ) : hzlth n m -> neg ( hzgeh n m ) := λ gnm lnm, hzlehtoneghzgth _ _ lnm gnm .
Definition neghzlehtogth ( n m : hz ) : neg ( hzleh n m ) -> hzgth n m := isnegrelhzgth n m .
Definition neghzgehtolth ( n m : hz ) : neg ( hzgeh n m ) -> hzlth n m := isnegrelhzlth n m .
Definition neghzgthtoleh ( n m : hz ) : neg ( hzgth n m ) -> hzleh n m .
Show proof.
.
Definition neghzlthtogeh ( n m : hz ) : neg ( hzlth n m ) -> hzgeh n m := λ nl, neghzgthtoleh _ _ nl .
Definition hzgthorleh ( n m : hz ) : ( hzgth n m ) ⨿ ( hzleh n m ) .
Show proof.
.
Definition hzlthorgeh ( n m : hz ) : ( hzlth n m ) ⨿ ( hzgeh n m ) := hzgthorleh _ _ .
Definition hzneqchoice ( n m : hz ) ( ne : neg ( n = m ) ) : ( hzgth n m ) ⨿ ( hzlth n m ) .
Show proof.
. intros . destruct ( hzgthorleh n m ) as [ g | l ] . destruct ( hzlthorgeh n m ) as [ g' | l' ] . destruct ( isasymmhzgth _ _ g g' ) . apply ( ii1 g ) . destruct ( hzlthorgeh n m ) as [ l' | g' ] . apply ( ii2 l' ) . destruct ( ne ( isantisymmhzleh _ _ l g' ) ) .
.Definition hzlehchoice ( n m : hz ) ( l : hzleh n m ) : ( hzlth n m ) ⨿ ( n = m ) .
Show proof.
. intros . destruct ( hzlthorgeh n m ) as [ l' | g ] . apply ( ii1 l' ) . apply ( ii2 ( isantisymmhzleh _ _ l g ) ) .
.Definition hzgehchoice ( n m : hz ) ( g : hzgeh n m ) : ( hzgth n m ) ⨿ ( n = m ) .
Show proof.
. intros . destruct ( hzgthorleh n m ) as [ g' | l ] . apply ( ii1 g' ) . apply ( ii2 ( isantisymmhzleh _ _ l g ) ) .
.Lemma hzgthgehtrans ( n m k : hz ) : hzgth n m -> hzgeh m k -> hzgth n k .
Show proof.
intros gnm gmk . destruct ( hzgehchoice m k gmk ) as [ g' | e ] . apply ( istranshzgth _ _ _ gnm g' ) . rewrite e in gnm . apply gnm .
Lemma hzgehgthtrans ( n m k : hz ) : hzgeh n m -> hzgth m k -> hzgth n k .
Show proof.
intros gnm gmk . destruct ( hzgehchoice n m gnm ) as [ g' | e ] . apply ( istranshzgth _ _ _ g' gmk ) . rewrite e . apply gmk .
Lemma hzlthlehtrans ( n m k : hz ) : hzlth n m -> hzleh m k -> hzlth n k .
Show proof.
.
Lemma hzlehlthtrans ( n m k : hz ) : hzleh n m -> hzlth m k -> hzlth n k .
Show proof.
.
Definition hzgthandplusl ( n m k : hz ) : hzgth n m -> hzgth ( k + n ) ( k + m ) .
Show proof.
.
Definition hzgthandplusr ( n m k : hz ) : hzgth n m -> hzgth ( n + k ) ( m + k ) .
Show proof.
.
Definition hzgthandpluslinv ( n m k : hz ) : hzgth ( k + n ) ( k + m ) -> hzgth n m .
Show proof.
intros g . set ( g' := hzgthandplusl _ _ ( - k ) g ) . clearbody g' . rewrite ( pathsinv0 ( hzplusassoc _ _ n ) ) in g' . rewrite ( pathsinv0 ( hzplusassoc _ _ m ) ) in g' . rewrite ( hzlminus k ) in g' . rewrite ( hzplusl0 _ ) in g' . rewrite ( hzplusl0 _ ) in g' . apply g' .
.Definition hzgthandplusrinv ( n m k : hz ) : hzgth ( n + k ) ( m + k ) -> hzgth n m .
Show proof.
intros l . rewrite ( hzpluscomm n k ) in l . rewrite ( hzpluscomm m k ) in l . apply ( hzgthandpluslinv _ _ _ l ) .
.Lemma hzgthsnn ( n : hz ) : hzgth ( n + 1 ) n .
Show proof.
. set ( int := hzgthandplusl _ _ n ( ct ( hzgth , isdecrelhzgth, 1 , 0 ) ) ) . clearbody int . rewrite ( hzplusr0 _ ) in int . apply int .
.Definition hzlthandplusl ( n m k : hz ) : hzlth n m -> hzlth ( k + n ) ( k + m ) := hzgthandplusl _ _ _ .
Definition hzlthandplusr ( n m k : hz ) : hzlth n m -> hzlth ( n + k ) ( m + k ) := hzgthandplusr _ _ _ .
Definition hzlthandpluslinv ( n m k : hz ) : hzlth ( k + n ) ( k + m ) -> hzlth n m := hzgthandpluslinv _ _ _ .
Definition hzlthandplusrinv ( n m k : hz ) : hzlth ( n + k ) ( m + k ) -> hzlth n m := hzgthandplusrinv _ _ _ .
Definition hzlthnsn ( n : hz ) : hzlth n ( n + 1 ) := hzgthsnn n .
Definition hzlehandplusl ( n m k : hz ) : hzleh n m -> hzleh ( k + n ) ( k + m ) := negf ( hzgthandpluslinv n m k ) .
Definition hzlehandplusr ( n m k : hz ) : hzleh n m -> hzleh ( n + k ) ( m + k ) := negf ( hzgthandplusrinv n m k ) .
Definition hzlehandpluslinv ( n m k : hz ) : hzleh ( k + n ) ( k + m ) -> hzleh n m := negf ( hzgthandplusl n m k ) .
Definition hzlehandplusrinv ( n m k : hz ) : hzleh ( n + k ) ( m + k ) -> hzleh n m := negf ( hzgthandplusr n m k ) .
Definition hzgehandplusl ( n m k : hz ) : hzgeh n m -> hzgeh ( k + n ) ( k + m ) := negf ( hzgthandpluslinv m n k ) .
Definition hzgehandplusr ( n m k : hz ) : hzgeh n m -> hzgeh ( n + k ) ( m + k ) := negf ( hzgthandplusrinv m n k ) .
Definition hzgehandpluslinv ( n m k : hz ) : hzgeh ( k + n ) ( k + m ) -> hzgeh n m := negf ( hzgthandplusl m n k ) .
Definition hzgehandplusrinv ( n m k : hz ) : hzgeh ( n + k ) ( m + k ) -> hzgeh n m := negf ( hzgthandplusr m n k ) .
Properties of hzgth in the terminology of algebra1.v (continued below)
Lemma isplushrelhzgth : @isbinophrel hzaddabgr hzgth .
Show proof.
.
Lemma isinvplushrelhzgth : @isinvbinophrel hzaddabgr hzgth .
Show proof.
.
Lemma isringmulthzgth : isringmultgt _ hzgth .
Show proof.
.
Lemma isinvringmulthzgth : isinvringmultgt _ hzgth .
Show proof.
. apply ( isinvringrigtoringmultgt natcommrig isplushrelnatgth isinvplushrelnatgth isinvrigmultgtnatgth ) .
.Lemma hzgth0andminus { n : hz } ( is : hzgth n 0 ) : hzlth ( - n ) 0 .
Show proof.
.
Lemma hzminusandgth0 { n : hz } ( is : hzgth ( - n ) 0 ) : hzlth n 0 .
Show proof.
.
Lemma hzlth0andminus { n : hz } ( is : hzlth n 0 ) : hzgth ( - n ) 0 .
Show proof.
.
Lemma hzminusandlth0 { n : hz } ( is : hzlth ( - n ) 0 ) : hzgth n 0 .
Show proof.
.
Lemma hzleh0andminus { n : hz } ( is : hzleh n 0 ) : hzgeh ( - n ) 0 .
Show proof.
.
Lemma hzminusandleh0 { n : hz } ( is : hzleh ( - n ) 0 ) : hzgeh n 0 .
Show proof.
.
Lemma hzgeh0andminus { n : hz } ( is : hzgeh n 0 ) : hzleh ( - n ) 0 .
Show proof.
.
Lemma hzminusandgeh0 { n : hz } ( is : hzgeh ( - n ) 0 ) : hzleh n 0 .
Show proof.
.
Definition hzgthandmultl ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth n m -> hzgth ( k * n ) ( k * m ) .
Show proof.
.
Definition hzgthandmultr ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth n m -> hzgth ( n * k ) ( m * k ) .
Show proof.
.
Definition hzgthandmultlinv ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth ( k * n ) ( k * m ) -> hzgth n m .
Show proof.
. intros is' . apply ( isinvringmultgttoislinvringmultgt hz isplushrelhzgth isinvringmulthzgth n m k is is' ) .
.Definition hzgthandmultrinv ( n m k : hz ) ( is : hzgth k hzzero ) : hzgth ( n * k ) ( m * k ) -> hzgth n m .
Show proof.
intros is' . apply ( isinvringmultgttoisrinvringmultgt hz isplushrelhzgth isinvringmulthzgth n m k is is' ) .
.Definition hzlthandmultl ( n m k : hz ) ( is : hzgth k 0 ) : hzlth n m -> hzlth ( k * n ) ( k * m ) := hzgthandmultl _ _ _ is .
Definition hzlthandmultr ( n m k : hz ) ( is : hzgth k 0 ) : hzlth n m -> hzlth ( n * k ) ( m * k ) := hzgthandmultr _ _ _ is .
Definition hzlthandmultlinv ( n m k : hz ) ( is : hzgth k 0 ) : hzlth ( k * n ) ( k * m ) -> hzlth n m := hzgthandmultlinv _ _ _ is .
Definition hzlthandmultrinv ( n m k : hz ) ( is : hzgth k 0 ) : hzlth ( n * k ) ( m * k ) -> hzlth n m := hzgthandmultrinv _ _ _ is .
Definition hzlehandmultl ( n m k : hz ) ( is : hzgth k 0 ) : hzleh n m -> hzleh ( k * n ) ( k * m ) := negf ( hzgthandmultlinv _ _ _ is ) .
Definition hzlehandmultr ( n m k : hz ) ( is : hzgth k 0 ) : hzleh n m -> hzleh ( n * k ) ( m * k ) := negf ( hzgthandmultrinv _ _ _ is ) .
Definition hzlehandmultlinv ( n m k : hz ) ( is : hzgth k 0 ) : hzleh ( k * n ) ( k * m ) -> hzleh n m := negf ( hzgthandmultl _ _ _ is ) .
Definition hzlehandmultrinv ( n m k : hz ) ( is : hzgth k 0 ) : hzleh ( n * k ) ( m * k ) -> hzleh n m := negf ( hzgthandmultr _ _ _ is ) .
Definition hzgehandmultl ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh n m -> hzgeh ( k * n ) ( k * m ) := negf ( hzgthandmultlinv _ _ _ is ) .
Definition hzgehandmultr ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh n m -> hzgeh ( n * k ) ( m * k ) := negf ( hzgthandmultrinv _ _ _ is ) .
Definition hzgehandmultlinv ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh ( k * n ) ( k * m ) -> hzgeh n m := negf ( hzgthandmultl _ _ _ is ) .
Definition hzgehandmultrinv ( n m k : hz ) ( is : hzgth k 0 ) : hzgeh ( n * k ) ( m * k ) -> hzgeh n m := negf ( hzgthandmultr _ _ _ is ) .
Multiplication of positive with positive, positive with negative, negative with positive, two negatives etc.
Lemma hzmultgth0gth0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzgth n 0 ) : hzgth ( m * n ) 0 .
Show proof.
.
Lemma hzmultgth0geh0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzgeh n 0 ) : hzgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzgehchoice _ _ isn ) as [ gn | en ] .
apply ( hzgthtogeh _ _ ( hzmultgth0gth0 ism gn ) ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
.apply ( hzgthtogeh _ _ ( hzmultgth0gth0 ism gn ) ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
Lemma hzmultgeh0gth0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzgth n 0 ) : hzgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzgehchoice _ _ ism ) as [ gm | em ] .
apply ( hzgthtogeh _ _ ( hzmultgth0gth0 gm isn ) ) .
rewrite em . rewrite ( hzmult0x _ ) . apply isreflhzgeh .
.apply ( hzgthtogeh _ _ ( hzmultgth0gth0 gm isn ) ) .
rewrite em . rewrite ( hzmult0x _ ) . apply isreflhzgeh .
Lemma hzmultgeh0geh0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzgeh n 0 ) : hzgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzgehchoice _ _ isn ) as [ gn | en ] .
apply ( hzmultgeh0gth0 ism gn ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
.apply ( hzmultgeh0gth0 ism gn ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
Lemma hzmultgth0lth0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzlth n 0 ) : hzlth ( m * n ) 0 .
Show proof.
.
Lemma hzmultgth0leh0 { m n : hz } ( ism : hzgth m 0 ) ( isn : hzleh n 0 ) : hzleh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] .
apply ( hzlthtoleh _ _ ( hzmultgth0lth0 ism ln ) ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzleh .
.apply ( hzlthtoleh _ _ ( hzmultgth0lth0 ism ln ) ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzleh .
Lemma hzmultgeh0lth0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzlth n 0 ) : hzleh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzlehchoice _ _ ism ) as [ lm | em ] .
apply ( hzlthtoleh _ _ ( hzmultgth0lth0 lm isn ) ) .
destruct em . rewrite ( hzmult0x _ ) . apply isreflhzleh .
.apply ( hzlthtoleh _ _ ( hzmultgth0lth0 lm isn ) ) .
destruct em . rewrite ( hzmult0x _ ) . apply isreflhzleh .
Lemma hzmultgeh0leh0 { m n : hz } ( ism : hzgeh m 0 ) ( isn : hzleh n 0 ) : hzleh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] .
apply ( hzmultgeh0lth0 ism ln ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzleh .
.apply ( hzmultgeh0lth0 ism ln ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzleh .
Lemma hzmultlth0gth0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzgth n 0 ) : hzlth ( m * n ) 0 .
Show proof.
.
Lemma hzmultlth0geh0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzgeh n 0 ) : hzleh ( m * n ) 0 .
Show proof.
.
Lemma hzmultleh0gth0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzgth n 0 ) : hzleh ( m * n ) 0 .
Show proof.
.
Lemma hzmultleh0geh0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzgeh n 0 ) : hzleh ( m * n ) 0 .
Show proof.
.
Lemma hzmultlth0lth0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzlth n 0 ) : hzgth ( m * n ) 0 .
Show proof.
. intros . assert ( ism' := hzlth0andminus ism ) . assert ( isn' := hzlth0andminus isn ) . assert ( int := isringmulthzgth _ _ ism' isn' ) . rewrite ( ringmultminusminus hz ) in int . apply int .
.Lemma hzmultlth0leh0 { m n : hz } ( ism : hzlth m 0 ) ( isn : hzleh n 0 ) : hzgeh ( m * n ) 0 .
Show proof.
. intros . intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] .
apply ( hzgthtogeh _ _ ( hzmultlth0lth0 ism ln ) ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
.apply ( hzgthtogeh _ _ ( hzmultlth0lth0 ism ln ) ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
Lemma hzmultleh0lth0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzlth n 0 ) : hzgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzlehchoice _ _ ism ) as [ lm | em ] .
apply ( hzgthtogeh _ _ ( hzmultlth0lth0 lm isn ) ) .
rewrite em . rewrite ( hzmult0x _ ) . apply isreflhzgeh .
.apply ( hzgthtogeh _ _ ( hzmultlth0lth0 lm isn ) ) .
rewrite em . rewrite ( hzmult0x _ ) . apply isreflhzgeh .
Lemma hzmultleh0leh0 { m n : hz } ( ism : hzleh m 0 ) ( isn : hzleh n 0 ) : hzgeh ( m * n ) 0 .
Show proof.
. intros . destruct ( hzlehchoice _ _ isn ) as [ ln | en ] .
apply ( hzmultleh0lth0 ism ln ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
.apply ( hzmultleh0lth0 ism ln ) .
rewrite en . rewrite ( hzmultx0 m ) . apply isreflhzgeh .
hz as an integral domain
Lemma isintdomhz : isintdom hz .
Show proof.
. split with isnonzerorighz . intros a b e0 . destruct ( isdeceqhz a 0 ) as [ ea | nea ] . apply ( hinhpr ( ii1 ea ) ) . destruct ( isdeceqhz b 0 ) as [ eb | neb ] . apply ( hinhpr ( ii2 eb ) ) . destruct ( hzneqchoice _ _ nea ) as [ ga | la ] . destruct ( hzneqchoice _ _ neb ) as [ gb | lb ] . destruct ( hzgthtoneq _ _ ( hzmultgth0gth0 ga gb ) e0 ) . destruct ( hzlthtoneq _ _ ( hzmultgth0lth0 ga lb ) e0 ) . destruct ( hzneqchoice _ _ neb ) as [ gb | lb ] . destruct ( hzlthtoneq _ _ ( hzmultlth0gth0 la gb ) e0 ) . destruct ( hzgthtoneq _ _ ( hzmultlth0lth0 la lb ) e0 ) .
.Definition hzintdom : intdom := tpair _ _ isintdomhz .
Definition hzneq0andmult ( n m : hz ) ( isn : hzneq n 0 ) ( ism : hzneq m 0 ) : hzneq ( n * m ) 0 := intdomneq0andmult hzintdom n m isn ism .
Lemma hzmultlcan ( a b c : hz ) ( ne : neg ( c = 0 ) ) ( e : ( c * a ) = ( c * b ) ) : a = b .
Show proof.
.
Lemma hzmultrcan ( a b c : hz ) ( ne : neg ( c = 0 ) ) ( e : ( a * c ) = ( b * c ) ) : a = b .
Show proof.
.
Lemma isinclhzmultl ( n : hz )( ne : neg ( n = 0 ) ) : isincl ( λ m : hz, n * m ) .
Show proof.
.
Lemma isinclhzmultr ( n : hz )( ne : neg ( n = 0 ) ) : isincl ( λ m : hz, m * n ) .
Show proof.
Definition hzgthtogths ( n m : hz ) : hzgth n m -> hzgth ( n + 1 ) m .
Show proof.
.
Definition hzlthtolths ( n m : hz ) : hzlth n m -> hzlth n ( m + 1 ) := hzgthtogths _ _ .
Definition hzlehtolehs ( n m : hz ) : hzleh n m -> hzleh n ( m + 1 ) .
Show proof.
.
Definition hzgehtogehs ( n m : hz ) : hzgeh n m -> hzgeh ( n + 1 ) m := hzlehtolehs _ _ .
Lemma hzgthtogehsn ( n m : hz ) : hzgth n m -> hzgeh n ( m + 1 ) .
Show proof.
assert ( int : ∏ n m , isaprop ( hzgth n m -> hzgeh n ( m + 1 ) ) ) .
{ intros . apply impred . intro . apply ( pr2 _ ) . }
unfold hzgth in * . apply ( setquotuniv2prop _ ( λ n m, make_hProp _ ( int n m ) ) ) . set ( R := abgrdiffrelint nataddabmonoid natgth ) .
intros x x' . change ( R x x' -> ( neg ( R ( @op ( abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig) ) x' ( make_dirprod 1%nat 0%nat ) ) x ) ) ) .
unfold R . unfold abgrdiffrelint . simpl .
apply ( @hinhuniv _ (make_hProp ( neg ( ishinh_UU _ ) ) ( isapropneg _ ) ) ) .
intro t2 . simpl . unfold neg . apply ( @hinhuniv _ ( make_hProp _ isapropempty ) ) .
intro t2' .
set ( x1 := pr1 x ) . set ( a1 := pr2 x ) . set ( x2 := pr1 x' ) .
set ( a2 := pr2 x' ) . set ( c1 := pr1 t2 ) . assert ( r1 := pr2 t2 ) .
change ( pr1 ( ( x1 + a2 + c1 ) > ( x2 + a1 + c1 ) ) ) in r1 .
set ( c2 := pr1 t2' ) . assert ( r2 := pr2 t2' ) .
change ( pr1 ( ( ( x2 + 1 ) + a1 + c2 ) > ( x1 + ( a2 + 0 ) + c2 ) ) ) in r2 .
assert ( r1' := natgthandplusrinv _ _ c1 r1 ) .
assert ( r2' := natgthandplusrinv _ _ c2 r2 ) .
rewrite ( natplusr0 _ ) in r2' .
rewrite ( natpluscomm _ 1 ) in r2' .
rewrite ( natplusassoc _ _ _ ) in r2' .
change (1 + (x2 + a1) > x1 + a2) with (x1 + a2 ≤ x2 + a1) in r2'.
contradicts (natlehneggth r2') r1'.
.{ intros . apply impred . intro . apply ( pr2 _ ) . }
unfold hzgth in * . apply ( setquotuniv2prop _ ( λ n m, make_hProp _ ( int n m ) ) ) . set ( R := abgrdiffrelint nataddabmonoid natgth ) .
intros x x' . change ( R x x' -> ( neg ( R ( @op ( abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig) ) x' ( make_dirprod 1%nat 0%nat ) ) x ) ) ) .
unfold R . unfold abgrdiffrelint . simpl .
apply ( @hinhuniv _ (make_hProp ( neg ( ishinh_UU _ ) ) ( isapropneg _ ) ) ) .
intro t2 . simpl . unfold neg . apply ( @hinhuniv _ ( make_hProp _ isapropempty ) ) .
intro t2' .
set ( x1 := pr1 x ) . set ( a1 := pr2 x ) . set ( x2 := pr1 x' ) .
set ( a2 := pr2 x' ) . set ( c1 := pr1 t2 ) . assert ( r1 := pr2 t2 ) .
change ( pr1 ( ( x1 + a2 + c1 ) > ( x2 + a1 + c1 ) ) ) in r1 .
set ( c2 := pr1 t2' ) . assert ( r2 := pr2 t2' ) .
change ( pr1 ( ( ( x2 + 1 ) + a1 + c2 ) > ( x1 + ( a2 + 0 ) + c2 ) ) ) in r2 .
assert ( r1' := natgthandplusrinv _ _ c1 r1 ) .
assert ( r2' := natgthandplusrinv _ _ c2 r2 ) .
rewrite ( natplusr0 _ ) in r2' .
rewrite ( natpluscomm _ 1 ) in r2' .
rewrite ( natplusassoc _ _ _ ) in r2' .
change (1 + (x2 + a1) > x1 + a2) with (x1 + a2 ≤ x2 + a1) in r2'.
contradicts (natlehneggth r2') r1'.
Lemma hzgthsntogeh ( n m : hz ) : hzgth ( n + 1 ) m -> hzgeh n m .
Show proof.
Lemma hzlehsntolth ( n m : hz ) : hzleh ( n + 1 ) m -> hzlth n m .
Show proof.
.
Lemma hzlthtolehsn ( n m : hz ) : hzlth n m -> hzleh ( n + 1 ) m .
Show proof.
.
Lemma hzlthsntoleh ( n m : hz ) : hzlth n ( m + 1 ) -> hzleh n m .
Show proof.
Lemma hzgehsntogth ( n m : hz ) : hzgeh n ( m + 1 ) -> hzgth n m .
Show proof.
.
Lemma hzlehchoice2 ( n m : hz ) : hzleh n m -> coprod ( hzleh ( n + 1 ) m ) ( n = m ) .
Show proof.
. intros l . destruct ( hzlehchoice n m l ) as [ l' | e ] . apply ( ii1 ( hzlthtolehsn _ _ l' ) ) . apply ( ii2 e ) .
.Lemma hzgehchoice2 ( n m : hz ) : hzgeh n m -> coprod ( hzgeh n ( m + 1 ) ) ( n = m ) .
Show proof.
. intros g . destruct ( hzgehchoice n m g ) as [ g' | e ] . apply ( ii1 ( hzgthtogehsn _ _ g' ) ) . apply ( ii2 e ) .
.Lemma hzgthchoice2 ( n m : hz ) : hzgth n m -> coprod ( hzgth n ( m + 1 ) ) ( n = ( m + 1 ) ) .
Show proof.
intros g . destruct ( hzgehchoice _ _ ( hzgthtogehsn _ _ g ) ) as [ g' | e ] . apply ( ii1 g' ) . apply ( ii2 e ) .
.Lemma hzlthchoice2 ( n m : hz ) : hzlth n m -> coprod ( hzlth ( n + 1 ) m ) ( ( n + 1 ) = m ) .
Show proof.
intros l . destruct ( hzlehchoice _ _ ( hzlthtolehsn _ _ l ) ) as [ l' | e ] . apply ( ii1 l' ) . apply ( ii2 e ) .
.Operations and comparisons on hz and natnattohz
Lemma natnattohzandgth ( xa1 xa2 : dirprod nat nat ) ( is : hzgth ( setquotpr _ xa1 ) ( setquotpr _ xa2 ) ) : natgth ( ( pr1 xa1 ) + ( pr2 xa2 ) ) ( ( pr1 xa2 ) + ( pr2 xa1 ) ) .
Show proof.
. intros . change ( ishinh_UU ( total2 ( λ a0, natgth (pr1 xa1 + pr2 xa2 + a0) (pr1 xa2 + pr2 xa1 + a0) ) ) ) in is . generalize is . apply @hinhuniv . intro t2 . set ( a0 := pr1 t2 ) . assert ( g := pr2 t2 ) . change ( pr1 ( natgth (pr1 xa1 + pr2 xa2 + a0) (pr1 xa2 + pr2 xa1 + a0) ) ) in g . apply ( natgthandplusrinv _ _ a0 g ) .
.Lemma natnattohzandlth ( xa1 xa2 : dirprod nat nat ) ( is : hzlth ( setquotpr _ xa1 ) ( setquotpr _ xa2 ) ) : natlth ( ( pr1 xa1 ) + ( pr2 xa2 ) ) ( ( pr1 xa2 ) + ( pr2 xa1 ) ) .
Show proof.
.
Definition nattohz : nat -> hz := λ n, setquotpr _ ( make_dirprod n 0%nat ) .
Definition isinclnattohz : isincl nattohz := isincltoringdiff natcommrig ( λ n, isinclnatplusr n ) .
Definition nattohzandneq ( n m : nat ) ( is : natnegpaths n m ) : hzneq ( nattohz n ) ( nattohz m ) := negf ( invmaponpathsincl _ isinclnattohz n m ) is .
Definition nattohzand0 : ( nattohz 0%nat ) = 0 := idpath _ .
Definition nattohzandS ( n : nat ) : ( nattohz ( S n ) ) = ( 1 + nattohz n ) := isbinop1funtoringdiff natcommrig 1%nat n .
Definition nattohzand1 : ( nattohz 1%nat ) = 1 := idpath _ .
Lemma nattorig_nattohz :
∏ n : nat, nattorig (X := hz) n = nattohz n.
Show proof.
induction n as [|n IHn].
- unfold nattorig, nattohz ; simpl.
reflexivity.
- rewrite nattorigS, IHn.
apply pathsinv0, nattohzandS.
- unfold nattorig, nattohz ; simpl.
reflexivity.
- rewrite nattorigS, IHn.
apply pathsinv0, nattohzandS.
Definition nattohzandplus ( n m : nat ) : ( nattohz ( n + m )%nat ) = ( nattohz n + nattohz m ) := isbinop1funtoringdiff natcommrig n m .
Definition nattohzandminus ( n m : nat ) ( is : natgeh n m ) : ( nattohz ( n - m )%nat ) = ( nattohz n - nattohz m ) .
Show proof.
. intros . apply ( hzplusrcan _ _ ( nattohz m ) ) . unfold hzminus . rewrite ( hzplusassoc ( nattohz n ) ( - nattohz m ) ( nattohz m ) ) . rewrite ( hzlminus _ ) . rewrite hzplusr0 . rewrite ( pathsinv0 ( nattohzandplus _ _ ) ) . rewrite ( minusplusnmm _ _ is ) . apply idpath .
.Opaque nattohzandminus .
Definition nattohzandmult ( n m : nat ) : ( nattohz ( n * m )%nat ) = ( nattohz n * nattohz m ) .
Show proof.
. intros . simpl . change nattohz with ( toringdiff natcommrig ) . apply ( isbinop2funtoringdiff natcommrig n m ) .
.Definition nattohzandgth ( n m : nat ) ( is : natgth n m ) : hzgth ( nattohz n ) ( nattohz m ) := iscomptoringdiff natcommrig isplushrelnatgth n m is .
Definition nattohzandlth ( n m : nat ) ( is : natlth n m ) : hzlth ( nattohz n ) ( nattohz m ) := nattohzandgth m n is .
Definition nattohzandleh ( n m : nat ) ( is : natleh n m ) : hzleh ( nattohz n ) ( nattohz m ) .
Show proof.
. intros . destruct ( natlehchoice _ _ is ) as [ l | e ] . apply ( hzlthtoleh _ _ ( nattohzandlth _ _ l ) ) . rewrite e . apply ( isreflhzleh ) .
.Definition nattohzandgeh ( n m : nat ) ( is : natgeh n m ) : hzgeh ( nattohz n ) ( nattohz m ) := nattohzandleh _ _ is .
Definition hzabsvalint : ( dirprod nat nat ) -> nat .
Show proof.
. intro nm . destruct ( natgthorleh ( pr1 nm ) ( pr2 nm ) ) . apply ( sub ( pr1 nm ) ( pr2 nm ) ) . apply ( sub ( pr2 nm ) ( pr1 nm ) ) .
.Lemma hzabsvalintcomp : @iscomprelfun ( dirprod nat nat ) nat ( hrelabgrdiff nataddabmonoid ) hzabsvalint .
Show proof.
. unfold iscomprelfun . intros x x' . unfold hrelabgrdiff . simpl . apply ( @hinhuniv _ ( make_hProp _ ( isasetnat (hzabsvalint x) (hzabsvalint x') ) ) ) . unfold hzabsvalint . set ( n := ( pr1 x ) : nat ) . set ( m := ( pr2 x ) : nat ) . set ( n' := ( pr1 x' ) : nat ) . set ( m' := ( pr2 x' ) : nat ) . set ( int := natgthorleh n m ) . set ( int' := natgthorleh n' m' ) . intro tt0 . simpl . destruct tt0 as [ x0 eq ] . simpl in eq . assert ( e' := invmaponpathsincl _ ( isinclnatplusr x0 ) _ _ eq ) .
destruct int as [isgt | isle ] . destruct int' as [ isgt' | isle' ] .
apply ( invmaponpathsincl _ ( isinclnatplusr ( m + m' ) ) ) . rewrite ( pathsinv0 ( natplusassoc ( n - m ) m m' ) ) . rewrite ( natpluscomm m m' ) . rewrite ( pathsinv0 ( natplusassoc ( n' - m' ) m' m ) ) . rewrite ( minusplusnmm n m ( natgthtogeh _ _ isgt ) ) . rewrite ( minusplusnmm n' m' ( natgthtogeh _ _ isgt' ) ) . apply e' .
assert ( e'' := natlehandplusl n' m' n isle' ) . assert ( e''' := natgthandplusr n m n' isgt ) . assert ( e'''' := natlthlehtrans _ _ _ e''' e'' ) . rewrite e' in e'''' . rewrite ( natpluscomm m n' ) in e'''' . destruct ( isirreflnatgth _ e'''' ) .
destruct int' as [ isgt' | isle' ] .
destruct ( natpluscomm m n') . set ( e'' := natlehandplusr n m m' isle ) . set ( e''' := natgthandplusl n' m' m isgt' ) . set ( e'''' := natlehlthtrans _ _ _ e'' e''' ) . rewrite e' in e'''' . destruct ( isirreflnatgth _ e'''' ) .
apply ( invmaponpathsincl _ ( isinclnatplusr ( n + n') ) ) . rewrite ( pathsinv0 ( natplusassoc ( m - n ) n n' ) ) . rewrite ( natpluscomm n n' ) . rewrite ( pathsinv0 ( natplusassoc ( m' - n') n' n ) ) . rewrite ( minusplusnmm m n isle ) . rewrite ( minusplusnmm m' n' isle' ) . rewrite ( natpluscomm m' n ) . rewrite ( natpluscomm m n' ) . apply ( pathsinv0 e' ) .
.destruct int as [isgt | isle ] . destruct int' as [ isgt' | isle' ] .
apply ( invmaponpathsincl _ ( isinclnatplusr ( m + m' ) ) ) . rewrite ( pathsinv0 ( natplusassoc ( n - m ) m m' ) ) . rewrite ( natpluscomm m m' ) . rewrite ( pathsinv0 ( natplusassoc ( n' - m' ) m' m ) ) . rewrite ( minusplusnmm n m ( natgthtogeh _ _ isgt ) ) . rewrite ( minusplusnmm n' m' ( natgthtogeh _ _ isgt' ) ) . apply e' .
assert ( e'' := natlehandplusl n' m' n isle' ) . assert ( e''' := natgthandplusr n m n' isgt ) . assert ( e'''' := natlthlehtrans _ _ _ e''' e'' ) . rewrite e' in e'''' . rewrite ( natpluscomm m n' ) in e'''' . destruct ( isirreflnatgth _ e'''' ) .
destruct int' as [ isgt' | isle' ] .
destruct ( natpluscomm m n') . set ( e'' := natlehandplusr n m m' isle ) . set ( e''' := natgthandplusl n' m' m isgt' ) . set ( e'''' := natlehlthtrans _ _ _ e'' e''' ) . rewrite e' in e'''' . destruct ( isirreflnatgth _ e'''' ) .
apply ( invmaponpathsincl _ ( isinclnatplusr ( n + n') ) ) . rewrite ( pathsinv0 ( natplusassoc ( m - n ) n n' ) ) . rewrite ( natpluscomm n n' ) . rewrite ( pathsinv0 ( natplusassoc ( m' - n') n' n ) ) . rewrite ( minusplusnmm m n isle ) . rewrite ( minusplusnmm m' n' isle' ) . rewrite ( natpluscomm m' n ) . rewrite ( natpluscomm m n' ) . apply ( pathsinv0 e' ) .
Definition hzabsval : hz -> nat := setquotuniv _ natset hzabsvalint hzabsvalintcomp .
Lemma hzabsval0 : ( hzabsval 0 ) = 0%nat .
Show proof.
. apply idpath .
.Lemma hzabsvalgth0 { x : hz } ( is : hzgth x 0 ) : ( nattohz ( hzabsval x ) ) = x .
Show proof.
.
revert x is.
assert ( int : ∏ x : hz , isaprop ( hzgth x 0 -> ( nattohz ( hzabsval x ) ) = x ) ) . intro . apply impred . intro . apply ( setproperty hz ) . apply ( setquotunivprop _ ( λ x, make_hProp _ ( int x ) ) ) . intros xa g . simpl in xa . assert ( g' := natnattohzandgth _ _ g ) . simpl in g' . simpl . change (( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) ( make_dirprod ( hzabsvalint xa ) 0%nat ) ) = ( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) xa ) ) . apply weqpathsinsetquot . simpl . apply hinhpr . split with 0%nat . change ( pr1 ( natgth ( pr1 xa + 0%nat ) ( pr2 xa ) ) ) in g' . rewrite ( natplusr0 _ ) in g' . change ((hzabsvalint xa + pr2 xa + 0)%nat = (pr1 xa + 0 + 0)%nat ) . rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . unfold hzabsvalint . destruct ( natgthorleh (pr1 xa) (pr2 xa) ) as [ g'' | l ] .
rewrite ( minusplusnmm _ _ ( natlthtoleh _ _ g'' ) ) . apply idpath .
contradicts (natlehneggth l) g'.
.revert x is.
assert ( int : ∏ x : hz , isaprop ( hzgth x 0 -> ( nattohz ( hzabsval x ) ) = x ) ) . intro . apply impred . intro . apply ( setproperty hz ) . apply ( setquotunivprop _ ( λ x, make_hProp _ ( int x ) ) ) . intros xa g . simpl in xa . assert ( g' := natnattohzandgth _ _ g ) . simpl in g' . simpl . change (( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) ( make_dirprod ( hzabsvalint xa ) 0%nat ) ) = ( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) xa ) ) . apply weqpathsinsetquot . simpl . apply hinhpr . split with 0%nat . change ( pr1 ( natgth ( pr1 xa + 0%nat ) ( pr2 xa ) ) ) in g' . rewrite ( natplusr0 _ ) in g' . change ((hzabsvalint xa + pr2 xa + 0)%nat = (pr1 xa + 0 + 0)%nat ) . rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . unfold hzabsvalint . destruct ( natgthorleh (pr1 xa) (pr2 xa) ) as [ g'' | l ] .
rewrite ( minusplusnmm _ _ ( natlthtoleh _ _ g'' ) ) . apply idpath .
contradicts (natlehneggth l) g'.
Opaque hzabsvalgth0 .
Lemma hzabsvalgeh0 { x : hz } ( is : hzgeh x 0 ) : ( nattohz ( hzabsval x ) ) = x .
Show proof.
. intros . destruct ( hzgehchoice _ _ is ) as [ g | e ] . apply ( hzabsvalgth0 g ) . rewrite e . apply idpath .
.Lemma hzabsvallth0 { x : hz } ( is : hzlth x 0 ) : ( nattohz ( hzabsval x ) ) = ( - x ) .
Show proof.
.
revert x is.
assert ( int : ∏ x : hz , isaprop ( hzlth x 0 -> ( nattohz ( hzabsval x ) ) = ( - x ) ) ) . intro . apply impred . intro . apply ( setproperty hz ) . apply ( setquotunivprop _ ( λ x, make_hProp _ ( int x ) ) ) . intros xa l . simpl in xa . assert ( l' := natnattohzandlth _ _ l ) . simpl in l' . simpl . change (( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) ( make_dirprod ( hzabsvalint xa ) 0%nat ) ) = ( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) ( make_dirprod ( pr2 xa ) ( pr1 xa ) ) ) ) . apply weqpathsinsetquot . simpl . apply hinhpr . split with 0%nat . change ( pr1 ( natlth ( pr1 xa + 0%nat ) ( pr2 xa ) ) ) in l' . rewrite ( natplusr0 _ ) in l' . change ((hzabsvalint xa + pr1 xa + 0)%nat = (pr2 xa + 0 + 0)%nat). rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . unfold hzabsvalint . destruct ( natgthorleh (pr1 xa) (pr2 xa) ) as [ g | l'' ] .
destruct ( isasymmnatgth _ _ g l' ) .
rewrite ( minusplusnmm _ _ l'' ) . apply idpath .
.revert x is.
assert ( int : ∏ x : hz , isaprop ( hzlth x 0 -> ( nattohz ( hzabsval x ) ) = ( - x ) ) ) . intro . apply impred . intro . apply ( setproperty hz ) . apply ( setquotunivprop _ ( λ x, make_hProp _ ( int x ) ) ) . intros xa l . simpl in xa . assert ( l' := natnattohzandlth _ _ l ) . simpl in l' . simpl . change (( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) ( make_dirprod ( hzabsvalint xa ) 0%nat ) ) = ( setquotpr (eqrelabgrdiff (rigaddabmonoid natcommrig)) ( make_dirprod ( pr2 xa ) ( pr1 xa ) ) ) ) . apply weqpathsinsetquot . simpl . apply hinhpr . split with 0%nat . change ( pr1 ( natlth ( pr1 xa + 0%nat ) ( pr2 xa ) ) ) in l' . rewrite ( natplusr0 _ ) in l' . change ((hzabsvalint xa + pr1 xa + 0)%nat = (pr2 xa + 0 + 0)%nat). rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . rewrite ( natplusr0 _ ) . unfold hzabsvalint . destruct ( natgthorleh (pr1 xa) (pr2 xa) ) as [ g | l'' ] .
destruct ( isasymmnatgth _ _ g l' ) .
rewrite ( minusplusnmm _ _ l'' ) . apply idpath .
Opaque hzabsvallth0 .
Lemma hzabsvalleh0 { x : hz } ( is : hzleh x 0 ) : ( nattohz ( hzabsval x ) ) = ( - x ) .
Show proof.
. intros . destruct ( hzlehchoice _ _ is ) as [ l | e ] . apply ( hzabsvallth0 l ) . rewrite e . apply idpath .
.Lemma hzabsvaleq0 { x : hz } ( e : ( hzabsval x ) = 0%nat ) : x = 0 .
Show proof.
. intros . destruct ( isdeceqhz x 0 ) as [ e0 | ne0 ] . apply e0 . destruct ( hzneqchoice _ _ ne0 ) as [ g | l ] .
assert ( e' := hzabsvalgth0 g ) . rewrite e in e' . change ( 0 = x ) in e' . apply ( pathsinv0 e' ) .
assert ( e' := hzabsvallth0 l ) . rewrite e in e' . change ( 0 = ( - x ) ) in e' . assert ( g := hzlth0andminus l ) . rewrite e' in g . destruct ( isirreflhzgth _ g ) .
.assert ( e' := hzabsvalgth0 g ) . rewrite e in e' . change ( 0 = x ) in e' . apply ( pathsinv0 e' ) .
assert ( e' := hzabsvallth0 l ) . rewrite e in e' . change ( 0 = ( - x ) ) in e' . assert ( g := hzlth0andminus l ) . rewrite e' in g . destruct ( isirreflhzgth _ g ) .
Definition hzabsvalneq0 { x : hz } ne := neg_to_negProp (nP := natneq _ _) (negf ( @hzabsvaleq0 x ) ne).
Lemma hzabsvalandmult ( a b : hz ) : ( ( hzabsval a ) * ( hzabsval b ) )%nat = ( hzabsval ( a * b ) ) .
Show proof.
. intros . apply ( invmaponpathsincl _ isinclnattohz ) . rewrite ( nattohzandmult _ _ ) . destruct ( hzgthorleh a 0 ) as [ ga | lea ] . destruct ( hzgthorleh b 0 ) as [ gb | leb ] .
rewrite ( hzabsvalgth0 ga ) . rewrite ( hzabsvalgth0 gb ) . rewrite ( hzabsvalgth0 ( hzmultgth0gth0 ga gb ) ) . apply idpath .
rewrite ( hzabsvalgth0 ga ) . rewrite ( hzabsvalleh0 leb ) . rewrite ( hzabsvalleh0 ( hzmultgth0leh0 ga leb ) ) . apply ( ringrmultminus hz ) . destruct ( hzgthorleh b 0 ) as [ gb | leb ] .
rewrite ( hzabsvalgth0 gb ) . rewrite ( hzabsvalleh0 lea ) . rewrite ( hzabsvalleh0 ( hzmultleh0gth0 lea gb ) ) . apply ( ringlmultminus hz ) .
rewrite ( hzabsvalleh0 lea ) . rewrite ( hzabsvalleh0 leb ) . rewrite ( hzabsvalgeh0 ( hzmultleh0leh0 lea leb ) ) . apply (ringmultminusminus hz ) .
.rewrite ( hzabsvalgth0 ga ) . rewrite ( hzabsvalgth0 gb ) . rewrite ( hzabsvalgth0 ( hzmultgth0gth0 ga gb ) ) . apply idpath .
rewrite ( hzabsvalgth0 ga ) . rewrite ( hzabsvalleh0 leb ) . rewrite ( hzabsvalleh0 ( hzmultgth0leh0 ga leb ) ) . apply ( ringrmultminus hz ) . destruct ( hzgthorleh b 0 ) as [ gb | leb ] .
rewrite ( hzabsvalgth0 gb ) . rewrite ( hzabsvalleh0 lea ) . rewrite ( hzabsvalleh0 ( hzmultleh0gth0 lea gb ) ) . apply ( ringlmultminus hz ) .
rewrite ( hzabsvalleh0 lea ) . rewrite ( hzabsvalleh0 leb ) . rewrite ( hzabsvalgeh0 ( hzmultleh0leh0 lea leb ) ) . apply (ringmultminusminus hz ) .
Some common equalities on integers
These lemmas are used for example in Complexes.v to construct complexes.
Local Opaque hz isdecrelhzeq iscommringops.
Lemma hzeqbooleqii (i : hz) : hzbooleq i i = true.
Show proof.
Lemma hzbooleqisi (i : hz) : hzbooleq i (i + 1) = false.
Show proof.
Lemma hzbooleqisi' (i : hz) : hzbooleq i (i + 1) = false.
Show proof.
Lemma hzbooleqissi (i : hz) : hzbooleq i (i + 1 + 1) = false.
Show proof.
Lemma hzeqeisi {i i0 : hz} (e : hzeq i i0) (e' : hzeq i (i0 + 1)) : empty.
Show proof.
Lemma hzeqisi {i : hz} (e' : hzeq i (i + 1)) : empty.
Show proof.
Lemma hzeqissi {i : hz} (e : hzeq i (i + 1 + 1)) : empty.
Show proof.
Lemma hzeqeissi {i i0 : hz} (e : hzeq i i0) (e' : hzeq i (i0 + 1 + 1)) : empty.
Show proof.
Lemma hzeqsnmnsm {n m : hz} (e : hzeq (n + 1) m) (e' : hzeq n (m + 1)) : empty.
Show proof.
Lemma hzeqnmplusr {n m i : hz} (e : n = m) (e' : ¬ (n + i = m + i)) : empty.
Show proof.
Lemma hzeqnmplusr' {n m i : hz} (e : ¬ (n = m)) (e' : n + i = m + i) : empty.
Show proof.
Lemma isdecrelhzeqi (i : hz) : isdecrelhzeq i i = ii1 (idpath _).
Show proof.
Lemma isdecrelhzeqminusplus (i j : hz) : isdecrelhzeq i (i - j + j) = ii1 (hzrminusplus' i j).
Show proof.
Lemma isdecrelhzeqminusplus' (i j : hz) : isdecrelhzeq (i - j + j) i = ii1 (hzrminusplus i j).
Show proof.
Lemma hzeqpii {i : hz} : i - 1 != i.
Show proof.
Lemma isdecrelhzeqpii (i : hz) :
isdecrelhzeq (i - 1) i = ii2 (fun (e : hzeq (i - 1) i) => hzeqpii e).
Show proof.
Local Transparent hz isdecrelhzeq iscommringops.
Lemma hzeqbooleqii (i : hz) : hzbooleq i i = true.
Show proof.
unfold hzbooleq. unfold decreltobrel. induction (pr2 hzdeceq i i) as [T | F].
- apply idpath.
- apply fromempty. apply F. apply idpath.
- apply idpath.
- apply fromempty. apply F. apply idpath.
Lemma hzbooleqisi (i : hz) : hzbooleq i (i + 1) = false.
Show proof.
apply negrtopaths.
apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i.
confirm_not_equal isdecrelhzeq.
apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i.
confirm_not_equal isdecrelhzeq.
Lemma hzbooleqisi' (i : hz) : hzbooleq i (i + 1) = false.
Show proof.
apply negrtopaths.
apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i.
simple refine (confirm_not_equal isdecrelhzeq _ _ _).
reflexivity.
apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i.
simple refine (confirm_not_equal isdecrelhzeq _ _ _).
reflexivity.
Lemma hzbooleqissi (i : hz) : hzbooleq i (i + 1 + 1) = false.
Show proof.
apply negrtopaths.
rewrite hzplusassoc.
apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i.
confirm_not_equal isdecrelhzeq.
rewrite hzplusassoc.
apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i.
confirm_not_equal isdecrelhzeq.
Lemma hzeqeisi {i i0 : hz} (e : hzeq i i0) (e' : hzeq i (i0 + 1)) : empty.
Show proof.
apply nopathstruetofalse.
use (pathscomp0 _ (hzbooleqisi i0)).
rewrite <- e'. rewrite <- e.
apply (! (hzeqbooleqii i)).
use (pathscomp0 _ (hzbooleqisi i0)).
rewrite <- e'. rewrite <- e.
apply (! (hzeqbooleqii i)).
Lemma hzeqisi {i : hz} (e' : hzeq i (i + 1)) : empty.
Show proof.
Lemma hzeqissi {i : hz} (e : hzeq i (i + 1 + 1)) : empty.
Show proof.
set (tmp := hzbooleqissi i). cbn in e. rewrite <- e in tmp.
rewrite (hzeqbooleqii i) in tmp. apply nopathstruetofalse. apply tmp.
rewrite (hzeqbooleqii i) in tmp. apply nopathstruetofalse. apply tmp.
Lemma hzeqeissi {i i0 : hz} (e : hzeq i i0) (e' : hzeq i (i0 + 1 + 1)) : empty.
Show proof.
Lemma hzeqsnmnsm {n m : hz} (e : hzeq (n + 1) m) (e' : hzeq n (m + 1)) : empty.
Show proof.
Lemma hzeqnmplusr {n m i : hz} (e : n = m) (e' : ¬ (n + i = m + i)) : empty.
Show proof.
Lemma hzeqnmplusr' {n m i : hz} (e : ¬ (n = m)) (e' : n + i = m + i) : empty.
Show proof.
Lemma isdecrelhzeqi (i : hz) : isdecrelhzeq i i = ii1 (idpath _).
Show proof.
induction (isdecrelhzeq i i) as [T | F].
- apply maponpaths. apply isasethz.
- apply fromempty. apply F. apply idpath.
- apply maponpaths. apply isasethz.
- apply fromempty. apply F. apply idpath.
Lemma isdecrelhzeqminusplus (i j : hz) : isdecrelhzeq i (i - j + j) = ii1 (hzrminusplus' i j).
Show proof.
induction (isdecrelhzeq i (i - j + j)) as [T | F].
- apply maponpaths. apply isasethz.
- apply fromempty. apply F. apply (hzrminusplus' i j).
- apply maponpaths. apply isasethz.
- apply fromempty. apply F. apply (hzrminusplus' i j).
Lemma isdecrelhzeqminusplus' (i j : hz) : isdecrelhzeq (i - j + j) i = ii1 (hzrminusplus i j).
Show proof.
induction (isdecrelhzeq (i - j + j) i) as [T | F].
- apply maponpaths. apply isasethz.
- apply fromempty. apply F. apply (hzrminusplus i j).
- apply maponpaths. apply isasethz.
- apply fromempty. apply F. apply (hzrminusplus i j).
Lemma hzeqpii {i : hz} : i - 1 != i.
Show proof.
Lemma isdecrelhzeqpii (i : hz) :
isdecrelhzeq (i - 1) i = ii2 (fun (e : hzeq (i - 1) i) => hzeqpii e).
Show proof.
induction (isdecrelhzeq (i - 1) i) as [e | n].
- apply fromempty. apply (hzeqpii e).
- apply maponpaths. apply funextfun. intros e.
apply fromempty. apply n. apply e.
- apply fromempty. apply (hzeqpii e).
- apply maponpaths. apply funextfun. intros e.
apply fromempty. apply n. apply e.
Local Transparent hz isdecrelhzeq iscommringops.
hz is an archimedean ring
Local Open Scope hz_scope .
Lemma isarchhz : isarchring (X := hz) hzgth.
Show proof.
simple refine (isarchrigtoring _ _ _ _ _ _).
- reflexivity.
- intros n m.
apply istransnatgth.
- apply isarchrig_setquot_aux.
+ split.
* apply natgthandpluslinv.
* apply natgthandplusrinv.
+ apply isarchnat.
- reflexivity.
- intros n m.
apply istransnatgth.
- apply isarchrig_setquot_aux.
+ split.
* apply natgthandpluslinv.
* apply natgthandplusrinv.
+ apply isarchnat.
Lemma isarchhz_one :
∏ x : hz, hzgth x 0 → ∃ n : nat, hzgth (nattohz n * x) 1.
Show proof.
intros x Hx.
generalize (isarchring_1 _ isarchhz x Hx).
apply hinhfun.
intros n.
exists (pr1 n).
rewrite <- nattorig_nattohz.
exact (pr2 n).
generalize (isarchring_1 _ isarchhz x Hx).
apply hinhfun.
intros n.
exists (pr1 n).
rewrite <- nattorig_nattohz.
exact (pr2 n).
Lemma isarchhz_gt :
∏ x : hz, ∃ n : nat, hzgth (nattohz n) x.
Show proof.
intros x.
generalize (isarchring_2 _ isarchhz x).
apply hinhfun.
intros n.
exists (pr1 n).
rewrite <- nattorig_nattohz.
exact (pr2 n).
generalize (isarchring_2 _ isarchhz x).
apply hinhfun.
intros n.
exists (pr1 n).
rewrite <- nattorig_nattohz.
exact (pr2 n).
hz -> abgr, 1 ↦ x, n ↦ x + x + ... + x (n times), hz_abmonoid_monoidfun
Definition nat_to_monoid_fun {X : monoid} (x : X) : natset -> X.
Show proof.
Lemma nat_to_monoid_fun_unel {X : monoid} (x : X) : nat_to_monoid_fun x O = (unel X).
Show proof.
Lemma nat_to_monoid_fun_S {X : abmonoid} (x : X) (n : nat) :
nat_to_monoid_fun x (S n) = (nat_to_monoid_fun x n * x)%multmonoid.
Show proof.
induction n as [ | n IHn].
- exact (commax X x (unel X)).
- cbn. rewrite (assocax X). use two_arg_paths.
+ use idpath.
+ exact (commax X x _).
- exact (commax X x (unel X)).
- cbn. rewrite (assocax X). use two_arg_paths.
+ use idpath.
+ exact (commax X x _).
Lemma nat_to_abmonoid_fun_plus {X : monoid} (x : X) (n m : nat) :
nat_to_monoid_fun x (n + m)%nat = @op X (nat_to_monoid_fun x n) (nat_to_monoid_fun x m).
Show proof.
revert m. induction n as [ | n IHn].
- intros m. rewrite (lunax X). use idpath.
- intros m. cbn. rewrite (assocax X). use two_arg_paths.
+ use idpath.
+ exact (IHn m).
- intros m. rewrite (lunax X). use idpath.
- intros m. cbn. rewrite (assocax X). use two_arg_paths.
+ use idpath.
+ exact (IHn m).
Definition nat_nat_to_monoid_fun {X : gr} (x : X) : natset × natset -> X.
Show proof.
intros n.
exact (@op X (nat_to_monoid_fun x (dirprod_pr1 n))
(nat_to_monoid_fun (grinv X x) (dirprod_pr2 n))).
exact (@op X (nat_to_monoid_fun x (dirprod_pr1 n))
(nat_to_monoid_fun (grinv X x) (dirprod_pr2 n))).
Lemma nat_to_monoid_unel' {X : abgr} (x : X) (n : nat) :
((nat_to_monoid_fun x n) * (nat_to_monoid_fun (grinv X x) n))%multmonoid = (unel X).
Show proof.
induction n as [ | n IHn].
- use (runax X).
- Opaque nat_to_monoid_fun. cbn in *.
rewrite (@nat_to_monoid_fun_S X x). rewrite (@nat_to_monoid_fun_S X (grinv X x)).
rewrite (commax X _ x). rewrite (assocax X).
rewrite <- (assocax X (@nat_to_monoid_fun X x n)).
use (pathscomp0 (maponpaths (λ xx : pr1 X, (x * (xx * (grinv X x))))%multmonoid IHn)).
clear IHn. use (pathscomp0 _ (grrinvax X x)).
use two_arg_paths.
+ use idpath.
+ use (lunax X).
Transparent nat_to_monoid_fun.- use (runax X).
- Opaque nat_to_monoid_fun. cbn in *.
rewrite (@nat_to_monoid_fun_S X x). rewrite (@nat_to_monoid_fun_S X (grinv X x)).
rewrite (commax X _ x). rewrite (assocax X).
rewrite <- (assocax X (@nat_to_monoid_fun X x n)).
use (pathscomp0 (maponpaths (λ xx : pr1 X, (x * (xx * (grinv X x))))%multmonoid IHn)).
clear IHn. use (pathscomp0 _ (grrinvax X x)).
use two_arg_paths.
+ use idpath.
+ use (lunax X).
Lemma nat_nat_to_monoid1 {X : gr} (x : X) {n1 n2 m2 : nat} (e : n2 = m2) :
nat_nat_to_monoid_fun x (make_dirprod n1 n2) = nat_nat_to_monoid_fun x (make_dirprod n1 m2).
Show proof.
Lemma nat_nat_to_monoid2 {X : gr} (x : X) {n1 m1 n2 : nat} (e : n1 = m1) :
nat_nat_to_monoid_fun x (make_dirprod n1 n2) = nat_nat_to_monoid_fun x (make_dirprod m1 n2).
Show proof.
Definition nataddabmonoid_nataddabmonoid_to_monoid_fun {X : gr} (x : X) :
abmonoiddirprod nataddabmonoid nataddabmonoid -> X := nat_nat_to_monoid_fun x.
Opaque nat_to_monoid_fun.
Lemma nat_nat_monoid_fun_isbinopfun {X : abgr} (x : X) :
isbinopfun (nataddabmonoid_nataddabmonoid_to_monoid_fun x).
Show proof.
use make_isbinopfun. intros n m. induction n as [n1 n2]. induction m as [m1 m2]. cbn.
unfold nataddabmonoid_nataddabmonoid_to_monoid_fun. unfold nat_nat_to_monoid_fun. cbn.
rewrite nat_to_abmonoid_fun_plus. rewrite nat_to_abmonoid_fun_plus.
rewrite (assocax X). rewrite (assocax X).
use two_arg_paths.
- use idpath.
- rewrite <- (assocax X). rewrite (commax X (nat_to_monoid_fun (grinv X x) n2) _).
rewrite (assocax X). rewrite (assocax X).
use two_arg_paths.
+ use idpath.
+ use (commax X).
Transparent nat_to_monoid_fun.unfold nataddabmonoid_nataddabmonoid_to_monoid_fun. unfold nat_nat_to_monoid_fun. cbn.
rewrite nat_to_abmonoid_fun_plus. rewrite nat_to_abmonoid_fun_plus.
rewrite (assocax X). rewrite (assocax X).
use two_arg_paths.
- use idpath.
- rewrite <- (assocax X). rewrite (commax X (nat_to_monoid_fun (grinv X x) n2) _).
rewrite (assocax X). rewrite (assocax X).
use two_arg_paths.
+ use idpath.
+ use (commax X).
Lemma nat_nat_to_monoid_plus1 {X : abgr} (x : X) {n1 m1 m2: nat} (e : m2 = (m1 + n1)%nat) :
nat_to_monoid_fun (grinv X x) n1 =
(nat_to_monoid_fun x m1 * nat_to_monoid_fun (grinv X x) m2)%multmonoid.
Show proof.
rewrite e. clear e. rewrite nat_to_abmonoid_fun_plus.
rewrite <- (assocax X). use pathsinv0.
use (pathscomp0 (maponpaths (λ xx : X, (xx * (nat_to_monoid_fun (grinv X x) n1))%multmonoid)
(nat_to_monoid_unel' x m1))).
use (lunax X).
rewrite <- (assocax X). use pathsinv0.
use (pathscomp0 (maponpaths (λ xx : X, (xx * (nat_to_monoid_fun (grinv X x) n1))%multmonoid)
(nat_to_monoid_unel' x m1))).
use (lunax X).
Lemma nat_nat_prod_abmonoid_fun_unel {X : abgr} (x : X) :
(nataddabmonoid_nataddabmonoid_to_monoid_fun x)
(unel (abmonoiddirprod nataddabmonoid nataddabmonoid)) = (unel X).
Show proof.
Definition nat_nat_prod_abmonoid_monoidfun {X : abgr} (x : X) :
monoidfun (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) X.
Show proof.
use monoidfunconstr.
- exact (nataddabmonoid_nataddabmonoid_to_monoid_fun x).
- use make_ismonoidfun.
+ exact (nat_nat_monoid_fun_isbinopfun x).
+ exact (nat_nat_prod_abmonoid_fun_unel x).
- exact (nataddabmonoid_nataddabmonoid_to_monoid_fun x).
- use make_ismonoidfun.
+ exact (nat_nat_monoid_fun_isbinopfun x).
+ exact (nat_nat_prod_abmonoid_fun_unel x).
Lemma hz_abmonoid_ismonoidfun :
@ismonoidfun
(abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig))
hzaddabgr (@setquotpr (abmonoiddirprod (rigaddabmonoid natcommrig)
(rigaddabmonoid natcommrig))
(binopeqrelabgrdiff (rigaddabmonoid natcommrig))).
Show proof.
Definition hz_abmonoid_monoidfun :
monoidfun (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) hzaddabgr.
Show proof.
Definition nat_nat_fun_unel {X : abgr} (x : X) (n : nat) :
nat_nat_to_monoid_fun x (make_dirprod n n) = unel X.
Show proof.
Opaque nat_to_monoid_fun.
Definition nat_nat_fun_ind {X : abgr} (x : X) (n m : nat) :
nat_nat_to_monoid_fun x (make_dirprod (n + m)%nat m) = nat_nat_to_monoid_fun x (make_dirprod n O).
Show proof.
use (pathscomp0 (nat_nat_monoid_fun_isbinopfun x (make_dirprod n O) (make_dirprod m m))).
unfold nataddabmonoid_nataddabmonoid_to_monoid_fun.
rewrite (nat_nat_fun_unel x m). rewrite (runax X). use idpath.
Transparent nat_to_monoid_fun.unfold nataddabmonoid_nataddabmonoid_to_monoid_fun.
rewrite (nat_nat_fun_unel x m). rewrite (runax X). use idpath.
Opaque nat_to_monoid_fun.
Definition nat_nat_fun_ind2 {X : abgr} (x : X) (n1 n2 m k : nat) :
nat_nat_to_monoid_fun x (make_dirprod n1 m) = nat_nat_to_monoid_fun x (make_dirprod n2 k) ->
nat_nat_to_monoid_fun x (make_dirprod n1 (S m)) = nat_nat_to_monoid_fun x (make_dirprod n2 (S k)).
Show proof.
intros H.
unfold nat_nat_to_monoid_fun in *. cbn in *.
rewrite (@nat_to_monoid_fun_S X (grinv X x)).
rewrite (@nat_to_monoid_fun_S X (grinv X x)).
rewrite <- (assocax X). rewrite <- (assocax X).
use two_arg_paths.
- exact H.
- use idpath.
Transparent nat_to_monoid_fun.unfold nat_nat_to_monoid_fun in *. cbn in *.
rewrite (@nat_to_monoid_fun_S X (grinv X x)).
rewrite (@nat_to_monoid_fun_S X (grinv X x)).
rewrite <- (assocax X). rewrite <- (assocax X).
use two_arg_paths.
- exact H.
- use idpath.
Opaque nat_to_monoid_fun.
Definition abgr_precategory_integer_fun_iscomprelfun {X : abgr} (x : X) :
iscomprelfun (binopeqrelabgrdiff (rigaddabmonoid natcommrig))
(nat_nat_prod_abmonoid_monoidfun x).
Show proof.
intros x1. induction x1 as [x1 e1].
unfold nat_nat_prod_abmonoid_monoidfun. cbn.
unfold nataddabmonoid_nataddabmonoid_to_monoid_fun.
unfold nat_nat_to_monoid_fun. cbn.
induction x1 as [ | x1 IHx1].
- intros x2 H. use (squash_to_prop H (setproperty X _ _)). intros H'. cbn in H'.
induction H' as [H1 H2]. clear H. induction x2 as [x2 e2].
apply natplusrcan in H2. rewrite nat_to_monoid_fun_unel. rewrite (lunax X). cbn. cbn in H2.
exact (nat_nat_to_monoid_plus1 x H2).
- intros x2 H. use (squash_to_prop H (setproperty X _ _)). intros H'. cbn in H'.
induction H' as [H1 H2]. clear H. induction x2 as [x2 e2]. cbn in H2. cbn.
use (pathscomp0
(maponpaths (λ xx : X, (xx * (nat_to_monoid_fun (grinv X x) e1))%multmonoid)
(@nat_to_monoid_fun_S X x x1))).
rewrite (commax X _ x). rewrite (assocax X). cbn.
assert (HH : ishinh_UU(∑ x0 : nat, (x1 + (S e2) + x0)%nat = (x2 + e1 + x0)%nat)).
{
use hinhpr. use tpair.
- exact O.
- cbn. rewrite natplusr0. rewrite natplusr0. cbn.
rewrite natplusassoc in H2.
rewrite plus_n_Sm in H2. rewrite plus_n_Sm in H2.
rewrite natplusnsm in H2. rewrite <- natplusassoc in H2.
apply natplusrcan in H2. exact H2.
}
set (tmp := IHx1 (make_dirprod x2 (S e2)) HH). cbn in tmp.
use (pathscomp0 (maponpaths (λ xx : X, (x * xx)%multmonoid) tmp)).
clear tmp. clear HH. clear H2. clear IHx1. rewrite (commax X x). rewrite (assocax X).
use two_arg_paths.
+ use idpath.
+ use (pathscomp0
(maponpaths (λ xx : X, (xx * x)%multmonoid)
(@nat_to_monoid_fun_S X (grinv X x) e2))).
rewrite (assocax X). rewrite (grlinvax X x). use (runax X).
Transparent nat_to_monoid_fun.unfold nat_nat_prod_abmonoid_monoidfun. cbn.
unfold nataddabmonoid_nataddabmonoid_to_monoid_fun.
unfold nat_nat_to_monoid_fun. cbn.
induction x1 as [ | x1 IHx1].
- intros x2 H. use (squash_to_prop H (setproperty X _ _)). intros H'. cbn in H'.
induction H' as [H1 H2]. clear H. induction x2 as [x2 e2].
apply natplusrcan in H2. rewrite nat_to_monoid_fun_unel. rewrite (lunax X). cbn. cbn in H2.
exact (nat_nat_to_monoid_plus1 x H2).
- intros x2 H. use (squash_to_prop H (setproperty X _ _)). intros H'. cbn in H'.
induction H' as [H1 H2]. clear H. induction x2 as [x2 e2]. cbn in H2. cbn.
use (pathscomp0
(maponpaths (λ xx : X, (xx * (nat_to_monoid_fun (grinv X x) e1))%multmonoid)
(@nat_to_monoid_fun_S X x x1))).
rewrite (commax X _ x). rewrite (assocax X). cbn.
assert (HH : ishinh_UU(∑ x0 : nat, (x1 + (S e2) + x0)%nat = (x2 + e1 + x0)%nat)).
{
use hinhpr. use tpair.
- exact O.
- cbn. rewrite natplusr0. rewrite natplusr0. cbn.
rewrite natplusassoc in H2.
rewrite plus_n_Sm in H2. rewrite plus_n_Sm in H2.
rewrite natplusnsm in H2. rewrite <- natplusassoc in H2.
apply natplusrcan in H2. exact H2.
}
set (tmp := IHx1 (make_dirprod x2 (S e2)) HH). cbn in tmp.
use (pathscomp0 (maponpaths (λ xx : X, (x * xx)%multmonoid) tmp)).
clear tmp. clear HH. clear H2. clear IHx1. rewrite (commax X x). rewrite (assocax X).
use two_arg_paths.
+ use idpath.
+ use (pathscomp0
(maponpaths (λ xx : X, (xx * x)%multmonoid)
(@nat_to_monoid_fun_S X (grinv X x) e2))).
rewrite (assocax X). rewrite (grlinvax X x). use (runax X).
Construction of tha map \mathbb{Z} --> A, 1 ↦ x
Definition hz_abgr_fun {X : abgr} (x : X) : hzaddabgr -> X.
Show proof.
Show proof.
use setquotuniv.
- exact (nat_nat_prod_abmonoid_monoidfun x).
- exact (abgr_precategory_integer_fun_iscomprelfun x).
- exact (nat_nat_prod_abmonoid_monoidfun x).
- exact (abgr_precategory_integer_fun_iscomprelfun x).
Hide ismonoidfun behind Qed.
Definition hz_abgr_fun_ismonoidfun {X : abgr} (x : X) : ismonoidfun (hz_abgr_fun x).
Show proof.
Show proof.
use make_ismonoidfun.
- use isbinopfun_twooutof3b.
+ use (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)).
+ use (hz_abmonoid_monoidfun).
+ use issurjsetquotpr.
+ use binopfunisbinopfun.
+ use binopfunisbinopfun.
- use (runax X).
- use isbinopfun_twooutof3b.
+ use (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)).
+ use (hz_abmonoid_monoidfun).
+ use issurjsetquotpr.
+ use binopfunisbinopfun.
+ use binopfunisbinopfun.
- use (runax X).
Construction of the monoidfun \mathbb{Z} --> A, 1 ↦ x
Commutativity of the following diagram
nat × nat --- nat_nat_prod_abmonoid_monoidfun ---> X
hz_abgr_fun_monoidfun | ||
hz -------- hz_abmonoid_monoidfun -------------> X
Lemma abgr_natnat_hz_X_comm {X : abgr} (x : X) :
monoidfuncomp hz_abmonoid_monoidfun (hz_abgr_fun_monoidfun x) =
nat_nat_prod_abmonoid_monoidfun x.
Show proof.
Opaque nat_to_monoid_fun.
Lemma monoidfun_nat_to_monoid_fun {X Y : abgr} (f : monoidfun X Y) (x : X) (n : nat) :
pr1 f (nat_to_monoid_fun x n) = nat_to_monoid_fun (f x) n.
Show proof.
monoidfuncomp hz_abmonoid_monoidfun (hz_abgr_fun_monoidfun x) =
nat_nat_prod_abmonoid_monoidfun x.
Show proof.
Opaque nat_to_monoid_fun.
Lemma monoidfun_nat_to_monoid_fun {X Y : abgr} (f : monoidfun X Y) (x : X) (n : nat) :
pr1 f (nat_to_monoid_fun x n) = nat_to_monoid_fun (f x) n.
Show proof.
induction n as [ | n IHn].
- use monoidfununel.
- use (pathscomp0 (maponpaths (pr1 f) (@nat_to_monoid_fun_S X x n))).
use (pathscomp0 (binopfunisbinopfun f _ _)).
use (pathscomp0 _ (! (@nat_to_monoid_fun_S Y (f x) n))).
use two_arg_paths.
+ exact IHn.
+ use idpath.
Transparent nat_to_monoid_fun.- use monoidfununel.
- use (pathscomp0 (maponpaths (pr1 f) (@nat_to_monoid_fun_S X x n))).
use (pathscomp0 (binopfunisbinopfun f _ _)).
use (pathscomp0 _ (! (@nat_to_monoid_fun_S Y (f x) n))).
use two_arg_paths.
+ exact IHn.
+ use idpath.
Some more facts about integers added by D. Grayson
Definition ℤ := hzaddabgr.
Definition toℤ (n:nat) : ℤ := nattohz n.
Definition toℤneg (n:nat) : ℤ := natnattohz O n.
Definition zero := toℤ 0.
Definition one := toℤ 1.
Definition hzabsvalnat n : hzabsval (natnattohz n 0) = n. Show proof.
intros. unfold hzabsval. unfold setquotuniv. simpl.
unfold hzabsvalint. simpl. destruct (natgthorleh n 0).
{ apply natminuseqn. } { exact (! (natleh0tois0 h)). }
unfold hzabsvalint. simpl. destruct (natgthorleh n 0).
{ apply natminuseqn. } { exact (! (natleh0tois0 h)). }
Lemma hzsign_natnattohz m n : - natnattohz m n = natnattohz n m. Show proof.
reflexivity.
Lemma hzsign_nattohz m : - nattohz m = natnattohz 0 m. Show proof.
reflexivity.
Lemma hzsign_hzsign (i:hz) : - - i = i.
Show proof.
Definition hz_normal_form (i:ℤ) :=
coprod (∑ n, natnattohz n 0 = i)
(∑ n, natnattohz 0 (S n) = i).
Definition hznf_pos n := _,, inl (n,,idpath _) : total2 hz_normal_form.
Definition hznf_neg n := _,, inr (n,,idpath _) : total2 hz_normal_form.
Definition hznf_zero := hznf_pos 0.
Definition hznf_neg_one := hznf_neg 0.
Definition hz_to_normal_form (i:ℤ) : hz_normal_form i.
Show proof.
intros. destruct (hzlthorgeh i 0) as [r|s].
{ apply inr. assert (a := hzabsvallth0 r). assert (b := hzlthtoneq _ _ r).
assert (c := hzabsvalneq0 b). assert (d := natneq0togth0 _ c).
assert (f := natgthtogehsn _ _ d). assert (g := minusplusnmm _ _ f).
rewrite natpluscomm in g. simpl in g. exists (hzabsval i - 1)%nat.
rewrite g. apply hzinvmaponpathsminus. exact a. }
{ apply inl. exists (hzabsval i). exact (hzabsvalgeh0 s). }
{ apply inr. assert (a := hzabsvallth0 r). assert (b := hzlthtoneq _ _ r).
assert (c := hzabsvalneq0 b). assert (d := natneq0togth0 _ c).
assert (f := natgthtogehsn _ _ d). assert (g := minusplusnmm _ _ f).
rewrite natpluscomm in g. simpl in g. exists (hzabsval i - 1)%nat.
rewrite g. apply hzinvmaponpathsminus. exact a. }
{ apply inl. exists (hzabsval i). exact (hzabsvalgeh0 s). }
Lemma nattohz_inj {m n} : nattohz m = nattohz n -> m = n.
Show proof.
Lemma hzdichot {m n} : neg (nattohz m = - nattohz (S n)).
Show proof.
intros. intro e. assert (d := maponpaths hzsign e); clear e.
rewrite hzsign_hzsign in d.
assert( f := maponpaths (λ i, nattohz m + i) d); simpl in f; clear d.
change (nattohz m + - nattohz m) with (nattohz m - nattohz m) in f.
rewrite hzrminus in f. change (0 = nattohz (m + S n)) in f.
assert (g := nattohz_inj f); clear f. rewrite natpluscomm in g.
exact (negpaths0sx _ g).
rewrite hzsign_hzsign in d.
assert( f := maponpaths (λ i, nattohz m + i) d); simpl in f; clear d.
change (nattohz m + - nattohz m) with (nattohz m - nattohz m) in f.
rewrite hzrminus in f. change (0 = nattohz (m + S n)) in f.
assert (g := nattohz_inj f); clear f. rewrite natpluscomm in g.
exact (negpaths0sx _ g).
Definition negpos' : isweq (@pr1 _ hz_normal_form).
Show proof.
apply isweqpr1; intro i.
exists (hz_to_normal_form i).
generalize (hz_to_normal_form i) as s.
intros [[m p]|[m p]] [[n q]|[n q]].
{ apply (maponpaths (@ii1 (∑ n, natnattohz n 0 = i)
(∑ n, natnattohz 0 (S n) = i))).
apply (proofirrelevance _ (isinclnattohz i)). }
{ apply fromempty. assert (r := p@!q); clear p q. apply (hzdichot r). }
{ apply fromempty. assert (r := q@!p); clear p q. apply (hzdichot r). }
{ apply (maponpaths (@ii2 (∑ n, natnattohz n 0 = i)
(∑ n, natnattohz 0 (S n) = i))).
assert (p' := maponpaths hzsign p). assert (q' := maponpaths hzsign q).
change (- natnattohz O (S m)) with (nattohz (S m)) in p'.
change (- natnattohz O (S n)) with (nattohz (S n)) in q'.
assert (c := proofirrelevance _ (isinclnattohz (-i)) (S m,,p') (S n,,q')).
assert (d := maponpaths pr1 c); simpl in d.
assert (e := invmaponpathsS _ _ d); clear d.
apply subtypePath.
- intro; apply setproperty.
- exact (!e). }
exists (hz_to_normal_form i).
generalize (hz_to_normal_form i) as s.
intros [[m p]|[m p]] [[n q]|[n q]].
{ apply (maponpaths (@ii1 (∑ n, natnattohz n 0 = i)
(∑ n, natnattohz 0 (S n) = i))).
apply (proofirrelevance _ (isinclnattohz i)). }
{ apply fromempty. assert (r := p@!q); clear p q. apply (hzdichot r). }
{ apply fromempty. assert (r := q@!p); clear p q. apply (hzdichot r). }
{ apply (maponpaths (@ii2 (∑ n, natnattohz n 0 = i)
(∑ n, natnattohz 0 (S n) = i))).
assert (p' := maponpaths hzsign p). assert (q' := maponpaths hzsign q).
change (- natnattohz O (S m)) with (nattohz (S m)) in p'.
change (- natnattohz O (S n)) with (nattohz (S n)) in q'.
assert (c := proofirrelevance _ (isinclnattohz (-i)) (S m,,p') (S n,,q')).
assert (d := maponpaths pr1 c); simpl in d.
assert (e := invmaponpathsS _ _ d); clear d.
apply subtypePath.
- intro; apply setproperty.
- exact (!e). }
Definition negpos_weq := make_weq _ negpos' : weq (total2 hz_normal_form) ℤ.
Definition negpos : weq (coprod nat nat) ℤ. Show proof.
simple refine (make_weq _ (isweq_iso _ _ _ _)).
{ intros [n'|n].
{ exact (natnattohz 0 (S n')). } { exact (natnattohz n 0). } }
{ intro i. destruct (hz_to_normal_form i) as [[n p]|[m q]].
{ exact (inr n). } { exact (inl m). } }
{ intros [n'|n].
{ simpl. rewrite natminuseqn. reflexivity. }
{ simpl. rewrite hzabsvalnat. reflexivity. } }
{ simpl. intro i.
destruct (hz_to_normal_form i) as [[n p]|[m q]].
{ exact p. } { exact q. } }
{ intros [n'|n].
{ exact (natnattohz 0 (S n')). } { exact (natnattohz n 0). } }
{ intro i. destruct (hz_to_normal_form i) as [[n p]|[m q]].
{ exact (inr n). } { exact (inl m). } }
{ intros [n'|n].
{ simpl. rewrite natminuseqn. reflexivity. }
{ simpl. rewrite hzabsvalnat. reflexivity. } }
{ simpl. intro i.
destruct (hz_to_normal_form i) as [[n p]|[m q]].
{ exact p. } { exact q. } }
Lemma hzminusplus (x y:hz) : -(x+y) = (-x) + (-y). Show proof.
intros. apply (hzplusrcan _ _ (x+y)). rewrite hzlminus.
rewrite (hzpluscomm (-x)). rewrite (hzplusassoc (-y)).
rewrite <- (hzplusassoc (-x)). rewrite hzlminus. rewrite hzplusl0.
rewrite hzlminus. reflexivity.
rewrite (hzpluscomm (-x)). rewrite (hzplusassoc (-y)).
rewrite <- (hzplusassoc (-x)). rewrite hzlminus. rewrite hzplusl0.
rewrite hzlminus. reflexivity.
Definition loop_power {Y} {y:Y} (l:y = y) (n:ℤ) : y = y.
Show proof.
intros. assert (m := loop_power_nat l (hzabsval n)).
destruct (hzlthorgeh n 0%hz). { exact (!m). } { exact m. }
destruct (hzlthorgeh n 0%hz). { exact (!m). } { exact m. }