The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

On 13/02/2015 16:05, Saulo Araujo wrote:
> Thanks a lot Amin!
>
>
I want to present another proof expressed with the mathematical proof
language.
This proof is longer that the previous proof written with coq-commands,
because I am retired and I don't write proofs very often.
But a mathematician, without coq's knowledge, can read it : great
advantage ! And even write an another better proof.
Thanks to Pierre Corbineau for this language.


Require Import Coq.Logic.Classical.
Require Import Coq.omega.Omega.
Require Import Coq.Arith.Arith.

(* Basic fact on nat *)
Theorem leS : forall n p : nat, S n >= p -> n >= p \/ S n = p.
proof.
assume n: nat and p:nat and H1: (S n >= p).
(* then H1 :(le_or_lt p (S n)).*)
then H2:((S n > p) \/ (S n = p)) by (le_lt_or_eq p (S n)).
per cases on H2.
suppose H3:(S n > p).
then H4:(n >= p) by (lt_n_Sm_le p n).
thus thesis by H4.
suppose H3 : (S n = p).
thus thesis by H3.
end cases.
end proof.
Qed.

(* The theorem : an non decreasing bounded above function, becomes stable *)
Theorem convergence_t1 :
  forall (f : nat -> nat),
    (forall n, f n <= f (S n)) -> ((exists l, forall n, f n <= l) ->
    exists N L, forall n, n >= N -> f n = L).
proof.
assume f:(nat->nat) and H1: (forall n, f n <= f (S n )).
assume H2 : (exists l, forall n, f n <= l).
(* soit f croissante bornée : f devient stable *)
consider l:nat such that H3 : (forall n, f n <= l) from H2.
claim H4:((forall n,f n <= l) -> exists N L, forall n, n >= N -> f n = L).
per induction on l.

(* cas l = 0 *)
suppose it is 0 .
assume H4 :(forall n,f n <= 0).
then H5:(forall n,n >= 0 -> f n = 0) by H4.
thus thesis by H5.
(* fin du cas l = 0 *)

(* cas l = (S m) *)
suppose it is (S m)
and H4 : ((forall n,f n <= m) ->
(exists N L,  forall n,n >= N -> f n = L)) .

assume H5 :(forall n,f n <= S m).


claim H9: (~(forall n,f n <= m) -> (exists n, f n = S m)) .
assume H10: (~(forall n,f n <= m)).
then H11 : (exists n,~(f n <= m)) by ((not_all_ex_not  nat (fun n => f n
<= m))H10).
consider n such that H12 :(~(f n <= m)) from H11.
then H13:(f n = S m) by (H5 n),H12.
thus thesis by H13.
end claim.

claim H10 : ((forall n,f n <= m) \/ (exists n, f n = S m)) .
then H11 : ((forall n,f n <= m) \/ ~ (forall n, f n <= m)) by (classic
(forall n,f n <= m)).
per cases on H11.

suppose H12 : (forall n,f n <= m).
thus thesis by H12.

suppose H13 : (~(forall n,f n <= m)).
then H14 : (exists n,f n = S m) by H13, H9.
thus thesis by H14.
end cases.
end claim.
(* fin de la preuve de H10 *)

per cases on H10.
suppose H11 : (forall n, f n <= m).
thus thesis by H4, H11.
suppose H12 : (exists n, f n = S m).
consider N such that H13 :(f N = S m) from H12.

claim H14 : (forall n:nat, n >= N -> f n = S m).
let n : nat.
per induction on n.

suppose it is 0.
assume H15 : (0 >= N).
then H16 :(N = 0) by H15.
thus thesis by H16, H13.

suppose it is (S k) and H17:(k >= N -> f k = S m).
assume H18 : (S k >= N).
then H19:((k >= N) \/ (S k = N)) by (leS k N).

per cases on H19.
suppose H20:(k >= N).
then H21:(f k = S m) by H17.
then H22 :(f (S k) >= f k) by (H1 k).
then H23 : (f (S k) >= S m) by H21,H22.
thus thesis by H23, (H5 (S k)).
suppose H20:(S k = N).
thus thesis by H20,H13.
end cases.
end induction.
end claim.
thus thesis by H14.
end cases.
(* fin des cas de H10 *)


end induction.
thus thesis by H3,H4.

end proof.
Qed.

-- 
email : 
michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy