aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/fourier/fourierR.ml
blob: bffca62231ddcd87fca0a8c3bd202d43f87aeefb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)



(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
des inéquations et équations sont entiers. En attendant la tactique Field.
*)

open Term
open Tactics
open Names
open Globnames
open Fourier
open Contradiction
open Proofview.Notations

(******************************************************************************
Opérations sur les combinaisons linéaires affines.
La partie homogène d'une combinaison linéaire est en fait une table de hash
qui donne le coefficient d'un terme du calcul des constructions,
qui est zéro si le terme n'y est pas.
*)

module Constrhash = Hashtbl.Make
  (struct type t = constr
	  let equal = eq_constr
	  let hash = hash_constr
   end)

type flin = {fhom: rational Constrhash.t;
             fcste:rational};;

let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;

let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;;

let flin_add f x c =
    let cx = flin_coef f x in
    Constrhash.replace f.fhom x (rplus cx c);
    f
;;
let flin_add_cste f c =
    {fhom=f.fhom;
     fcste=rplus f.fcste c}
;;

let flin_one () = flin_add_cste (flin_zero()) r1;;

let flin_plus f1 f2 =
    let f3 = flin_zero() in
    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
    flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
;;

let flin_minus f1 f2 =
    let f3 = flin_zero() in
    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
    Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
    flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
;;
let flin_emult a f =
    let f2 = flin_zero() in
    Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
    flin_add_cste f2 (rmult a f.fcste);
;;

(*****************************************************************************)

type ineq = Rlt | Rle | Rgt | Rge

let string_of_R_constant kn =
  match Names.repr_con kn with
    | MPfile dir, sec_dir, id when
	sec_dir = DirPath.empty &&
	DirPath.to_string dir = "Coq.Reals.Rdefinitions"
	-> Label.to_string id
    | _ -> "constant_not_of_R"

let rec string_of_R_constr c =
 match kind_of_term c with
   Cast (c,_,_) -> string_of_R_constr c
  |Const (c,_) -> string_of_R_constant c
  | _ -> "not_of_constant"

exception NoRational

let rec rational_of_constr c =
  match kind_of_term c with
  | Cast (c,_,_) -> (rational_of_constr c)
  | App (c,args) ->
      (match (string_of_R_constr c) with
	 | "Ropp" ->
	     rop (rational_of_constr args.(0))
	 | "Rinv" ->
	     rinv (rational_of_constr args.(0))
	 | "Rmult" ->
	     rmult (rational_of_constr args.(0))
                   (rational_of_constr args.(1))
	 | "Rdiv" ->
	     rdiv (rational_of_constr args.(0))
                  (rational_of_constr args.(1))
	 | "Rplus" ->
	     rplus (rational_of_constr args.(0))
                   (rational_of_constr args.(1))
	 | "Rminus" ->
	     rminus (rational_of_constr args.(0))
                    (rational_of_constr args.(1))
	 | _ -> raise NoRational)
  | Const (kn,_) ->
      (match (string_of_R_constant kn) with
	       "R1" -> r1
              |"R0" -> r0
              |  _ -> raise NoRational)
  |  _ -> raise NoRational
;;

exception NoLinear

let rec flin_of_constr c =
  try(
    match kind_of_term c with
  | Cast (c,_,_) -> (flin_of_constr c)
  | App (c,args) ->
      (match (string_of_R_constr c) with
	   "Ropp" ->
             flin_emult (rop r1) (flin_of_constr args.(0))
	 | "Rplus"->
             flin_plus (flin_of_constr args.(0))
	               (flin_of_constr args.(1))
	 | "Rminus"->
             flin_minus (flin_of_constr args.(0))
	                (flin_of_constr args.(1))
	 | "Rmult"->
	     (try
                let a = rational_of_constr args.(0) in
                try
                  let b = rational_of_constr args.(1) in
		  flin_add_cste (flin_zero()) (rmult a b)
		with NoRational ->
                  flin_add (flin_zero()) args.(1) a
	      with NoRational ->
                flin_add (flin_zero()) args.(0)
		  (rational_of_constr args.(1)))
	 | "Rinv"->
	     let a = rational_of_constr args.(0) in
	     flin_add_cste (flin_zero()) (rinv a)
	 | "Rdiv"->
	     (let b = rational_of_constr args.(1) in
	      try
                let a = rational_of_constr args.(0) in
	        flin_add_cste (flin_zero()) (rdiv a b)
	      with NoRational ->
                flin_add (flin_zero()) args.(0) (rinv b))
         |_-> raise NoLinear)
  | Const (c,_) ->
        (match (string_of_R_constant c) with
	       "R1" -> flin_one ()
              |"R0" -> flin_zero ()
              |_-> raise NoLinear)
  |_-> raise NoLinear)
  with NoRational | NoLinear -> flin_add (flin_zero()) c r1
