Let's take a number m and exhibit a prime bigger than it.
Every natural number greater than 1 has at least one prime divisor.
If we take m! + 1, then such prime divisor p can be shown to be grater
than m as follows.
By contra position we assume p <= m and we show p does not divide m! + 1.
Being smaller than m, p|m!, hence to divide m! + 1, p should divide 1,
that is not possible since p is prime, hence greater than 1.
Lemma contraL c b : (c -> ~~ b) -> b -> ~~ c.
Lemma gtnNdvd n d : 0 < n -> n < d -> (d %| n) = false.
Lemma dvdn_addr m d n : d %| m -> (d %| m + n) = (d %| n).
Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
Bool is not enough
The bool data type is not closed under general quantifiers
Coq provides the Prop world for propositions
We need a way to relate the two worlds
to say: exists/curry howard, bool/Prop, reflect
by case: a; case: b.
by move=> [pa pb]; rewrite pa pb.
Views and intro patterns
Two ways to use a reflect
to say: move= /andP eqP ==
Lemma ltnW m n : m < n -> m <= n.
Lemma eqP m n : reflect (m = n) (m == n).
Lemma ltngtP m n : compare_nat m n (m < n) (n < m) (m == n)
Infinitude of primes
Lemma pdivP n : 1 < n -> exists2 p, prime p & p %| n.
Lemma dvdn_mull d m n : d %| n -> d %| m * n.
Lemma dvdn_mulr d m n : d %| m -> d %| m * n.
Wrap up
logic of Coq
lets you express programs
Coq knows hot compute them
their execution is a legit form of proof
boolean predicates
symbolic computation at hand
EM at hand
... UIP at hand ...
proof language
small bricks
compose well
squeezing video game quite addictive ;-)
Exercises
Hint1: Search results can be limited to the ssrnat module as in
Search_somethinginssrnat. All the lemmas you
are looking for live in there.
Hint2: removing an hypothesis named Hyp from the context
can be done with move=>{Hyp}.
elim: n => // n IHn.
rewrite expnS odd_mul IHn orbC.
move=> {IHn}.
by case: (odd m).
by rewrite mulnBl !mulnDr addnC (mulnC m) subnDl !mulnn.
