1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
29 des inéquations et équations sont entiers. En attendant la tactique Field.
32 (*open Term // in coq/kernel
39 (******************************************************************************
40 Operations on linear combinations.
42 Opérations sur les combinaisons linéaires affines.
43 La partie homogène d'une combinaison linéaire est en fait une table de hash
44 qui donne le coefficient d'un terme du calcul des constructions,
45 qui est zéro si le terme n'y est pas.
51 The type for linear combinations
53 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
59 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
65 @return the rational associated with x (coefficient)
69 (Hashtbl.find f.fhom x)
75 Adds c to the coefficient of x
82 let cx = flin_coef f x in
83 Hashtbl.remove f.fhom x;
84 Hashtbl.add f.fhom x (rplus cx c);
93 let flin_add_cste f c =
95 fcste=rplus f.fcste c}
99 @return a empty flin with r1 in fcste
101 let flin_one () = flin_add_cste (flin_zero()) r1;;
106 let flin_plus f1 f2 =
107 let f3 = flin_zero() in
108 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
109 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
110 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
116 let flin_minus f1 f2 =
117 let f3 = flin_zero() in
118 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
119 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
120 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
127 let f2 = flin_zero() in
128 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
129 flin_add_cste f2 (rmult a f.fcste);
133 (*****************************************************************************)
138 @return proiection on string of t
140 let rec string_of_term t =
142 Cic.Cast (t1,t2) -> string_of_term t1
143 |Cic.Const (u,boh) -> UriManager.string_of_uri u
144 |Cic.Var (u) -> UriManager.string_of_uri u
145 | _ -> "not_of_constant"
149 let string_of_constr = string_of_term
155 @raise Failure if conversion is impossible
156 @return rational proiection of t
158 let rec rational_of_term t =
159 (* fun to apply f to the first and second rational-term of l *)
160 let rat_of_binop f l =
161 let a = List.hd l and
162 b = List.hd(List.tl l) in
163 f (rational_of_term a) (rational_of_term b)
165 (* as before, but f is unary *)
166 let rat_of_unop f l =
167 f (rational_of_term (List.hd l))
170 | Cic.Cast (t1,t2) -> (rational_of_term t1)
171 | Cic.Appl (t1::next) ->
174 (match (UriManager.string_of_uri u) with
175 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
177 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
178 rat_of_unop rinv next
179 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
180 rat_of_binop rmult next
181 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
182 rat_of_binop rdiv next
183 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
184 rat_of_binop rplus next
185 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
186 rat_of_binop rminus next
187 | _ -> failwith "not a rational")
188 | _ -> failwith "not a rational")
189 | Cic.Const (u,boh) ->
190 (match (UriManager.string_of_uri u) with
191 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
192 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
193 | _ -> failwith "not a rational")
194 | _ -> failwith "not a rational"
198 let rational_of_const = rational_of_term;;
202 let rec flin_of_term t =
203 let fl_of_binop f l =
204 let a = List.hd l and
205 b = List.hd(List.tl l) in
206 f (flin_of_term a) (flin_of_term b)
210 | Cic.Cast (t1,t2) -> (flin_of_term t1)
211 | Cic.Appl (t1::next) ->
216 match (UriManager.string_of_uri u) with
217 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
218 flin_emult (rop r1) (flin_of_term (List.hd next))
219 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
220 fl_of_binop flin_plus next
221 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
222 fl_of_binop flin_minus next
223 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
225 let arg1 = (List.hd next) and
226 arg2 = (List.hd(List.tl next))
230 let a = rational_of_term arg1 in
233 let b = (rational_of_term arg2) in
234 (flin_add_cste (flin_zero()) (rmult a b))
237 _ -> (flin_add (flin_zero()) arg2 a)
240 _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
242 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
243 let a=(rational_of_term (List.hd next)) in
244 flin_add_cste (flin_zero()) (rinv a)
245 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
247 let b=(rational_of_term (List.hd(List.tl next))) in
250 let a = (rational_of_term (List.hd next)) in
251 (flin_add_cste (flin_zero()) (rdiv a b))
254 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
260 | Cic.Const (u,boh) ->
262 match (UriManager.string_of_uri u) with
263 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
264 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
268 with _ -> flin_add (flin_zero()) t r1
272 let flin_of_constr = flin_of_term;;
276 Translates a flin to (c,x) list
278 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
280 let flin_to_alist f =
282 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
286 (* Représentation des hypothèses qui sont des inéquations ou des équations.
290 The structure for ineq
292 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
293 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
300 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
303 let ineq1_of_term (h,t) =
305 Cic.Appl (t1::next) ->
306 let arg1= List.hd next in
307 let arg2= List.hd(List.tl next) in
310 (match UriManager.string_of_uri u with
311 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
315 hflin= flin_minus (flin_of_term arg1)
318 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
322 hflin= flin_minus (flin_of_term arg2)
325 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
329 hflin= flin_minus (flin_of_term arg1)
332 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
336 hflin= flin_minus (flin_of_term arg2)
340 | Cic.MutInd (u,i,o) ->
341 (match UriManager.string_of_uri u with
342 "cic:/Coq/Init/Logic_Type/eqT.con" ->
345 let arg2= List.hd(List.tl (List.tl next)) in
348 (match UriManager.string_of_uri u with
349 "cic:/Coq/Reals/Rdefinitions/R.con"->
354 hflin= flin_minus (flin_of_term arg1)
361 hflin= flin_minus (flin_of_term arg2)
371 let ineq1_of_constr = ineq1_of_term;;
374 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
377 let fourier_lineq lineq1 =
379 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
381 Hashtbl.iter (fun x c ->
382 try (Hashtbl.find hvar x;())
383 with _-> nvar:=(!nvar)+1;
384 Hashtbl.add hvar x (!nvar))
387 let sys= List.map (fun h->
388 let v=Array.create ((!nvar)+1) r0 in
389 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
391 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
396 (******************************************************************************
397 Construction de la preuve en cas de succès de la méthode de Fourier,
398 i.e. on obtient une contradiction.
401 let is_int x = (x.den)=1
404 (* fraction = couple (num,den) *)
405 let rec rational_to_fraction x= (x.num,x.den)
408 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
416 for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
417 if n<0 then s:="(Ropp "^(!s)^")";
420 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
422 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
423 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
424 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
427 let rec int_to_real_aux n =
429 0 -> _R0 (* o forse R0 + R0 ????? *)
430 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
435 let x = int_to_real_aux (abs n) in
437 Cic.Appl [ _Ropp ; x ]
443 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
445 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
446 let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
449 let rational_to_real x =
450 let (n,d)=rational_to_fraction x in
451 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
454 (* preuve que 0<n*1/d
457 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
459 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
461 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
464 let tac_zero_inf_pos gl (n,d) =
465 (*let cste = pf_parse_constr gl in*)
466 let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
467 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
469 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
471 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
472 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
475 (* preuve que 0<=n*1/d
477 (*let tac_zero_infeq_pos gl (n,d)=
478 let cste = pf_parse_constr gl in
480 then (apply (cste "Rle_zero_zero"))
481 else (apply (cste "Rle_zero_1"))) in
482 let tacd=ref (apply (cste "Rlt_zero_1")) in
484 tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
486 tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
487 (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
490 (* preuve que 0<(-n)*(1/d) => False
492 (*let tac_zero_inf_false gl (n,d) =
493 let cste = pf_parse_constr gl in
494 if n=0 then (apply (cste "Rnot_lt0"))
496 (tclTHEN (apply (cste "Rle_not_lt"))
497 (tac_zero_infeq_pos gl (-n,d)))
500 (* preuve que 0<=(-n)*(1/d) => False
502 (*let tac_zero_infeq_false gl (n,d) =
503 let cste = pf_parse_constr gl in
504 (tclTHEN (apply (cste "Rlt_not_le"))
505 (tac_zero_inf_pos gl (-n,d)))
508 let create_meta () = mkMeta(new_meta());;
511 let concl = pf_concl gl in
512 apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
514 let exact = exact_check;;
516 let tac_use h = match h.htype with
517 "Rlt" -> exact h.hname
518 |"Rle" -> exact h.hname
519 |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
521 |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
523 |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
525 |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
531 match (kind_of_term t) with
533 (match (string_of_constr f) with
534 "Coq.Reals.Rdefinitions.Rlt" -> true
535 |"Coq.Reals.Rdefinitions.Rgt" -> true
536 |"Coq.Reals.Rdefinitions.Rle" -> true
537 |"Coq.Reals.Rdefinitions.Rge" -> true
538 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
539 "Coq.Reals.Rdefinitions.R"->true
545 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
548 let l = Array.to_list a in
549 mkApp(List.hd l, Array.of_list (List.tl l))
552 (* Résolution d'inéquations linéaires dans R *)
556 let parse = pf_parse_constr gl in
557 let goal = strip_outer_cast (pf_concl gl) in
558 let fhyp=id_of_string "new_hyp_for_fourier" in
559 (* si le but est une inéquation, on introduit son contraire,
560 et le but à prouver devient False *)
562 match (kind_of_term goal) with
564 (match (string_of_constr f) with
565 "Coq.Reals.Rdefinitions.Rlt" ->
567 (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
570 |"Coq.Reals.Rdefinitions.Rle" ->
572 (tclTHEN (apply (parse "Rfourier_not_gt_le"))
575 |"Coq.Reals.Rdefinitions.Rgt" ->
577 (tclTHEN (apply (parse "Rfourier_not_le_gt"))
580 |"Coq.Reals.Rdefinitions.Rge" ->
582 (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
593 let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
594 (list_of_sign (pf_hyps gl)) in
596 List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
601 (* lineq = les inéquations découlant des hypothèses *)
605 let res=fourier_lineq (!lineq) in
606 let tac=ref tclIDTAC in
608 then (print_string "Tactic Fourier fails.\n";
612 (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
618 (* lc=coefficients multiplicateurs des inéquations
619 qui donnent 0<cres ou 0<=cres selon sres *)
620 (*print_string "Fourier's method can prove the goal...";flush stdout;*)
628 then (lutil:=(h,c)::(!lutil)(*;
629 print_rational(c);print_string " "*)))
630 (List.combine (!lineq) lc);
633 (* on construit la combinaison linéaire des inéquation *)
638 let s=ref (h1.hstrict) in
639 let t1=ref (mkAppL [|parse "Rmult";
640 parse (rational_to_real c1);
642 let t2=ref (mkAppL [|parse "Rmult";
643 parse (rational_to_real c1);
645 List.iter (fun (h,c) ->
646 s:=(!s)||(h.hstrict);
647 t1:=(mkAppL [|parse "Rplus";
649 mkAppL [|parse "Rmult";
650 parse (rational_to_real c);
652 t2:=(mkAppL [|parse "Rplus";
654 mkAppL [|parse "Rmult";
655 parse (rational_to_real c);
658 let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
661 let tc=parse (rational_to_real cres) in
665 let tac1=ref (if h1.hstrict
666 then (tclTHENS (apply (parse "Rfourier_lt"))
669 (rational_to_fraction c1)])
670 else (tclTHENS (apply (parse "Rfourier_le"))
673 (rational_to_fraction c1)])) in
675 List.iter (fun (h,c)->
678 then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
681 (rational_to_fraction c)])
682 else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
685 (rational_to_fraction c)]))
687 then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
690 (rational_to_fraction c)])
691 else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
694 (rational_to_fraction c)])));
695 s:=(!s)||(h.hstrict))
698 then tac_zero_inf_false gl (rational_to_fraction cres)
699 else tac_zero_infeq_false gl (rational_to_fraction cres)
701 tac:=(tclTHENS (my_cut ineq)
702 [tclTHEN (change_in_concl
703 (mkAppL [| parse "not"; ineq|]
705 (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
706 else parse "Rnot_le_le"))
707 (tclTHENS (Equality.replace
708 (mkAppL [|parse "Rminus";!t2;!t1|]
712 (tclTHENS (Equality.replace (parse "(Rinv R1)")
715 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
720 (tclTHEN (apply (parse "sym_eqT"))
721 (apply (parse "Rinv_R1")))]
726 tac:=(tclTHENS (cut (parse "False"))
727 [tclTHEN intro contradiction;
729 |_-> assert false) |_-> assert false
731 ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
733 ((tclABSTRACT None !tac) gl)
737 let fourier_tac x gl =
741 let v_fourier = add_tactic "Fourier" fourier_tac
744 (*open CicReduction*)
745 (*open PrimitiveTactics*)
746 (*open ProofEngineTypes*)
747 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;