;;

let flin_to_alist f =
    let res=ref [] in
    Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f;
    !res
;;

(* Représentation des hypothèses qui sont des inéquations ou des équations.
*)
type hineq={hname:constr; (* le nom de l'hypothèse *)
            htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
            hleft:constr;
            hright:constr;
            hflin:flin;
            hstrict:bool}
;;

(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
*)

exception NoIneq

let ineq1_of_constr (h,t) =
    match (kind_of_term t) with
      | App (f,args) ->
        (match kind_of_term f with
          | Const (c,_) when Array.length args = 2 ->
            let t1= args.(0) in
            let t2= args.(1) in
            (match (string_of_R_constant c) with
	      |"Rlt" -> [{hname=h;
                           htype="Rlt";
		           hleft=t1;
			   hright=t2;
			   hflin= flin_minus (flin_of_constr t1)
                                             (flin_of_constr t2);
			   hstrict=true}]
	      |"Rgt" -> [{hname=h;
                           htype="Rgt";
		           hleft=t2;
			   hright=t1;
			   hflin= flin_minus (flin_of_constr t2)
                                             (flin_of_constr t1);
			   hstrict=true}]
	      |"Rle" -> [{hname=h;
                           htype="Rle";
		           hleft=t1;
			   hright=t2;
			   hflin= flin_minus (flin_of_constr t1)
                                             (flin_of_constr t2);
			   hstrict=false}]
	      |"Rge" -> [{hname=h;
                           htype="Rge";
		           hleft=t2;
			   hright=t1;
			   hflin= flin_minus (flin_of_constr t2)
                                             (flin_of_constr t1);
			   hstrict=false}]
              |_-> raise NoIneq)
          | Ind ((kn,i),_) ->
            if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq;
            let t0= args.(0) in
            let t1= args.(1) in
            let t2= args.(2) in
	    (match (kind_of_term t0) with
              | Const (c,_) ->
		(match (string_of_R_constant c) with
		  | "R"->
                         [{hname=h;
                           htype="eqTLR";
		           hleft=t1;
			   hright=t2;
			   hflin= flin_minus (flin_of_constr t1)
                                             (flin_of_constr t2);
			   hstrict=false};
                          {hname=h;
                           htype="eqTRL";
		           hleft=t2;
			   hright=t1;
			   hflin= flin_minus (flin_of_constr t2)
                                             (flin_of_constr t1);
			   hstrict=false}]
                  |_-> raise NoIneq)
              |_-> raise NoIneq)
          |_-> raise NoIneq)
      |_-> raise NoIneq
;;

(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
*)

let fourier_lineq lineq1 =
   let nvar=ref (-1) in
   let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
   List.iter (fun f ->
		Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin
				nvar:=(!nvar)+1;
				Constrhash.add hvar x (!nvar)
			      end)
                  f.hflin.fhom)
             lineq1;
   let sys= List.map (fun h->
               let v=Array.make ((!nvar)+1) r0 in
               Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c)
                  h.hflin.fhom;
               ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
             lineq1 in
   unsolvable sys
;;

(*********************************************************************)
(* Defined constants *)

let get = Lazy.force
let cget = get
let eget c = EConstr.of_constr (Lazy.force c)
let constant = Coqlib.gen_constant "Fourier"

(* Standard library *)
open Coqlib
let coq_sym_eqT = lazy (build_coq_eq_sym ())
let coq_False = lazy (build_coq_False ())
let coq_not = lazy (build_coq_not ())
let coq_eq = lazy (build_coq_eq ())

