(* Preuves automatiques pour le 125-théorème *)
Retour


type rbarre=Real | Left | Right | Plusinfinity | Minusinfinity;;


let intro b c="Fixons "^
(match c with
   | Real -> "eps>0. "
   | Left -> "eps>0. "
   | Right -> "eps>0. "
   | Plusinfinity -> "M dans R. "
   | Minusinfinity -> "M dans R. ")
^(string_of_char (char_of_int 10))^(string_of_char (char_of_int 10))
^"Puisque g(x) tend vers "^
(match c with
   | Real -> "c"
   | Left -> "c-"
   | Right -> "c+"
   | Plusinfinity -> "+infini "
   | Minusinfinity -> "-infini ")
^" lorsque x tend vers "^
(match b with
   | Real -> "b"
   | Left -> "b-"
   | Right -> "b+"
   | Plusinfinity -> "+infini "
   | Minusinfinity -> "-infini ")
^", il existe "^
(match b with
   | Real -> "alpha>0"
   | Left -> "alpha>0"
   | Right -> "alpha>0"
   | Plusinfinity -> "X réel"
   | Minusinfinity -> "X réel")
^" tel que pour tout x dans "^
(match b with
   | Real -> "[b-alpha,b+alpha]"
   | Left -> "[b-alpha,b["
   | Right -> "]b,b+alpha]"
   | Plusinfinity -> "[X,+infini["
   | Minusinfinity -> "]-infini,X]")^
", on a g(x) dans "^
(match c with
   | Real -> "[c-eps,c+eps]"
   | Left -> "[c-eps,c["
   | Right -> "]c,c+eps]"
   | Plusinfinity -> "[M,+infini[ "
   | Minusinfinity -> "]-infini,M]")^".";;


let intermediaire a b c="Mais  f(t) tend vers "^
(match b with
   | Real -> "b"
   | Left -> "b-"
   | Right -> "b+"
   | Plusinfinity -> "+infini "
   | Minusinfinity -> "-infini ")
^" lorsque t tend vers "^
(match a with
   | Real -> "a"
   | Left -> "a-"
   | Right -> "a+"
   | Plusinfinity -> "+infini "
   | Minusinfinity -> "-infini ")
^", donc il existe "^
(match a with
   | Real -> "rho>0"
   | Left -> "rho>0"
   | Right -> "rho>0"
   | Plusinfinity -> "T réel"
   | Minusinfinity -> "T réel")
^" tel que pour tout t dans "^
(match a with
   | Real -> "[a-rho,a+rho]"
   | Left -> "[a-rho,a["
   | Right -> "]a,a+rho]"
   | Plusinfinity -> "[T,+infini["
   | Minusinfinity -> "]-infini,T]")^
", on a f(t) dans "^
(match b with
   | Real -> "[b-alpha,b+alpha]"
   | Left -> "[b-alpha,b["
   | Right -> "]b,b+alpha]"
   | Plusinfinity -> "[X,+infini["
   | Minusinfinity -> "]-infini,X]")^
", donc  g(f(t)) dans "^
(match c with
   | Real -> "[c-eps,c+eps]"
   | Left -> "[c-eps,c["
   | Right -> "]c,c+eps]"
   | Plusinfinity -> "[M,+infini[ "
   | Minusinfinity -> "]-infini,M]")^".";;


let conclusion a c="On vient donc de montrer que pour tout "^
(match c with
   | Real -> "eps>0"
   | Left -> "eps>0"
   | Right -> "eps>0"
   | Plusinfinity -> "M dans R"
   | Minusinfinity -> "M dans R")
^", il existe "^
(match a with
   | Real -> "rho>0"
   | Left -> "rho>0"
   | Right -> "rho>0"
   | Plusinfinity -> "T réel"
   | Minusinfinity -> "T réel")
^" tel que pour tout t dans "^
(match a with
   | Real -> "[a-rho,a+rho]"
   | Left -> "[a-rho,a["
   | Right -> "]a,a+rho]"
   | Plusinfinity -> "[T,+infini["
   | Minusinfinity -> "]-infini,T]")^
", on a g(f(t)) dans "^
(match c with
   | Real -> "[c-eps,c+eps]"
   | Left -> "[c-eps,c["
   | Right -> "]c,c+eps]"
   | Plusinfinity -> "[M,+infini[ "
   | Minusinfinity -> "]-infini,M]")
^" : c'est  exactement ce qu'il fallait démontrer.";;

#open "sys";;

let preuve a b c file_name=
  let file_out=open_out (file_name^".txt") in
    begin
      output_string file_out (intro b c);
      output_char file_out `\n`;
      output_char file_out `\n`;
      output_string file_out (intermediaire a b c);
      output_char file_out `\n`;
      output_char file_out `\n`;
      output_string file_out "----------";
      output_char file_out `\n`;
      output_char file_out `\n`;
      output_string file_out (conclusion a c);
      close_out file_out
    end;;

chdir "c:/mesdoc~1/PCSI/cours_~1/analyse/continuite/Preuves";

preuve Real Real Real "rrr";;
preuve Real Plusinfinity Left "rpg";;
preuve Plusinfinity Right Minusinfinity "pdm";;

let tab_rbarre=[|Real;Left;Right;Plusinfinity;Minusinfinity|]
and tab_noms=[|"r";"g";"d";"p";"m"|];;

let create_files () =
  (* Attention, il faut être dans le bon repertoire... *)
  for a=0 to 4 do for b=0 to 4 do for c=0 to 4 do
  preuve (tab_rbarre.(a)) (tab_rbarre.(b)) (tab_rbarre.(c))
((tab_noms.(a))^(tab_noms.(b))^(tab_noms.(c)))
  done done done;;


create_files ();;