From 04f0e78400f9848f08f5ef194c02002e2c2c75c7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 9 Oct 2002 17:28:02 +0000 Subject: [PATCH] Several bug-fixes: - apply_tac and my_cut used to generate a new metavariable without updating the metasenv - a boolean "false" was used in place of the propositional "False" - minor fixes The equality_replace tactic is completely wrong. For now the whole proof branch that needs it is commented out. Open bugs: Some unification problem in the proof that the linear combination can be derived from the initial disequations. --- helm/gTopLevel/fourierR.ml | 65 ++++++++++++++++++++++++++++---------- 1 file changed, 49 insertions(+), 16 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 585513e59..446b2ef4b 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -428,6 +428,7 @@ Construction de la preuve en cas de succ i.e. on obtient une contradiction. *) +let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;; let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;; let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;; let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;; @@ -436,7 +437,7 @@ let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_ let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;; let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;; let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;; -let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;; +let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;; let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;; let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;; let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;; @@ -470,7 +471,7 @@ let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;; let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;; -let _False = Cic.MutConstruct(UriManager.uri_of_string "cic:/Coq/Init/Datatypes/bool.ind") 0 1 0 ;; +let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;; let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;; @@ -575,16 +576,18 @@ let tac_zero_infeq_false gl (n,d) = (* *********** ********** ******** ??????????????? *********** **************) -let mkMeta (proof,goal) = -let curi,metasenv,pbo,pty = proof in -let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in -Cic.Meta (ProofEngineHelpers.new_meta proof) - (ProofEngineHelpers.identity_relocation_list_for_metavariable context) -;; - let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = - let new_m = mkMeta (proof,goal) in - PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (new_m,t))::al)) ~status:(proof,goal) + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,t)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) ~status:(proof',goal) + in + proof'',fresh_meta::goals ;; @@ -594,7 +597,19 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 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 - apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,ty)) ~applist:[mkMeta(proof,goal)] ~status:(proof,goal) + + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,c)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] ~status:(proof',goal) + in + (* We permute the generated goals to be consistent with Coq *) + match goals with + [] -> assert false + | he::tl -> proof'',he::fresh_meta::tl ;; @@ -679,9 +694,22 @@ let rec superlift c n= ;; (* fix !!!!!!!!!! this may not work *) -let equality_replace a b = +let equality_replace a b ~status = + let proof,goal = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +prerr_endline (" " ^ CicPp.ppterm b) ; +prerr_endline ("### IN MY_CUT: ") ; +prerr_endline ("@ " ^ CicPp.ppterm ty) ; +List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ; +prerr_endline ("##- IN MY_CUT ") ; +let res = let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in - PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;a;b]) +(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *) + PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status +in +prerr_endline "EUREKA" ; +res ;; let tcl_fail a ~status:(proof,goal) = @@ -882,10 +910,15 @@ let rec fourier ~status:(s_proof,s_goal)= in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) ~continuations:[Tacticals.then_ (* ?????????????????????????????? *) - ~start:(PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq] )) + ~start:(fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status) ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le)) + ~continuation:Ring.id_tac +(*CSC ~continuation:(Tacticals.thens ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc) ~continuations:[tac2;(Tacticals.thens @@ -903,7 +936,7 @@ let rec fourier ~status:(s_proof,s_goal)= ) ] (* end continuations before comment *) - ) + ) *) ); !tac1] );(*end tac:=*) -- 2.39.2