(* Rdefinitions *)
let constant_real = constant ["Reals";"Rdefinitions"]

let coq_Rlt = lazy (constant_real "Rlt")
let coq_Rgt = lazy (constant_real "Rgt")
let coq_Rle = lazy (constant_real "Rle")
let coq_Rge = lazy (constant_real "Rge")
let coq_R = lazy (constant_real "R")
let coq_Rminus = lazy (constant_real "Rminus")
let coq_Rmult = lazy (constant_real "Rmult")
let coq_Rplus = lazy (constant_real "Rplus")
let coq_Ropp = lazy (constant_real "Ropp")
let coq_Rinv = lazy (constant_real "Rinv")
let coq_R0 = lazy (constant_real "R0")
let coq_R1 = lazy (constant_real "R1")

(* RIneq *)
let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1")

(* Fourier_util *)
let constant_fourier = constant ["fourier";"Fourier_util"]

let coq_Rlt_zero_1 = lazy (constant_fourier "Rlt_zero_1")
let coq_Rlt_zero_pos_plus1 = lazy (constant_fourier "Rlt_zero_pos_plus1")
let coq_Rle_zero_pos_plus1 = lazy (constant_fourier "Rle_zero_pos_plus1")
let coq_Rlt_mult_inv_pos = lazy (constant_fourier "Rlt_mult_inv_pos")
let coq_Rle_zero_zero = lazy (constant_fourier "Rle_zero_zero")
let coq_Rle_zero_1 = lazy (constant_fourier "Rle_zero_1")
let coq_Rle_mult_inv_pos = lazy (constant_fourier "Rle_mult_inv_pos")
let coq_Rnot_lt0 = lazy (constant_fourier "Rnot_lt0")
let coq_Rle_not_lt = lazy (constant_fourier "Rle_not_lt")
let coq_Rfourier_gt_to_lt = lazy (constant_fourier "Rfourier_gt_to_lt")
let coq_Rfourier_ge_to_le = lazy (constant_fourier "Rfourier_ge_to_le")
let coq_Rfourier_eqLR_to_le = lazy (constant_fourier "Rfourier_eqLR_to_le")
let coq_Rfourier_eqRL_to_le = lazy (constant_fourier "Rfourier_eqRL_to_le")

let coq_Rfourier_not_ge_lt = lazy (constant_fourier "Rfourier_not_ge_lt")
let coq_Rfourier_not_gt_le = lazy (constant_fourier "Rfourier_not_gt_le")
let coq_Rfourier_not_le_gt = lazy (constant_fourier "Rfourier_not_le_gt")
let coq_Rfourier_not_lt_ge = lazy (constant_fourier "Rfourier_not_lt_ge")
let coq_Rfourier_lt = lazy (constant_fourier "Rfourier_lt")
let coq_Rfourier_le = lazy (constant_fourier "Rfourier_le")
let coq_Rfourier_lt_lt = lazy (constant_fourier "Rfourier_lt_lt")
let coq_Rfourier_lt_le = lazy (constant_fourier "Rfourier_lt_le")
let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt")
let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le")
let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt")
let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le")
let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp")

(******************************************************************************
Construction de la preuve en cas de succès de la méthode de Fourier,
i.e. on obtient une contradiction.
*)
let is_int x = (x.den)=1
;;

(* fraction = couple (num,den) *)
let rational_to_fraction x= (x.num,x.den)
;;

(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
*)
let int_to_real n =
   let nn=abs n in
   if nn=0
   then get coq_R0
   else
     (let s=ref (get coq_R1) in
      for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
      if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s)
;;
(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
*)
let rational_to_real x =
   let (n,d)=rational_to_fraction x in
   mkApp (get coq_Rmult,
     [|int_to_real n;mkApp(get coq_Rinv,[|int_to_real d|])|])
;;

