Library UniMath.PAdics.lemmas
*Fixing notation, terminology and basic lemmas
By Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren
made compatible with the current UniMath library again by Benedikt Ahrens in 2014
and by Ralph Matthes in 2017
Imports
Require Export UniMath.Tactics.EnsureStructuredProofs.
Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.Algebra.Domains_and_Fields.
Require Import UniMath.NumberSystems.Integers.
Require Import UniMath.Algebra.Monoids.
Unset Kernel Term Sharing.
Arguments tpair [ T P ].
Definition neq ( X : UU ) : hrel X :=
fun x y : X => make_hProp (neg (x = y)) (isapropneg (x = y)).
Lemma minus0r ( n : nat ) : sub n 0 = n.
Show proof.
Lemma minusnn0 ( n : nat ) : sub n n = 0%nat.
Show proof.
Lemma minussn1 ( n : nat ) : sub ( S n ) 1 = n.
Show proof.
Lemma minussn1non0 ( n : nat ) ( p : natlth 0 n ) : S ( sub n 1 ) = n.
Show proof.
revert p. destruct n.
- intro p. apply fromempty. exact (isirreflnatlth 0%nat p ).
- intro. apply maponpaths. apply minus0r.
- intro p. apply fromempty. exact (isirreflnatlth 0%nat p ).
- intro. apply maponpaths. apply minus0r.
Lemma minusleh ( n m : nat ) : natleh ( sub n m ) n.
Show proof.
revert m. induction n.
- intros m. apply isreflnatleh.
- intros m. destruct m.
+ apply isreflnatleh.
+ apply ( istransnatleh (IHn m)).
apply natlthtoleh.
apply natlthnsn.
- intros m. apply isreflnatleh.
- intros m. destruct m.
+ apply isreflnatleh.
+ apply ( istransnatleh (IHn m)).
apply natlthtoleh.
apply natlthnsn.
Lemma minus1leh { n m : nat } ( p : natlth 0 n ) ( q : natlth 0 m ) ( r : natleh n m ) : natleh ( sub n 1 ) ( sub m 1 ).
Show proof.
revert m p q r. destruct n.
- auto.
- intros m p q r. destruct m.
+ apply fromempty. exact (isirreflnatlth 0%nat q ).
+ assert ( natleh n m ) as a. { apply r. }
assert ( natleh ( sub n 0%nat ) m ) as a0.
{ exact (transportf ( fun x : nat => natleh x m ) ( pathsinv0 ( minus0r n ) ) a). }
exact ( transportf ( fun x : nat => natleh ( sub n 0 ) x ) (pathsinv0 ( minus0r m ) ) a0 ).
- auto.
- intros m p q r. destruct m.
+ apply fromempty. exact (isirreflnatlth 0%nat q ).
+ assert ( natleh n m ) as a. { apply r. }
assert ( natleh ( sub n 0%nat ) m ) as a0.
{ exact (transportf ( fun x : nat => natleh x m ) ( pathsinv0 ( minus0r n ) ) a). }
exact ( transportf ( fun x : nat => natleh ( sub n 0 ) x ) (pathsinv0 ( minus0r m ) ) a0 ).
Lemma minuslth ( n m : nat ) ( p : natlth 0 n ) ( q : natlth 0 m ) :
natlth ( sub n m ) n.
Show proof.
revert m p q. destruct n.
- auto.
- intros m p q. destruct m.
+ apply fromempty. exact ( isirreflnatlth 0%nat q).
+ apply ( natlehlthtrans _ n _ ).
* apply ( minusleh n m ).
* apply natlthnsn.
- auto.
- intros m p q. destruct m.
+ apply fromempty. exact ( isirreflnatlth 0%nat q).
+ apply ( natlehlthtrans _ n _ ).
* apply ( minusleh n m ).
* apply natlthnsn.
Lemma natlthsntoleh ( n m : nat ) : natlth m ( S n ) -> natleh m n.
Show proof.
revert m. induction n.
- intros m p. destruct m.
+ apply isreflnatleh.
+ assert ( natlth m 0 ) as q by apply p.
apply fromempty. exact ( negnatgth0n m q ).
- intros m p. destruct m.
+ apply natleh0n.
+ apply ( IHn m ). assumption.
- intros m p. destruct m.
+ apply isreflnatleh.
+ assert ( natlth m 0 ) as q by apply p.
apply fromempty. exact ( negnatgth0n m q ).
- intros m p. destruct m.
+ apply natleh0n.
+ apply ( IHn m ). assumption.
Lemma natlthminus0 { n m : nat } ( p : natlth m n ) :
natlth 0 ( sub n m ).
Show proof.
revert m p. induction n.
- intros m p. apply fromempty. exact ( negnatlthn0 m p ).
- intros m p. destruct m.
+ auto.
+ apply IHn. apply p.
- intros m p. apply fromempty. exact ( negnatlthn0 m p ).
- intros m p. destruct m.
+ auto.
+ apply IHn. apply p.
Lemma natlthsnminussmsn ( n m : nat ) ( p : natlth m n ) :
natlth ( sub ( S n ) ( S m ) ) ( S n ).
Show proof.
revert m p. induction n.
- intros m p. apply fromempty. apply (negnatlthn0 m p).
- intros m p. destruct m.
+ assert ( sub ( 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.
- intros m p. apply fromempty. apply (negnatlthn0 m p).
- intros m p. destruct m.
+ assert ( sub ( 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.
Lemma natlehsnminussmsn ( n m : nat ) ( p : natleh m n ) :
natleh (sub ( S n ) ( S m ) ) ( S n ).
Show proof.
revert m p. induction n.
- intros m p. apply negnatgthtoleh. intro X. apply nopathsfalsetotrue. assumption.
- intros m p. destruct m.
+ apply natlthtoleh. apply natlthnsn.
+ apply ( istransnatleh( m := S n ) ).
* apply IHn. assumption.
* apply natlthtoleh. apply natlthnsn.
- intros m p. apply negnatgthtoleh. intro X. apply nopathsfalsetotrue. assumption.
- intros m p. destruct m.
+ apply natlthtoleh. apply natlthnsn.
+ apply ( istransnatleh( m := S n ) ).
* apply IHn. assumption.
* apply natlthtoleh. apply natlthnsn.
Lemma pathssminus ( n m : nat ) ( p : natlth m ( S n ) ) :
S ( sub n m ) = sub ( S n ) m.
Show proof.
revert m p. induction n.
- intros m p. destruct m.
+ auto.
+ apply fromempty.
apply nopathstruetofalse. apply pathsinv0. assumption.
- intros m p. destruct m.
+ auto.
+ apply IHn. apply p.
- intros m p. destruct m.
+ auto.
+ apply fromempty.
apply nopathstruetofalse. apply pathsinv0. assumption.
- intros m p. destruct m.
+ auto.
+ apply IHn. apply p.
Lemma natlehsminus ( n m : nat ) :
natleh ( sub ( S n ) m ) ( S (sub n m ) ).
Show proof.
revert m. induction n.
- intros m. apply negnatgthtoleh. intro X. apply nopathstruetofalse.
apply pathsinv0. destruct m.
+ assumption.
+ assumption.
- intros m. destruct m.
+ apply isreflnatleh.
+ apply IHn.
- intros m. apply negnatgthtoleh. intro X. apply nopathstruetofalse.
apply pathsinv0. destruct m.
+ assumption.
+ assumption.
- intros m. destruct m.
+ apply isreflnatleh.
+ apply IHn.
Lemma natlthssminus { n m l : nat } ( p : natlth m ( S n ) )
( q : natlth l ( S ( sub ( S n ) m ) ) ) : natlth l ( S ( S n ) ).
Show proof.
apply ( natlthlehtrans _ ( S ( sub ( S n ) m ) ) ).
- assumption.
- destruct m.
+ apply isreflnatleh.
+ apply natlthtoleh. apply natlthsnminussmsn. assumption.
- assumption.
- destruct m.
+ apply isreflnatleh.
+ apply natlthtoleh. apply natlthsnminussmsn. assumption.
Lemma natdoubleminus { n k l : nat } ( p : natleh k n ) ( q : natleh l k ) :
sub n k = sub ( sub n l ) ( sub k l ).
Show proof.
revert k l p q. induction n.
- auto.
- intros k l p q. destruct k.
+ destruct l.
* auto.
* apply fromempty. exact ( negnatlehsn0 l q ).
+ destruct l.
* auto.
* apply ( IHn k l ); assumption.
- auto.
- intros k l p q. destruct k.
+ destruct l.
* auto.
* apply fromempty. exact ( negnatlehsn0 l q ).
+ destruct l.
* auto.
* apply ( IHn k l ); assumption.
Lemma minusnleh1 ( n m : nat ) ( p : natlth m n ) : natleh m ( sub n 1 ).
Show proof.
revert m p. destruct n.
- intros m p. apply fromempty. exact (negnatlthn0 m p ).
- intros m p. destruct m.
+ apply natleh0n.
+ apply natlthsntoleh.
change ( sub ( S n ) 1 ) with ( sub n 0 ).
rewrite minus0r. assumption.
- intros m p. apply fromempty. exact (negnatlthn0 m p ).
- intros m p. destruct m.
+ apply natleh0n.
+ apply natlthsntoleh.
change ( sub ( S n ) 1 ) with ( sub n 0 ).
rewrite minus0r. assumption.
Lemma doubleminuslehpaths ( n m : nat ) ( p : natleh m n ) :
sub n (sub n m ) = m.
Show proof.
revert m p. induction n.
- intros m p. destruct ( natlehchoice m 0 p ) as [ h | k ].
+ apply fromempty. apply negnatlthn0 with ( n := m ). assumption.
+ simpl. apply pathsinv0. assumption.
- intros. destruct m.
+ simpl. apply minusnn0.
+ change ( sub ( S n ) (sub 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.
- intros m p. destruct ( natlehchoice m 0 p ) as [ h | k ].
+ apply fromempty. apply negnatlthn0 with ( n := m ). assumption.
+ simpl. apply pathsinv0. assumption.
- intros. destruct m.
+ simpl. apply minusnn0.
+ change ( sub ( S n ) (sub 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.
Lemma boolnegtrueimplfalse ( v : bool ) ( p : neg ( v = true ) ) : v = false.
Show proof.
Definition natcoface ( i : nat ) : nat -> nat.
Show proof.
Lemma natcofaceleh ( i n upper : nat ) ( p : natleh n upper ) :
natleh ( natcoface i n ) ( S upper ).
Show proof.
intros.
unfold natcoface.
destruct ( natgtb i n ).
- apply natlthtoleh. apply (natlehlthtrans _ upper ).
+ assumption.
+ apply natlthnsn.
- apply p.
unfold natcoface.
destruct ( natgtb i n ).
- apply natlthtoleh. apply (natlehlthtrans _ upper ).
+ assumption.
+ apply natlthnsn.
- apply p.
Lemma natgehimplnatgtbfalse ( m n : nat ) ( p : natgeh n m ) : natgtb m n = false.
Show proof.
intros. unfold natgeh in p. unfold natgth in p.
apply boolnegtrueimplfalse.
intro q.
apply natlehneggth in p.
apply p. auto.
apply boolnegtrueimplfalse.
intro q.
apply natlehneggth in p.
apply p. auto.
Definition natcofaceretract ( i : nat ) : nat -> nat.
Show proof.
Lemma natcofaceretractisretract ( i : nat ) :
funcomp ( natcoface i ) ( natcofaceretract i ) = idfun nat.
Show proof.
simpl. apply funextfun.
intro n. simpl.
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.
intro n. simpl.
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.
Lemma isinjnatcoface ( i x y : nat ) : natcoface i x = natcoface i y -> x = y.
Show proof.
intros p.
change x with ( idfun _ x).
rewrite <- ( natcofaceretractisretract i ).
change y with ( idfun _ y ).
rewrite <- ( natcofaceretractisretract i ).
simpl. rewrite p. apply idpath.
change x with ( idfun _ x).
rewrite <- ( natcofaceretractisretract i ).
change y with ( idfun _ y ).
rewrite <- ( natcofaceretractisretract i ).
simpl. rewrite p. apply idpath.
Lemma natlehdecomp ( b a : nat ) :
( ∃ c : nat, ( a + c )%nat = b ) -> natleh a b.
Show proof.
revert a. induction b.
- intros a p. use (hinhuniv _ p).
intro t. destruct t as [ c f ]. destruct a.
+ apply isreflnatleh.
+ apply fromempty.
simpl in f .
exact ( negpathssx0 ( a + c ) f ).
- intros a p. use (hinhuniv _ 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.
- intros a p. use (hinhuniv _ p).
intro t. destruct t as [ c f ]. destruct a.
+ apply isreflnatleh.
+ apply fromempty.
simpl in f .
exact ( negpathssx0 ( a + c ) f ).
- intros a p. use (hinhuniv _ 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.
Lemma natdivleh ( a b k : nat ) ( f : ( a * k )%nat = b ) :
natleh a b ⨿ ( b = 0%nat ).
Show 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. rewrite natpluscomm.
assumption.
- 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. rewrite natpluscomm.
assumption.
Local Open Scope ring_scope.
Lemma ringminusdistr { X : commring } ( a b c : X ) :
a * (b - c) = a * b - a * c.
Show proof.
Lemma ringminusdistl { X : commring } ( a b c : X ) :
(b - c) * a = b * a - c * a.
Show proof.
Lemma multinvmultstable ( A : commring ) ( a b : A ) ( p : multinvpair A a )
( q : multinvpair A b ) : multinvpair A ( a * b ).
Show proof.
intros. destruct p as [ a' p ]. destruct q as [ b' q ].
split with ( b' * a' ). split.
- change ( ( ( b' * a' ) * ( a * b ) )%ring = @ringunel2 A ).
rewrite ( ringassoc2 A b').
rewrite <- ( ringassoc2 A a' ).
change ( ( ( a' * a )%ring = @ringunel2 A ) ×
( ( a * a' )%ring = @ringunel2 A ) ) in p.
change ( ( ( b' * b )%ring = @ringunel2 A ) ×
( ( b * b' )%ring = @ringunel2 A ) ) in q.
rewrite <- ( pr1 q ). apply maponpaths.
assert ( a' * a * b = 1 * b ) as f by
apply ( maponpaths ( fun x => x * b ) ( pr1 p ) ).
rewrite ringlunax2 in f. assumption.
- change ( ( ( a * b ) * ( b' * a' ) )%ring = @ringunel2 A ).
rewrite ( ringassoc2 A a). rewrite <- ( ringassoc2 A b ).
change ( ( ( a' * a )%ring = @ringunel2 A ) ×
( ( a * a' )%ring = @ringunel2 A ) ) in p.
change ( ( ( b' * b )%ring = @ringunel2 A ) ×
( ( b * b' )%ring = @ringunel2 A ) ) in q.
rewrite <- ( pr2 q ). rewrite ( pr2 q ).
rewrite ringlunax2. apply (pr2 p).
split with ( b' * a' ). split.
- change ( ( ( b' * a' ) * ( a * b ) )%ring = @ringunel2 A ).
rewrite ( ringassoc2 A b').
rewrite <- ( ringassoc2 A a' ).
change ( ( ( a' * a )%ring = @ringunel2 A ) ×
( ( a * a' )%ring = @ringunel2 A ) ) in p.
change ( ( ( b' * b )%ring = @ringunel2 A ) ×
( ( b * b' )%ring = @ringunel2 A ) ) in q.
rewrite <- ( pr1 q ). apply maponpaths.
assert ( a' * a * b = 1 * b ) as f by
apply ( maponpaths ( fun x => x * b ) ( pr1 p ) ).
rewrite ringlunax2 in f. assumption.
- change ( ( ( a * b ) * ( b' * a' ) )%ring = @ringunel2 A ).
rewrite ( ringassoc2 A a). rewrite <- ( ringassoc2 A b ).
change ( ( ( a' * a )%ring = @ringunel2 A ) ×
( ( a * a' )%ring = @ringunel2 A ) ) in p.
change ( ( ( b' * b )%ring = @ringunel2 A ) ×
( ( b * b' )%ring = @ringunel2 A ) ) in q.
rewrite <- ( pr2 q ). rewrite ( pr2 q ).
rewrite ringlunax2. apply (pr2 p).
Lemma commringaddinvunique ( X : commring ) ( a b c : X )
( p : @op1 X a b = @ringunel1 X )
( q : @op1 X a c = @ringunel1 X ) : b = c.
Show proof.
intros. rewrite ( pathsinv0 ( ringrunax1 X b ) ).
rewrite ( pathsinv0 q ).
rewrite ( pathsinv0 ( ringassoc1 X _ _ _ ) ).
rewrite ( ringcomm1 X b _ ).
rewrite p.
rewrite ringlunax1.
apply idpath.
rewrite ( pathsinv0 q ).
rewrite ( pathsinv0 ( ringassoc1 X _ _ _ ) ).
rewrite ( ringcomm1 X b _ ).
rewrite p.
rewrite ringlunax1.
apply idpath.
Lemma isapropmultinvpair ( X : commring ) ( a : X ) : isaprop ( multinvpair X a ).
Show 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 <- ( @ringrunax2 X b ).
change ( b * @ringunel2 X ) with ( b * 1 )%multmonoid.
rewrite <- ( pr2 c' ).
change ( ( b * ( a * c ) )%ring = c ).
rewrite <- ( ringassoc2 X ).
change ( b * a )%ring with ( b * a )%multmonoid.
rewrite ( pr1 b' ).
change ( ( @ringunel2 X ) * c = c )%ring.
apply ringlunax2.
}
apply (total2_paths2_f f0 ).
assert ( isaprop ( c * a = ( @ringunel2 X ) ×
a * c = ( @ringunel2 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 ( pr2 ( pr1 ( pr1 ( rigmultmonoid X ) ) ) ).
- intros. apply isofhleveldirprod.
+ apply hlevelntosn.
apply ( setproperty X ).
+ apply hlevelntosn. apply (setproperty X ).
}
apply is.
assert ( b = c ) as f.
{ destruct b as [ b b' ].
destruct c as [ c c'].
assert ( b = c ) as f0.
{ rewrite <- ( @ringrunax2 X b ).
change ( b * @ringunel2 X ) with ( b * 1 )%multmonoid.
rewrite <- ( pr2 c' ).
change ( ( b * ( a * c ) )%ring = c ).
rewrite <- ( ringassoc2 X ).
change ( b * a )%ring with ( b * a )%multmonoid.
rewrite ( pr1 b' ).
change ( ( @ringunel2 X ) * c = c )%ring.
apply ringlunax2.
}
apply (total2_paths2_f f0 ).
assert ( isaprop ( c * a = ( @ringunel2 X ) ×
a * c = ( @ringunel2 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 ( pr2 ( pr1 ( pr1 ( rigmultmonoid X ) ) ) ).
- intros. apply isofhleveldirprod.
+ apply hlevelntosn.
apply ( setproperty X ).
+ apply hlevelntosn. apply (setproperty X ).
}
apply is.
Close Scope ring_scope.
Local Open Scope hz_scope.
Lemma hzaddinvplus ( n m : hz ) : - ( n + m ) = ( - n ) + ( - m ).
Show proof.
intros.
apply commringaddinvunique with ( a := n + m ).
- apply ringrinvax1.
- assert ( ( n + m ) + ( - n + - m ) = n + - n + m + - m ) as i.
{ assert ( n + m + ( - n + - m ) = n + ( m + ( - n + - m ) ) ) as i0 by
apply ringassoc1.
assert ( n + ( m + ( - n + - m ) ) = n + ( m + - n + - m ) ) as i1.
{ apply maponpaths. apply pathsinv0. apply ringassoc1. }
assert ( n + ( m + - n + - m ) = n + (- n + m + - m ) ) as i2.
{ apply maponpaths. apply ( maponpaths ( fun x => x + - m ) ).
apply ringcomm1. }
assert ( n + ( - n + m + - m ) = n + ( - n + m ) + - m ) as i3.
{ apply pathsinv0. apply ringassoc1. }
assert ( n + ( - n + m ) + - m = n + - n + m + - m ) as i4.
{ apply pathsinv0. apply ( maponpaths ( fun x => x + - m ) ).
apply ringassoc1. }
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 ringrinvax1. }
assert ( 0 + m + - m = m + - m ) as j1.
{ apply ( maponpaths ( fun x => x + - m ) ).
apply ringlunax1. }
assert ( m + - m = 0 ) as j2 by apply ringrinvax1.
exact ( pathscomp0 j0 ( pathscomp0 j1 j2 ) ).
}
exact ( pathscomp0 i j ).
apply commringaddinvunique with ( a := n + m ).
- apply ringrinvax1.
- assert ( ( n + m ) + ( - n + - m ) = n + - n + m + - m ) as i.
{ assert ( n + m + ( - n + - m ) = n + ( m + ( - n + - m ) ) ) as i0 by
apply ringassoc1.
assert ( n + ( m + ( - n + - m ) ) = n + ( m + - n + - m ) ) as i1.
{ apply maponpaths. apply pathsinv0. apply ringassoc1. }
assert ( n + ( m + - n + - m ) = n + (- n + m + - m ) ) as i2.
{ apply maponpaths. apply ( maponpaths ( fun x => x + - m ) ).
apply ringcomm1. }
assert ( n + ( - n + m + - m ) = n + ( - n + m ) + - m ) as i3.
{ apply pathsinv0. apply ringassoc1. }
assert ( n + ( - n + m ) + - m = n + - n + m + - m ) as i4.
{ apply pathsinv0. apply ( maponpaths ( fun x => x + - m ) ).
apply ringassoc1. }
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 ringrinvax1. }
assert ( 0 + m + - m = m + - m ) as j1.
{ apply ( maponpaths ( fun x => x + - m ) ).
apply ringlunax1. }
assert ( m + - m = 0 ) as j2 by apply ringrinvax1.
exact ( pathscomp0 j0 ( pathscomp0 j1 j2 ) ).
}
exact ( pathscomp0 i j ).
Lemma hzgthsntogeh ( n m : hz ) ( p : hzgth ( n + 1 ) m ) : hzgeh n m.
Show proof.
intros.
set ( c := hzgthchoice2 ( n + 1 ) m ).
destruct c as [ h | k ].
- exact p.
- assert ( hzgth n m ) as a by exact ( hzgthandplusrinv n m 1 h ).
apply hzgthtogeh. exact a.
- rewrite ( hzplusrcan n m 1 k ). apply isreflhzgeh.
set ( c := hzgthchoice2 ( n + 1 ) m ).
destruct c as [ h | k ].
- exact p.
- assert ( hzgth n m ) as a by exact ( hzgthandplusrinv n m 1 h ).
apply hzgthtogeh. exact a.
- rewrite ( hzplusrcan n m 1 k ). apply isreflhzgeh.
Lemma hzlthsntoleh ( n m : hz ) ( p : hzlth m ( n + 1 ) ) : hzleh m n.
Show proof.
Lemma hzabsvalchoice ( n : hz ) :
( 0%nat = hzabsval n ) ⨿ ( ∑ x : nat, S x = hzabsval n ).
Show proof.
intros.
destruct ( natlehchoice _ _ ( natleh0n ( hzabsval n ) ) ) as [ l | r ].
- apply ii2. split with ( sub ( hzabsval n ) 1 ).
rewrite pathssminus.
+ change ( sub ( hzabsval n ) 0 = hzabsval n ).
rewrite minus0r. apply idpath.
+ assumption.
- apply ii1. assumption.
destruct ( natlehchoice _ _ ( natleh0n ( hzabsval n ) ) ) as [ l | r ].
- apply ii2. split with ( sub ( hzabsval n ) 1 ).
rewrite pathssminus.
+ change ( sub ( hzabsval n ) 0 = hzabsval n ).
rewrite minus0r. apply idpath.
+ assumption.
- apply ii1. assumption.
Lemma hzlthminusswap ( n m : hz ) ( p : hzlth n m ) : hzlth ( - m ) (- n ).
Show 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.
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.
Lemma hzlthminusequiv ( n m : hz ) :
( hzlth n m -> hzlth 0 ( m - n ) ) ×
( hzlth 0 ( m - n ) -> hzlth n m ).
Show 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.
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.
Lemma hzlthminus ( n m k : hz ) ( p : hzlth n k ) ( q : hzlth m k )
( q' : hzleh 0 m ) : hzlth ( n - m ) k.
Show 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.
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.
Lemma hzabsvalandminuspos ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) :
nattohz ( hzabsval ( n - m ) ) = nattohz ( hzabsval ( m - n ) ).
Show 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 )%ring.
rewrite ringminusminus.
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 )%ring.
rewrite ringminusminus.
rewrite hzpluscomm.
apply idpath.
* apply a.
+ rewrite k. apply idpath.
- 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 )%ring.
rewrite ringminusminus.
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 )%ring.
rewrite ringminusminus.
rewrite hzpluscomm.
apply idpath.
* apply a.
+ rewrite k. apply idpath.
Lemma hzabsvalneq0 ( n : hz ) ( p : hzneq 0 n ) :
hzlth 0 ( nattohz ( hzabsval n ) ).
Show proof.
intros. destruct ( hzneqchoice 0 n p ) as [ left | right ].
- rewrite hzabsvallth0.
+ apply hzlth0andminus. apply left.
+ apply left.
- rewrite hzabsvalgth0.
+ assumption.
+ apply right.
- rewrite hzabsvallth0.
+ apply hzlth0andminus. apply left.
+ apply left.
- rewrite hzabsvalgth0.
+ assumption.
+ apply right.
Definition hzrdistr ( a b c : hz ) : ( a + b ) * c = ( a * c ) + ( b * c ) :=
ringrdistr hz a b c.
Definition hzldistr ( a b c : hz ) : c * ( a + b ) = ( c * a ) + ( c * b ) :=
ringldistr hz a b c.
Lemma hzabsvaland1 : hzabsval 1 = 1%nat.
Show proof.
apply ( invmaponpathsincl _ isinclnattohz ).
rewrite hzabsvalgth0.
- rewrite nattohzand1.
apply idpath.
- rewrite <- ( hzplusl0 1 ). apply ( hzlthnsn 0 ).
rewrite hzabsvalgth0.
- rewrite nattohzand1.
apply idpath.
- rewrite <- ( hzplusl0 1 ). apply ( hzlthnsn 0 ).
Lemma hzabsvalandplusnonneg ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) :
hzabsval ( n + m ) = ( ( hzabsval n ) + ( hzabsval m ) )%nat.
Show 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 ( invmaponpathsincl _ isinclnattohz ).
rewrite nattohzandplus.
rewrite hzabsvalgeh0. - rewrite hzabsvalgeh0.
+ rewrite hzabsvalgeh0.
* apply idpath.
* assumption.
+ assumption.
- assumption.
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 ( invmaponpathsincl _ isinclnattohz ).
rewrite nattohzandplus.
rewrite hzabsvalgeh0. - rewrite hzabsvalgeh0.
+ rewrite hzabsvalgeh0.
* apply idpath.
* assumption.
+ assumption.
- assumption.
Lemma hzabsvalandplusneg ( n m : hz ) ( p : hzlth n 0 ) ( q : hzlth m 0 ) :
hzabsval ( n + m ) = ( ( hzabsval n ) + ( hzabsval m ) )%nat.
Show 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 ( invmaponpathsincl _ isinclnattohz ).
rewrite nattohzandplus.
rewrite hzabsvallth0.
- rewrite hzabsvallth0.
+ rewrite hzabsvallth0.
* rewrite hzaddinvplus. apply idpath.
* assumption.
+ assumption.
- assumption.
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 ( invmaponpathsincl _ isinclnattohz ).
rewrite nattohzandplus.
rewrite hzabsvallth0.
- rewrite hzabsvallth0.
+ rewrite hzabsvallth0.
* rewrite hzaddinvplus. apply idpath.
* assumption.
+ assumption.
- assumption.
Lemma hzabsvalandnattohz ( n : nat ) : hzabsval ( nattohz n ) = n.
Show 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.
- 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.
Lemma hzabsvalandlth ( n m : hz ) ( p : hzleh 0 n ) ( p' : hzlth n m ) :
natlth ( hzabsval n ) ( hzabsval m ).
Show proof.
intros.
destruct ( natlthorgeh ( hzabsval n ) ( hzabsval m ) ) as [ h | k ].
- assumption.
- apply fromempty.
apply ( isirreflhzlth m ).
apply ( hzlehlthtrans _ n _ ).
+ rewrite <- ( hzabsvalgeh0 ).
* rewrite <- ( hzabsvalgeh0 p ).
apply nattohzandleh.
apply k.
* apply hzgthtogeh.
apply ( hzgthgehtrans _ n _ ); assumption.
+ assumption.
destruct ( natlthorgeh ( hzabsval n ) ( hzabsval m ) ) as [ h | k ].
- assumption.
- apply fromempty.
apply ( isirreflhzlth m ).
apply ( hzlehlthtrans _ n _ ).
+ rewrite <- ( hzabsvalgeh0 ).
* rewrite <- ( hzabsvalgeh0 p ).
apply nattohzandleh.
apply k.
* apply hzgthtogeh.
apply ( hzgthgehtrans _ n _ ); assumption.
+ assumption.
Lemma nattohzandlthinv ( n m : nat ) ( p : hzlth ( nattohz n ) (nattohz m ) ) :
natlth n m.
Show proof.
intros.
rewrite <- ( hzabsvalandnattohz n ).
rewrite <- ( hzabsvalandnattohz m ).
apply hzabsvalandlth.
- change 0 with ( nattohz 0%nat ).
apply nattohzandleh.
apply natleh0n .
- assumption.
rewrite <- ( hzabsvalandnattohz n ).
rewrite <- ( hzabsvalandnattohz m ).
apply hzabsvalandlth.
- change 0 with ( nattohz 0%nat ).
apply nattohzandleh.
apply natleh0n .
- assumption.
Close Scope hz_scope.
Definition iscomparel { X : UU } ( R : hrel X ) :=
forall x y z : X, R x y -> R x z ⨿ R z y.
Definition isapart { X : UU } ( R : hrel X ) :=
isirrefl R × ( issymm R × iscotrans R ).
Definition istightapart { X : UU } ( R : hrel X ) :=
isapart R × forall x y : X, neg ( R x y ) -> x = y.
Definition apart ( X : hSet ) := ∑ 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 ) :=
isbinopapartl R opp × isbinopapartr R opp.
Lemma deceqtoneqapart { X : UU } ( is : isdeceq X ) : isapart ( neq X ).
Show proof.
intros. split.
- intros a p. simpl in p. apply p. apply idpath.
- split.
+ intros a b p q.
simpl in p. 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.
- intros a p. simpl in p. apply p. apply idpath.
- split.
+ intros a b p q.
simpl in p. 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.
Definition isapartdec { X : hSet } ( R : apart X ) :=
forall a b : X, pr1 R a b ⨿ ( a = b ).
Lemma isapartdectodeceq { X : hSet } ( R : apart X ) ( is : isapartdec R ) :
isdeceq X.
Show proof.
intros 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.
- apply ii2. intros f. apply ( pr1 ( pr2 R ) z).
rewrite f in l. assumption.
- apply ii1. assumption.
Lemma isdeceqtoisapartdec ( X : hSet ) ( is : isdeceq X ) :
isapartdec ( tpair _ ( deceqtoneqapart is ) ).
Show proof.
intros a b. destruct ( is a b ) as [ l | r ].
- apply ii2. assumption.
- apply ii1. intros f. apply r. assumption.
- apply ii2. assumption.
- apply ii1. intros f. apply r. assumption.
Local Open Scope ring_scope.
Definition acommring := ∑ (X : commring) (R : apart X),
isbinopapart R ( @op1 X ) × isbinopapart R ( @op2 X ).
Definition make_acommring := tpair ( P := fun X : commring =>
∑ R : apart X, isbinopapart R ( @op1 X ) × isbinopapart R ( @op2 X ) ).
Definition acommringconstr := make_acommring.
Definition acommringtocommring : acommring -> commring := @pr1 _ _.
Coercion acommringtocommring : acommring >-> commring.
Definition acommringapartrel ( X : acommring ) : hrel (pr1 X) :=
pr1 ( pr1 ( pr2 X ) ).
Notation " a # b " := ( acommringapartrel _ a b ) :
ring_scope.
Definition acommring_aadd ( X : acommring ) : isbinopapart ( pr1 ( pr2 X ) ) op1 :=
pr1 ( pr2 ( pr2 X ) ).
Definition acommring_amult ( X : acommring ) : isbinopapart ( pr1 ( pr2 X ) ) op2 :=
pr2 ( pr2 ( pr2 X ) ).
Definition acommring_airrefl ( X : acommring ) : isirrefl ( pr1 ( pr1 ( pr2 X ) ) ) :=
pr1 ( pr2 ( pr1 ( pr2 X ) ) ).
Definition acommring_asymm ( X : acommring ) : issymm ( pr1 ( pr1 ( pr2 X ) ) ) :=
pr1 ( pr2 ( pr2 ( pr1 ( pr2 X ) ) ) ).
Definition acommring_acotrans ( X : acommring ) : iscotrans ( pr1 ( pr1 ( pr2 X ) ) ) :=
pr2 ( pr2 ( pr2 ( pr1 ( pr2 X ) ) ) ).
Definition aintdom := ∑ A : acommring,
( ringunel2 ( X := A ) ) # 0 ×
forall a b : A, a # 0 -> b # 0 -> ( a * b ) # 0.
Definition make_aintdom := tpair ( P := fun A : acommring =>
( ringunel2 ( X := A ) ) # 0 ×
forall a b : A, a # 0 -> b # 0 -> ( a * b ) # 0 ).
Definition aintdomconstr := make_aintdom.
Definition pr1aintdom : aintdom -> acommring := @pr1 _ _.
Coercion pr1aintdom : aintdom >-> acommring.
Definition aintdomazerosubmonoid ( A : aintdom ) : @subabmonoid ( ringmultabmonoid A ).
Show proof.
intros. split with ( fun x : A => x # 0 ).
split.
- intros a b. simpl in *. apply (pr2 (pr2 A)).
+ simpl in a. apply (pr2 a).
+ apply (pr2 b).
- apply (pr2 A).
split.
- intros a b. simpl in *. apply (pr2 (pr2 A)).
+ simpl in a. apply (pr2 a).
+ apply (pr2 b).
- apply (pr2 A).
Definition isaafield ( A : acommring ) :=
( ringunel2 ( X := A ) ) # 0 ×
forall x : A, x # 0 -> multinvpair A x.
Definition afld := ∑ A : acommring, isaafield A.
Definition make_afld ( A : acommring ) ( is : isaafield A ) : afld := tpair A is .
Definition pr1afld : afld -> acommring := @pr1 _ _ .
Coercion pr1afld : afld >-> acommring.
Lemma afldinvertibletoazero ( A : afld ) ( a : A ) ( p : multinvpair A a ) : a # 0.
Show proof.
intros. destruct p as [ a' p ].
assert ( a' * a # 0 ) as q.
{ change ( a' * a # 0 ).
assert ( a' * a = a * a' ) as f by apply ( ringcomm2 A ).
assert ( a * a' = 1 ) as g by apply (pr2 p).
rewrite f, g.
apply (pr2 A).
}
assert ( a' * a # a' * ( ringunel1 ( X := A ) ) ) as q'.
{ assert ( ringunel1 ( X := A ) = a' * ( ringunel1 ( X := A ) ) ) as f.
{ apply pathsinv0. apply ( ringmultx0 A ). }
rewrite <- f. assumption.
}
apply ( pr1 ( acommring_amult A ) a' ).
assumption.
assert ( a' * a # 0 ) as q.
{ change ( a' * a # 0 ).
assert ( a' * a = a * a' ) as f by apply ( ringcomm2 A ).
assert ( a * a' = 1 ) as g by apply (pr2 p).
rewrite f, g.
apply (pr2 A).
}
assert ( a' * a # a' * ( ringunel1 ( X := A ) ) ) as q'.
{ assert ( ringunel1 ( X := A ) = a' * ( ringunel1 ( X := A ) ) ) as f.
{ apply pathsinv0. apply ( ringmultx0 A ). }
rewrite <- f. assumption.
}
apply ( pr1 ( acommring_amult A ) a' ).
assumption.
Definition afldtoaintdom ( A : afld ) : aintdom .
Show proof.
split with ( pr1 A ). split.
- apply (pr2 A).
- intros a b p q.
apply afldinvertibletoazero.
apply multinvmultstable.
+ apply (pr2 (pr2 A)). assumption.
+ apply (pr2 (pr2 A)). assumption.
- apply (pr2 A).
- intros a b p q.
apply afldinvertibletoazero.
apply multinvmultstable.
+ apply (pr2 (pr2 A)). assumption.
+ apply (pr2 (pr2 A)). assumption.
Lemma timesazero { A : acommring } { a b : A } ( p : a * b # 0 ) :
a # 0 × b # 0.
Show proof.
intros. split.
- assert ( a * b # 0 * b ) as h.
{ rewrite ( ringmult0x A ). assumption. }
apply ( pr2 ( acommring_amult A ) b ). assumption.
- apply ( pr1 ( acommring_amult A ) a ).
rewrite ( ringmultx0 A ). assumption.
- assert ( a * b # 0 * b ) as h.
{ rewrite ( ringmult0x A ). assumption. }
apply ( pr2 ( acommring_amult A ) b ). assumption.
- apply ( pr1 ( acommring_amult A ) a ).
rewrite ( ringmultx0 A ). assumption.
Lemma aaminuszero { A : acommring } { a b : A } ( p : a # b ) : ( a - b ) # 0.
Show proof.
intros.
rewrite <- ( ringrunax1 A a ) in p.
rewrite <- ( ringrunax1 A b ) in p.
assert ( a + 0 = a + ( b - b ) ) as f.
{ rewrite <- ( ringrinvax1 A b ). apply idpath. }
rewrite f in p.
rewrite <- ( ringmultwithminus1 A ) in p.
rewrite <- ( ringassoc1 A) in p.
rewrite ( ringcomm1 A a ) in p.
rewrite ( ringassoc1 A b ) in p.
rewrite ( ringmultwithminus1 A ) in p.
apply ( pr1 ( acommring_aadd A ) b ( a - b ) 0 ).
assumption.
rewrite <- ( ringrunax1 A a ) in p.
rewrite <- ( ringrunax1 A b ) in p.
assert ( a + 0 = a + ( b - b ) ) as f.
{ rewrite <- ( ringrinvax1 A b ). apply idpath. }
rewrite f in p.
rewrite <- ( ringmultwithminus1 A ) in p.
rewrite <- ( ringassoc1 A) in p.
rewrite ( ringcomm1 A a ) in p.
rewrite ( ringassoc1 A b ) in p.
rewrite ( ringmultwithminus1 A ) in p.
apply ( pr1 ( acommring_aadd A ) b ( a - b ) 0 ).
assumption.
Lemma aminuszeroa { A : acommring } { a b : A } ( p : ( a - b ) # 0 ) : a # b.
Show proof.
intros.
change 0 with ( @ringunel1 A ) in p.
rewrite <- ( ringrinvax1 A b ) in p.
rewrite <- ( ringmultwithminus1 A ) in p.
apply ( pr2 ( acommring_aadd A ) ( -1 * b ) a b ).
assumption.
change 0 with ( @ringunel1 A ) in p.
rewrite <- ( ringrinvax1 A b ) in p.
rewrite <- ( ringmultwithminus1 A ) in p.
apply ( pr2 ( acommring_aadd A ) ( -1 * b ) a b ).
assumption.
Close Scope ring_scope.
Lemma horelim ( A B : UU ) ( P : hProp ) :
( ishinh_UU A -> P ) × ( ishinh_UU B -> P ) -> A ∨ B -> P.
Show proof.
intros p q. simpl in q. apply q.
intro u. destruct u as [ u | v ].
- apply ( pr1 p ). intro Q. intro H. apply H. assumption.
- apply ( pr2 p ). intro Q. intro H. apply H. assumption.
intro u. destruct u as [ u | v ].
- apply ( pr1 p ). intro Q. intro H. apply H. assumption.
- apply ( pr2 p ). intro Q. intro H. apply H. assumption.
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.
Show proof.
intros. destruct n.
- assumption.
- apply q.
+ split.
+ 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. split.
++ intros k s. rewrite right in s. apply ( IHn k ). assumption.
- assumption.
- apply q.
+ split.
+ 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. split.
++ intros k s. rewrite right in s. apply ( IHn k ). assumption.
Definition isdecnatprop ( P : nat -> hProp ) :=
forall m : nat, P m ⨿ neg ( P m ).
Lemma negisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) :
isdecnatprop ( fun n : nat => hneg ( P n ) ).
Show proof.
intros n. destruct ( is n ) as [ l | r ].
- apply ii2. intro j.
assert hfalse as x.
{ simpl in j. apply j. assumption. }
apply x.
- apply ii1. assumption.
- apply ii2. intro j.
assert hfalse as x.
{ simpl in j. apply j. assumption. }
apply x.
- apply ii1. assumption.
Lemma bndexistsisdecnatprop ( P : nat -> hProp ) ( is : isdecnatprop P ) :
isdecnatprop ( fun n : nat => ∃ m : nat, natleh m n × P m ).
Show proof.
intros 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.
{ simpl in j. apply j. intro m.
destruct m as [ m m' ].
apply r.
change ( natleh m 0 × P m ) in m'.
rewrite ( natleh0tois0 ( pr1 m' ) ) in m'.
apply (pr2 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.
use (hinhuniv _ l').
intro m.
destruct m as [ m m' ].
apply total2tohexists.
split with m. split.
-- apply ( istransnatleh(m := n) ).
++ apply m'.
++ apply natlthtoleh. apply natlthnsn.
-- apply (pr2 m').
* apply ii2. intro j.
apply r'.
use (hinhuniv _ j).
intro m. destruct m as [ m m' ].
-- apply total2tohexists. split with m.
split.
++ destruct ( natlehchoice m ( S n ) ( pr1 m' ) ) as [ h | p ].
** apply natlthsntoleh. assumption.
** apply fromempty.
apply r.
rewrite <- p.
apply (pr2 m').
++ apply (pr2 m').
- 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.
{ simpl in j. apply j. intro m.
destruct m as [ m m' ].
apply r.
change ( natleh m 0 × P m ) in m'.
rewrite ( natleh0tois0 ( pr1 m' ) ) in m'.
apply (pr2 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.
use (hinhuniv _ l').
intro m.
destruct m as [ m m' ].
apply total2tohexists.
split with m. split.
-- apply ( istransnatleh(m := n) ).
++ apply m'.
++ apply natlthtoleh. apply natlthnsn.
-- apply (pr2 m').
* apply ii2. intro j.
apply r'.
use (hinhuniv _ j).
intro m. destruct m as [ m m' ].
-- apply total2tohexists. split with m.
split.
++ destruct ( natlehchoice m ( S n ) ( pr1 m' ) ) as [ h | p ].
** apply natlthsntoleh. assumption.
** apply fromempty.
apply r.
rewrite <- p.
apply (pr2 m').
++ apply (pr2 m').
Lemma isdecisbndqdec ( P : nat -> hProp ) ( is : isdecnatprop P ) ( n : nat ) :
( forall m : nat, natleh m n -> P m ) ⨿ ∃ m : nat, natleh m n × neg ( P m ).
Show proof.
destruct ( bndexistsisdecnatprop _ ( negisdecnatprop P is ) n ) as [ l | r ].
- apply ii2. assumption.
- apply ii1. intros m j.
destruct ( is m ) as [ l' | r' ].
+ assumption.
+ apply fromempty.
apply r. apply total2tohexists.
split with m.
split; assumption.
- apply ii2. assumption.
- apply ii1. intros m j.
destruct ( is m ) as [ l' | r' ].
+ assumption.
+ apply fromempty.
apply r. apply total2tohexists.
split with m.
split; assumption.
Lemma leastelementprinciple ( n : nat ) ( P : nat -> hProp )
( is : isdecnatprop P ) : P n ->
∃ k : nat, P k × forall m : nat, natlth m k -> neg ( P m ).
Show proof.
revert P is. induction n.
- intros P is u.
apply total2tohexists.
split with 0%nat. split.
+ assumption.
+ intros m i.
apply fromempty.
apply ( negnatgth0n m i ).
- intros P is u.
destruct ( is 0%nat ) as [ l | r ].
+ apply total2tohexists. split with 0%nat. split.
* assumption.
* intros m i.
apply fromempty.
apply ( negnatgth0n m i ).
+ set ( P' := fun m : nat => P ( S m ) ).
assert ( forall m : nat, P' m ⨿ neg ( P' m ) ) as is'.
{ intros m. unfold P'. apply ( is ( S m ) ). }
set ( c := IHn P' is' u ).
use (hinhuniv _ 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.
- intros P is u.
apply total2tohexists.
split with 0%nat. split.
+ assumption.
+ intros m i.
apply fromempty.
apply ( negnatgth0n m i ).
- intros P is u.
destruct ( is 0%nat ) as [ l | r ].
+ apply total2tohexists. split with 0%nat. split.
* assumption.
* intros m i.
apply fromempty.
apply ( negnatgth0n m i ).
+ set ( P' := fun m : nat => P ( S m ) ).
assert ( forall m : nat, P' m ⨿ neg ( P' m ) ) as is'.
{ intros m. unfold P'. apply ( is ( S m ) ). }
set ( c := IHn P' is' u ).
use (hinhuniv _ 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.
END OF FILE