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.
39 (******************************************************************************
40 Opérations sur les combinaisons linéaires affines.
41 La partie homogène d'une combinaison linéaire est en fait une table de hash
42 qui donne le coefficient d'un terme du calcul des constructions,
43 qui est zéro si le terme n'y est pas.
46 (*type flin = {fhom:(constr , rational)Hashtbl.t;
49 let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};;
51 let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;;
54 let cx = flin_coef f x in
55 Hashtbl.remove f.fhom x;
56 Hashtbl.add f.fhom x (rplus cx c);
59 let flin_add_cste f c =
61 fcste=rplus f.fcste c}
64 let flin_one () = flin_add_cste (flin_zero()) r1;;
67 let f3 = flin_zero() in
68 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
69 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
70 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
73 let flin_minus f1 f2 =
74 let f3 = flin_zero() in
75 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
76 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
77 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
80 let f2 = flin_zero() in
81 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
82 flin_add_cste f2 (rmult a f.fcste);
85 (*****************************************************************************)
86 (*let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;;
87 let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
88 let pf_parse_constr gl s =
89 Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
91 let rec string_of_constr c =
92 match kind_of_term c with
93 Cast (c,t) -> string_of_constr c
94 |Const c -> string_of_path c
95 |Var(c) -> string_of_id c
96 | _ -> "not_of_constant"
99 let rec rational_of_constr c =
100 match kind_of_term c with
101 | Cast (c,t) -> (rational_of_constr c)
103 (match kind_of_term c with
105 (match (string_of_path c) with
106 "Coq.Reals.Rdefinitions.Ropp" ->
107 rop (rational_of_constr args.(0))
108 |"Coq.Reals.Rdefinitions.Rinv" ->
109 rinv (rational_of_constr args.(0))
110 |"Coq.Reals.Rdefinitions.Rmult" ->
111 rmult (rational_of_constr args.(0))
112 (rational_of_constr args.(1))
113 |"Coq.Reals.Rdefinitions.Rdiv" ->
114 rdiv (rational_of_constr args.(0))
115 (rational_of_constr args.(1))
116 |"Coq.Reals.Rdefinitions.Rplus" ->
117 rplus (rational_of_constr args.(0))
118 (rational_of_constr args.(1))
119 |"Coq.Reals.Rdefinitions.Rminus" ->
120 rminus (rational_of_constr args.(0))
121 (rational_of_constr args.(1))
122 | _ -> failwith "not a rational")
123 | _ -> failwith "not a rational")
125 (match (string_of_path c) with
126 "Coq.Reals.Rdefinitions.R1" -> r1
127 |"Coq.Reals.Rdefinitions.R0" -> r0
128 | _ -> failwith "not a rational")
129 | _ -> failwith "not a rational"
132 let rec flin_of_constr c =
134 match kind_of_term c with
135 | Cast (c,t) -> (flin_of_constr c)
137 (match kind_of_term c with
139 (match (string_of_path c) with
140 "Coq.Reals.Rdefinitions.Ropp" ->
141 flin_emult (rop r1) (flin_of_constr args.(0))
142 |"Coq.Reals.Rdefinitions.Rplus"->
143 flin_plus (flin_of_constr args.(0))
144 (flin_of_constr args.(1))
145 |"Coq.Reals.Rdefinitions.Rminus"->
146 flin_minus (flin_of_constr args.(0))
147 (flin_of_constr args.(1))
148 |"Coq.Reals.Rdefinitions.Rmult"->
149 (try (let a=(rational_of_constr args.(0)) in
150 try (let b = (rational_of_constr args.(1)) in
151 (flin_add_cste (flin_zero()) (rmult a b)))
152 with _-> (flin_add (flin_zero())
155 with _-> (flin_add (flin_zero())
157 (rational_of_constr args.(1))))
158 |"Coq.Reals.Rdefinitions.Rinv"->
159 let a=(rational_of_constr args.(0)) in
160 flin_add_cste (flin_zero()) (rinv a)
161 |"Coq.Reals.Rdefinitions.Rdiv"->
162 (let b=(rational_of_constr args.(1)) in
163 try (let a = (rational_of_constr args.(0)) in
164 (flin_add_cste (flin_zero()) (rdiv a b)))
165 with _-> (flin_add (flin_zero())
171 (match (string_of_path c) with
172 "Coq.Reals.Rdefinitions.R1" -> flin_one ()
173 |"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
176 with _ -> flin_add (flin_zero())
181 let flin_to_alist f =
183 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
187 (* Représentation des hypothèses qui sont des inéquations ou des équations.
189 (*type hineq={hname:constr; (* le nom de l'hypothèse *)
190 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
197 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
199 (*let ineq1_of_constr (h,t) =
200 match (kind_of_term t) with
204 (match kind_of_term f with
206 (match (string_of_path c) with
207 "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
211 hflin= flin_minus (flin_of_constr t1)
214 |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h;
218 hflin= flin_minus (flin_of_constr t2)
221 |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h;
225 hflin= flin_minus (flin_of_constr t1)
228 |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h;
232 hflin= flin_minus (flin_of_constr t2)
237 (match (string_of_path sp) with
238 "Coq.Init.Logic_Type.eqT" -> let t0= args.(0) in
241 (match (kind_of_term t0) with
243 (match (string_of_path c) with
244 "Coq.Reals.Rdefinitions.R"->
249 hflin= flin_minus (flin_of_constr t1)
256 hflin= flin_minus (flin_of_constr t2)
266 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
269 (*let fourier_lineq lineq1 =
271 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
273 Hashtbl.iter (fun x c ->
274 try (Hashtbl.find hvar x;())
275 with _-> nvar:=(!nvar)+1;
276 Hashtbl.add hvar x (!nvar))
279 let sys= List.map (fun h->
280 let v=Array.create ((!nvar)+1) r0 in
281 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
283 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
288 (******************************************************************************
289 Construction de la preuve en cas de succès de la méthode de Fourier,
290 i.e. on obtient une contradiction.
293 (*let is_int x = (x.den)=1
296 (* fraction = couple (num,den) *)
297 (*let rec rational_to_fraction x= (x.num,x.den)
300 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
302 (*let int_to_real n =
308 for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
309 if n<0 then s:="(Ropp "^(!s)^")";
312 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
314 (*let rational_to_real x =
315 let (n,d)=rational_to_fraction x in
316 ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
319 (* preuve que 0<n*1/d
321 (*let tac_zero_inf_pos gl (n,d) =
322 let cste = pf_parse_constr gl in
323 let tacn=ref (apply (cste "Rlt_zero_1")) in
324 let tacd=ref (apply (cste "Rlt_zero_1")) in
326 tacn:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacn); done;
328 tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
329 (tclTHENS (apply (cste "Rlt_mult_inv_pos")) [!tacn;!tacd])
332 (* preuve que 0<=n*1/d
334 (*let tac_zero_infeq_pos gl (n,d)=
335 let cste = pf_parse_constr gl in
337 then (apply (cste "Rle_zero_zero"))
338 else (apply (cste "Rle_zero_1"))) in
339 let tacd=ref (apply (cste "Rlt_zero_1")) in
341 tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
343 tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
344 (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
347 (* preuve que 0<(-n)*(1/d) => False
349 (*let tac_zero_inf_false gl (n,d) =
350 let cste = pf_parse_constr gl in
351 if n=0 then (apply (cste "Rnot_lt0"))
353 (tclTHEN (apply (cste "Rle_not_lt"))
354 (tac_zero_infeq_pos gl (-n,d)))
357 (* preuve que 0<=(-n)*(1/d) => False
359 (*let tac_zero_infeq_false gl (n,d) =
360 let cste = pf_parse_constr gl in
361 (tclTHEN (apply (cste "Rlt_not_le"))
362 (tac_zero_inf_pos gl (-n,d)))
365 let create_meta () = mkMeta(new_meta());;
368 let concl = pf_concl gl in
369 apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
371 let exact = exact_check;;
373 let tac_use h = match h.htype with
374 "Rlt" -> exact h.hname
375 |"Rle" -> exact h.hname
376 |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
378 |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
380 |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
382 |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
388 match (kind_of_term t) with
390 (match (string_of_constr f) with
391 "Coq.Reals.Rdefinitions.Rlt" -> true
392 |"Coq.Reals.Rdefinitions.Rgt" -> true
393 |"Coq.Reals.Rdefinitions.Rle" -> true
394 |"Coq.Reals.Rdefinitions.Rge" -> true
395 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
396 "Coq.Reals.Rdefinitions.R"->true
402 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
405 let l = Array.to_list a in
406 mkApp(List.hd l, Array.of_list (List.tl l))
409 (* Résolution d'inéquations linéaires dans R *)
413 let parse = pf_parse_constr gl in
414 let goal = strip_outer_cast (pf_concl gl) in
415 let fhyp=id_of_string "new_hyp_for_fourier" in
416 (* si le but est une inéquation, on introduit son contraire,
417 et le but à prouver devient False *)
419 match (kind_of_term goal) with
421 (match (string_of_constr f) with
422 "Coq.Reals.Rdefinitions.Rlt" ->
424 (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
427 |"Coq.Reals.Rdefinitions.Rle" ->
429 (tclTHEN (apply (parse "Rfourier_not_gt_le"))
432 |"Coq.Reals.Rdefinitions.Rgt" ->
434 (tclTHEN (apply (parse "Rfourier_not_le_gt"))
437 |"Coq.Reals.Rdefinitions.Rge" ->
439 (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
450 let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
451 (list_of_sign (pf_hyps gl)) in
453 List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
458 (* lineq = les inéquations découlant des hypothèses *)
462 let res=fourier_lineq (!lineq) in
463 let tac=ref tclIDTAC in
465 then (print_string "Tactic Fourier fails.\n";
469 (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
475 (* lc=coefficients multiplicateurs des inéquations
476 qui donnent 0<cres ou 0<=cres selon sres *)
477 (*print_string "Fourier's method can prove the goal...";flush stdout;*)
485 then (lutil:=(h,c)::(!lutil)(*;
486 print_rational(c);print_string " "*)))
487 (List.combine (!lineq) lc);
490 (* on construit la combinaison linéaire des inéquation *)
495 let s=ref (h1.hstrict) in
496 let t1=ref (mkAppL [|parse "Rmult";
497 parse (rational_to_real c1);
499 let t2=ref (mkAppL [|parse "Rmult";
500 parse (rational_to_real c1);
502 List.iter (fun (h,c) ->
503 s:=(!s)||(h.hstrict);
504 t1:=(mkAppL [|parse "Rplus";
506 mkAppL [|parse "Rmult";
507 parse (rational_to_real c);
509 t2:=(mkAppL [|parse "Rplus";
511 mkAppL [|parse "Rmult";
512 parse (rational_to_real c);
515 let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
518 let tc=parse (rational_to_real cres) in
522 let tac1=ref (if h1.hstrict
523 then (tclTHENS (apply (parse "Rfourier_lt"))
526 (rational_to_fraction c1)])
527 else (tclTHENS (apply (parse "Rfourier_le"))
530 (rational_to_fraction c1)])) in
532 List.iter (fun (h,c)->
535 then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
538 (rational_to_fraction c)])
539 else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
542 (rational_to_fraction c)]))
544 then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
547 (rational_to_fraction c)])
548 else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
551 (rational_to_fraction c)])));
552 s:=(!s)||(h.hstrict))
555 then tac_zero_inf_false gl (rational_to_fraction cres)
556 else tac_zero_infeq_false gl (rational_to_fraction cres)
558 tac:=(tclTHENS (my_cut ineq)
559 [tclTHEN (change_in_concl
560 (mkAppL [| parse "not"; ineq|]
562 (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
563 else parse "Rnot_le_le"))
564 (tclTHENS (Equality.replace
565 (mkAppL [|parse "Rminus";!t2;!t1|]
569 (tclTHENS (Equality.replace (parse "(Rinv R1)")
572 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
577 (tclTHEN (apply (parse "sym_eqT"))
578 (apply (parse "Rinv_R1")))]
583 tac:=(tclTHENS (cut (parse "False"))
584 [tclTHEN intro contradiction;
586 |_-> assert false) |_-> assert false
588 ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
590 ((tclABSTRACT None !tac) gl)
594 let fourier_tac x gl =
598 let v_fourier = add_tactic "Fourier" fourier_tac
601 (*open CicReduction*)
602 (*open PrimitiveTactics*)
603 (*open ProofEngineTypes*)
604 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;