(* preuve que 0<n*1/d
*)
let tac_zero_inf_pos gl (n,d) =
  let get = eget in
   let tacn=ref (apply (get coq_Rlt_zero_1)) in
   let tacd=ref (apply (get coq_Rlt_zero_1)) in
   for _i = 1 to n - 1 do
       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
   for _i = 1 to d - 1 do
       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
   (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
;;

(* preuve que 0<=n*1/d
*)
let tac_zero_infeq_pos gl (n,d)=
  let get = eget in
   let tacn=ref (if n=0
                 then (apply (get coq_Rle_zero_zero))
                 else (apply (get coq_Rle_zero_1))) in
   let tacd=ref (apply (get coq_Rlt_zero_1)) in
   for  _i = 1 to n - 1 do
       tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
   for _i = 1 to d - 1 do
       tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
   (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
;;

(* preuve que 0<(-n)*(1/d) => False
*)
let tac_zero_inf_false gl (n,d) =
      let get = eget in
if n=0 then (apply (get coq_Rnot_lt0))
    else
     (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
	      (tac_zero_infeq_pos gl (-n,d)))
;;

(* preuve que 0<=(-n)*(1/d) => False
*)
let tac_zero_infeq_false gl (n,d) =
  let get = eget in
     (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
	      (tac_zero_inf_pos gl (-n,d)))
;;

let exact = exact_check;;

let tac_use h =
  let get = eget in
  let tac = exact (EConstr.of_constr h.hname) in
  match h.htype with
    "Rlt" -> tac
  |"Rle" -> tac
  |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
  |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
  |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
  |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
  |_->assert false
;;

(*
let is_ineq (h,t) =
    match (kind_of_term t) with
	App (f,args) ->
	  (match (string_of_R_constr f) with
	       "Rlt" -> true
	     | "Rgt" -> true
	     | "Rle" -> true
	     | "Rge" -> true
(* Wrong:not in Rdefinitions: *) | "eqT" ->
                (match (string_of_R_constr args.(0)) with
			     "R" -> true
			   | _ -> false)
             | _ ->false)
      |_->false
;;
*)

let list_of_sign s =
  let open Context.Named.Declaration in
  List.map (function LocalAssum (name, typ) -> name, typ
                   | LocalDef (name, _, typ) -> name, typ)
           s;;

let mkAppL a =
   let l = Array.to_list a in
   mkApp(List.hd l, Array.of_list (List.tl l))
;;

exception GoalDone

(* Résolution d'inéquations linéaires dans R *)
let rec fourier () =
  Proofview.Goal.nf_enter { enter = begin fun gl ->
    let concl = Proofview.Goal.concl gl in
    let sigma = Tacmach.New.project gl in
    Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
    let goal = Termops.strip_outer_cast sigma concl in
    let goal = EConstr.Unsafe.to_constr goal in
    let fhyp=Id.of_string "new_hyp_for_fourier" in
    (* si le but est une inéquation, on introduit son contraire,
       et le but à prouver devient False *)
    try 
      match (kind_of_term goal) with
      App (f,args) ->
      let get = eget in
      (match (string_of_R_constr f) with
	     "Rlt" ->
	       (Tacticals.New.tclTHEN
	         (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt))
			  (intro_using  fhyp))
		 (fourier ()))
	    |"Rle" ->
	     (Tacticals.New.tclTHEN
	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le))
		       (intro_using  fhyp))
			(fourier ()))
	    |"Rgt" ->
	     (Tacticals.New.tclTHEN
	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt))
		       (intro_using  fhyp))
	      (fourier ()))
	    |"Rge" ->
	     (Tacticals.New.tclTHEN
	      (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge))
		       (intro_using  fhyp))
	      (fourier ()))
	    |_-> raise GoalDone)
        |_-> raise GoalDone
     with GoalDone ->
    (* les hypothèses *)
    let hyps = List.map (fun (h,t)-> (mkVar h,t))
                        (list_of_sign (Proofview.Goal.hyps gl)) in
    let lineq =ref [] in
    List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
		        with NoIneq -> ())
              hyps;
    (* lineq = les inéquations découlant des hypothèses *)
    if !lineq=[] then CErrors.error "No inequalities";
    let res=fourier_lineq (!lineq) in
    let tac=ref (Proofview.tclUNIT ()) in
    if res=[]
    then CErrors.error "fourier failed"
    (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
    else (match res with
        [(cres,sres,lc)]->
    (* lc=coefficients multiplicateurs des inéquations
       qui donnent 0<cres ou 0<=cres selon sres *)
	(*print_string "Fourier's method can prove the goal...";flush stdout;*)
          let lutil=ref [] in
	  List.iter
            (fun (h,c) ->
			  if c<>r0
        		  then (lutil:=(h,c)::(!lutil)(*;
				print_rational(c);print_string " "*)))
                    (List.combine (!lineq) lc);
       (* on construit la combinaison linéaire des inéquation *)
             (match (!lutil) with
          (h1,c1)::lutil ->
	  let s=ref (h1.hstrict) in
	  let t1=ref (mkAppL [|get coq_Rmult;
	                  rational_to_real c1;
			  h1.hleft|]) in
	  let t2=ref (mkAppL [|get coq_Rmult;
	                  rational_to_real c1;
			  h1.hright|]) in
	  List.iter (fun (h,c) ->
	       s:=(!s)||(h.hstrict);
	       t1:=(mkAppL [|get coq_Rplus;
	                     !t1;
                             mkAppL [|get coq_Rmult;
                                      rational_to_real c;
			              h.hleft|] |]);
	       t2:=(mkAppL [|get coq_Rplus;
	                     !t2;
                             mkAppL [|get coq_Rmult;
                                      rational_to_real c;
			              h.hright|] |]))
               lutil;
          let ineq=mkAppL [|if (!s) then get coq_Rlt else get coq_Rle;
			      !t1;
			      !t2 |] in
	   let tc=rational_to_real cres in
       (* puis sa preuve *)
          let get = eget in
           let tac1=ref (if h1.hstrict
                         then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
                                 [tac_use h1;
                                  tac_zero_inf_pos  gl
                                      (rational_to_fraction c1)])
                         else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le))
                                 [tac_use h1;
				  tac_zero_inf_pos  gl
                                      (rational_to_fraction c1)])) in
           s:=h1.hstrict;
           List.iter (fun (h,c)->
             (if (!s)
	      then (if h.hstrict
	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt))
			       [!tac1;tac_use h;
			        tac_zero_inf_pos  gl
                                      (rational_to_fraction c)])
	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le))
			       [!tac1;tac_use h;
			        tac_zero_inf_pos  gl
                                      (rational_to_fraction c)]))
	      else (if h.hstrict
	            then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt))
			       [!tac1;tac_use h;
			        tac_zero_inf_pos  gl
                                      (rational_to_fraction c)])
	            else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le))
			       [!tac1;tac_use h;
			        tac_zero_inf_pos  gl
                                      (rational_to_fraction c)])));
	     s:=(!s)||(h.hstrict))
              lutil;
           let tac2= if sres
                      then tac_zero_inf_false gl (rational_to_fraction cres)
                      else tac_zero_infeq_false gl (rational_to_fraction cres)
           in
           tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq))
                     [Tacticals.New.tclTHEN (change_concl
			       (EConstr.of_constr (mkAppL [| cget coq_not; ineq|]
				       )))
		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
					       else get coq_Rnot_le_le))
			    (Tacticals.New.tclTHENS (Equality.replace
				       (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|]
					       ))
				       (EConstr.of_constr tc))
		 	       [tac2;
                                (Tacticals.New.tclTHENS
				  (Equality.replace
				    (EConstr.of_constr (mkApp (cget coq_Rinv,
				      [|cget coq_R1|])))
				    (get coq_R1))
(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)

      			        [Tacticals.New.tclORELSE
                                   (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
                                   (Proofview.tclUNIT ());
				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
					  (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq))
						(apply (get coq_Rinv_1))))]

					 )
				]));
                       !tac1]);
	   tac:=(Tacticals.New.tclTHENS (cut (get coq_False))
				  [Tacticals.New.tclTHEN intro (contradiction None);
				   !tac])
      |_-> assert false) |_-> assert false
	  );
(*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
      !tac
(*      ((tclABSTRACT None !tac) gl) *)
  end }
;;

(*
let fourier_tac x gl =
     fourier gl
;;

let v_fourier = add_tactic "Fourier" fourier_tac
*)