From: Enrico Tassi Date: Mon, 4 Nov 2002 09:26:10 +0000 (+0000) Subject: bug found: X-Git-Tag: V_0_0_3~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a19c0a69c65ecdb695315d79b1a9b3e037aba9ad;p=helm.git bug found: - >= is splitted in > or = ,so unification fails --- diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic index cae3925a7..09caea79b 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier.cic @@ -1,8 +1,35 @@ alias Rge /Coq/Reals/Rdefinitions/Rge.con alias Rle /Coq/Reals/Rdefinitions/Rle.con +alias Rgt /Coq/Reals/Rdefinitions/Rgt.con +alias Rlt /Coq/Reals/Rdefinitions/Rlt.con +alias Ropp /Coq/Reals/Rdefinitions/Ropp.con +alias Rinv /Coq/Reals/Rdefinitions/Rinv.con alias Rplus /Coq/Reals/Rdefinitions/Rplus.con alias Rminus /Coq/Reals/Rdefinitions/Rminus.con alias R1 /Coq/Reals/Rdefinitions/R1.con +alias R0 /Coq/Reals/Rdefinitions/R0.con alias R /Coq/Reals/Rdefinitions/R.con +alias Eq /Coq/Init/Logic_Type/eqT.ind#1/1 +//test base1 ok !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) + +//test base2 ok +!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1)) + +//test base3 (unification fails) +!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1))) + +//test base4 ok +!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1)) + +//test base5 ok +!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0)) + +//test base6 (unification fails) +!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) + +//test base7 (should fail) ok +!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1)) + + diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index c23cc448d..a4630ab7a 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -31,7 +31,9 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = let module U = UriManager in let curi,metasenv,pbo,pty = proof in let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in - let eq_ind_r,ty,t1,t2 = + + prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n"); + let eq_ind_r,ty,t1,t2 = match CicTypeChecker.type_of_aux' metasenv context equality with C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") -> @@ -79,6 +81,8 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); (proof',[fresh_meta]) ;; +(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*) + let simpl_tac ~status:(proof,goal) = @@ -391,6 +395,7 @@ type hineq={hname:Cic.term; (* le nom de l'hypoth *) let ineq1_of_term (h,t) = + debug("Trasformo in ineq "^CicPp.ppterm t^"\n"); match t with (* match t *) Cic.Appl (t1::next) -> let arg1= List.hd next in @@ -433,14 +438,16 @@ let ineq1_of_term (h,t) = |_->assert false)(* match u *) | Cic.MutInd (u,i,o) -> (match UriManager.string_of_uri u with - "cic:/Coq/Init/Logic_Type/eqT.con" -> - let t0= arg1 in + "cic:/Coq/Init/Logic_Type/eqT.ind" -> + debug("Ho trovato una ==\n"); + let t0= arg1 in let arg1= arg2 in let arg2= List.hd(List.tl (List.tl next)) in (match t0 with Cic.Const (u,boh) -> (match UriManager.string_of_uri u with "cic:/Coq/Reals/Rdefinitions/R.con"-> + [{hname=h; htype="eqTLR"; hleft=arg1; @@ -455,11 +462,11 @@ let ineq1_of_term (h,t) = hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); hstrict=false}] - |_-> assert false) - |_-> assert false) - |_-> assert false) - |_-> assert false)(* match t1 *) - |_-> assert false (* match t *) + |_-> debug("eqT deve essere applicato a const R\n");assert false) + |_-> debug("eqT deve essere appl a const\n");assert false) + |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false) + |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *) + |_-> debug("Il termine non e' una applicazione\n");assert false (* match t *) ;; (* coq wrapper let ineq1_of_constr = ineq1_of_term;; @@ -741,13 +748,19 @@ let tac_zero_inf_false gl (n,d) ~status= (* preuve que 0<=(-n)*(1/d) => False *) -let tac_zero_infeq_false gl (n,d) ~status= -debug("stat tac_zero_infeq_false"); -let r = - (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) +let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= +debug("stat tac_zero_infeq_false\n"); +(*let r = + ( + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + + debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); + Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) ~continuation:(tac_zero_inf_pos (-n,d))) ~status in - debug("stat tac_zero_infeq_false"); - r + debug("end tac_zero_infeq_false\n"); + r*) + Ring.id_tac ~status ;; @@ -901,7 +914,7 @@ debug("inizio EQ\n"); let irl = ProofEngineHelpers.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in -debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); +debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n"); let (proof,goals) = rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ~status:((curi,metasenv',pbo,pty),goal) @@ -1010,7 +1023,7 @@ theoreme,so let's parse our thesis *) (* transform hyps into inequations *) List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) - with _-> ()) + with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");) hyps; @@ -1021,7 +1034,7 @@ theoreme,so let's parse our thesis *) let tac=ref Ring.id_tac in if res=[] then (print_string "Tactic Fourier fails.\n";flush stdout; - failwith "fourier_tac fails") + failwith "fourier can't proove it") else ( match res with (*match res*) @@ -1176,7 +1189,8 @@ theoreme,so let's parse our thesis *) r) ~continuations:[(Tacticals.thens ~start:( - fun ~status -> + fun ~status:(proof,goals as status) -> + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in (match r with (p,gl) -> debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); @@ -1218,6 +1232,7 @@ theoreme,so let's parse our thesis *) goal) metasenv in (* check if ty is of type *) let w1 = + debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); (match ty with (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*) Cic.Prod (Cic.Anonimous,a,b) -> (Cic.Appl [_not;a]) @@ -1227,8 +1242,8 @@ theoreme,so let's parse our thesis *) debug("fine MY_CHNGE\n"); r ) - ~continuation:tac2])) - ;!tac1]);(*end tac:=*) + ~continuation:Ring.id_tac(*tac2*)])) + ;Ring.id_tac(*!tac1*)]);(*end tac:=*) tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False) ~continuations:[Tacticals.then_