From d64cc26e9b740fb375f46f6d9e39d42802db3ff7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 11 Nov 2002 12:03:10 +0000 Subject: [PATCH] An old bug in 'eqT' hipotesys solved --- helm/gTopLevel/esempi/fourier.cic | 20 +++++++++++++++++++- helm/gTopLevel/fourierR.ml | 15 ++++++++++----- 2 files changed, 29 insertions(+), 6 deletions(-) diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic index a76b4586a..dc883e4e4 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier.cic @@ -6,10 +6,13 @@ 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 Rmult /Coq/Reals/Rdefinitions/Rmult.con alias R1 /Coq/Reals/Rdefinitions/R1.con alias R0 /Coq/Reals/Rdefinitions/R0.con alias R /Coq/Reals/Rdefinitions/R.con alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 +alias not /Coq/Init/Logic/not.con + //test base1 ok !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) @@ -20,13 +23,28 @@ alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 //test base3 ok !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1))) +/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con + +/Coq/Init/Logic/False.ind#1/1 + +(Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))) + +/Coq/fourier/Fourier_util/Rnot_le_le.con + +t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) +t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) +tc=(Rmult (Ropp R1) (Rinv R1)) + +rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) + (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv 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 (fourier fails) +//test base6 ok !x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) //test base7 (should fail) ok diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 66e895119..90657b598 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -394,7 +394,7 @@ 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" -> + "cic:/Coq/Init/Logic_Type/eqT.ind" -> let t0= arg1 in let arg1= arg2 in let arg2= List.hd(List.tl (List.tl next)) in @@ -762,6 +762,9 @@ let my_cut ~term:c ~status:(proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +debug("my_cut di "^CicPp.ppterm c^"\n"); + + let fresh_meta = ProofEngineHelpers.new_meta proof in let irl = ProofEngineHelpers.identity_relocation_list_for_metavariable context in @@ -923,7 +926,7 @@ let assumption_tac ~status:(proof,goal)= (* !!!!! fix !!!!!!!!!! *) let contradiction_tac ~status:(proof,goal)= Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) ~continuation:(Tacticals.then_ ~start:(Ring.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) @@ -1138,7 +1141,7 @@ theoreme,so let's parse our thesis *) in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) - ~continuations:[Tacticals.then_ + ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)Tacticals.then_ ~start:(fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) @@ -1151,6 +1154,7 @@ theoreme,so let's parse our thesis *) ~continuation:(Tacticals.thens ~start:( fun ~status -> + debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc ~status in @@ -1214,12 +1218,13 @@ theoreme,so let's parse our thesis *) ) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) - tac:=(Tacticals.thens + (*tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False) ~continuations:[Tacticals.then_ ~start:(PrimitiveTactics.intros_tac ~name:"??") ~continuation:contradiction_tac - ;!tac]) + ;!tac])*) + tac:=!tac |_-> assert false)(*match (!lutil) *) -- 2.39.2