From ea651f11cbc6edb17e8d0d16c239e0cf3f526959 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Feb 2007 18:11:08 +0000 Subject: [PATCH] * 'default "equality"' command changed to consider also eq_rec, eq_rec_r, eq_rect, eq_rect_r * rewrite tactic changed to rewrite also in goals of type Set and Type * more progress in technicalities/setoids.ma --- .../software/components/cic/libraryObjects.ml | 74 +++++++++++++------ .../components/cic/libraryObjects.mli | 8 ++ .../components/tactics/equalityTactics.ml | 14 +++- .../contribs/LAMBDA-TYPES/Base-1/preamble.ma | 4 + helm/software/matita/legacy/coq.ma | 4 + .../software/matita/library/logic/equality.ma | 16 ++++ .../matita/library/technicalities/setoids.ma | 35 +++++---- .../matita/tests/paramodulation/BOO075-1.ma | 16 ++++ 8 files changed, 133 insertions(+), 38 deletions(-) diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml index d8af91a6f..579c21eed 100644 --- a/helm/software/components/cic/libraryObjects.ml +++ b/helm/software/components/cic/libraryObjects.ml @@ -56,12 +56,14 @@ let insert_unique e extract l = let set_default what l = match what,l with "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI; - eq_ind_r_URI;eq_f_URI;eq_f_sym_URI] -> + eq_ind_r_URI;eq_rec_URI;eq_rec_r_URI;eq_rect_URI; + eq_rect_r_URI;eq_f_URI;eq_f_sym_URI] -> eq_URIs_ref := insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI, - eq_ind_r_URI,eq_f_URI,eq_f_sym_URI) - (fun x,_,_,_,_,_,_ -> x) !eq_URIs_ref + eq_ind_r_URI,eq_rec_URI,eq_rec_r_URI,eq_rect_URI, + eq_rect_r_URI,eq_f_URI,eq_f_sym_URI) + (fun x,_,_,_,_,_,_,_,_,_,_ -> x) !eq_URIs_ref | "true",[true_URI] -> true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref | "false",[false_URI] -> @@ -82,11 +84,11 @@ let reset_defaults () = (**** LOOKUP FUNCTIONS ****) let eq_URI () = - try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq + try let eq,_,_,_,_,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq with Failure "hd" -> None let is_eq_URI uri = - List.exists (fun (eq,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref + List.exists (fun (eq,_,_,_,_,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref let is_eq_refl_URI uri = let urieq = UriManager.strip_xpointer uri in @@ -95,22 +97,32 @@ let is_eq_refl_URI uri = ;; let is_eq_ind_URI uri = - List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref + List.exists (fun (_,_,_,eq_ind,_,_,_,_,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref let is_eq_ind_r_URI uri = - List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref + List.exists (fun (_,_,_,_,eq_ind_r,_,_,_,_,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref +let is_eq_rec_URI uri = + List.exists (fun (_,_,_,_,_,eq_rec,_,_,_,_,_) -> UriManager.eq eq_rec uri) !eq_URIs_ref +let is_eq_rec_r_URI uri = + List.exists (fun (_,_,_,_,_,_,eq_rec_r,_,_,_,_) -> UriManager.eq eq_rec_r uri) !eq_URIs_ref +let is_eq_rect_URI uri = + List.exists (fun (_,_,_,_,_,_,_,eq_rect,_,_,_) -> UriManager.eq eq_rect uri) !eq_URIs_ref +let is_eq_rect_r_URI uri = + List.exists (fun (_,_,_,_,_,_,_,_,eq_rect_r,_,_) -> UriManager.eq eq_rect_r uri) !eq_URIs_ref let is_trans_eq_URI uri = - List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref + List.exists (fun (_,_,trans_eq,_,_,_,_,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref let is_sym_eq_URI uri = - List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref + List.exists (fun (_,sym_eq,_,_,_,_,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref let is_eq_f_URI uri = - List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref + List.exists (fun (_,_,_,_,_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref let is_eq_f_sym_URI uri = - List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref + List.exists (fun (_,_,_,_,_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref let in_eq_URIs uri = is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri || - is_eq_ind_r_URI uri || is_trans_eq_URI uri || is_sym_eq_URI uri || - is_eq_f_URI uri || is_eq_f_sym_URI uri + is_eq_ind_r_URI uri || is_eq_rec_URI uri || is_eq_rec_r_URI uri || + is_eq_rect_URI uri || is_eq_rect_r_URI uri || + is_trans_eq_URI uri || is_sym_eq_URI uri || is_eq_f_URI uri || + is_eq_f_sym_URI uri @@ -120,39 +132,59 @@ let eq_refl_URI ~eq:uri = let sym_eq_URI ~eq:uri = try - let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,x,_,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let trans_eq_URI ~eq:uri = try - let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,x,_,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_ind_URI ~eq:uri = try - let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,_,x,_,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_ind_r_URI ~eq:uri = try - let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,_,_,x,_,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) + +let eq_rec_URI ~eq:uri = + try + let _,_,_,_,_,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) + +let eq_rec_r_URI ~eq:uri = + try + let _,_,_,_,_,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) + +let eq_rect_URI ~eq:uri = + try + let _,_,_,_,_,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) + +let eq_rect_r_URI ~eq:uri = + try + let _,_,_,_,_,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_f_URI ~eq:uri = try - let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,_,_,_,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_f_sym_URI ~eq:uri = try - let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,_,_,_,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_URI_of_eq_f_URI eq_f_URI = try - let x,_,_,_,_,_,_ = - List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref + let x,_,_,_,_,_,_,_,_,_,_ = + List.find (fun _,_,_,_,_,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI)) diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli index 0bf8bfea5..f0d8e4631 100644 --- a/helm/software/components/cic/libraryObjects.mli +++ b/helm/software/components/cic/libraryObjects.mli @@ -33,6 +33,10 @@ val is_eq_URI : UriManager.uri -> bool val is_eq_refl_URI : UriManager.uri -> bool val is_eq_ind_URI : UriManager.uri -> bool val is_eq_ind_r_URI : UriManager.uri -> bool +val is_eq_rec_URI : UriManager.uri -> bool +val is_eq_rec_r_URI : UriManager.uri -> bool +val is_eq_rect_URI : UriManager.uri -> bool +val is_eq_rect_r_URI : UriManager.uri -> bool val is_trans_eq_URI : UriManager.uri -> bool val is_sym_eq_URI : UriManager.uri -> bool val is_eq_f_URI : UriManager.uri -> bool @@ -46,6 +50,10 @@ exception NotRecognized of string;; val eq_refl_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri +val eq_rec_URI : eq:UriManager.uri -> UriManager.uri +val eq_rec_r_URI : eq:UriManager.uri -> UriManager.uri +val eq_rect_URI : eq:UriManager.uri -> UriManager.uri +val eq_rect_r_URI : eq:UriManager.uri -> UriManager.uri val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri val eq_f_URI : eq:UriManager.uri -> UriManager.uri diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 839d0532a..f2760c30f 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -46,6 +46,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let proof,goal = status in let curi, metasenv, pbo, pty, attrs = proof in let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in + let gsort,_ = + CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in match hyps_pat with he::(_::_ as tl) -> PET.apply_tactic @@ -117,8 +119,16 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> let ind_uri = - if_right_to_left dir2 - LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI + match gsort with + C.Sort C.Prop -> + if_right_to_left dir2 + LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI + | C.Sort C.Set -> + if_right_to_left dir2 + LibraryObjects.eq_rec_URI LibraryObjects.eq_rec_r_URI + | _ -> + if_right_to_left dir2 + LibraryObjects.eq_rect_URI LibraryObjects.eq_rect_r_URI in let eq_ind = C.Const (ind_uri uri,[]) in if dir2 then diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma index 0b7687bdd..ce57b6e5e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma @@ -156,5 +156,9 @@ default "equality" cic:/matita/LAMBDA-TYPES/Base-1/preamble/trans_eq.con cic:/Coq/Init/Logic/eq_ind.con cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/eq_rec.con + cic:/Coq/Init/Logic/eq_rec_r.con + cic:/Coq/Init/Logic/eq_rect.con + cic:/Coq/Init/Logic/eq_rect_r.con cic:/matita/LAMBDA-TYPES/Base-1/preamble/f_equal.con cic:/matita/legacy/coq/f_equal1.con. diff --git a/helm/software/matita/legacy/coq.ma b/helm/software/matita/legacy/coq.ma index 9860c63e2..4ea9919f1 100644 --- a/helm/software/matita/legacy/coq.ma +++ b/helm/software/matita/legacy/coq.ma @@ -20,6 +20,10 @@ default "equality" cic:/Coq/Init/Logic/trans_eq.con cic:/Coq/Init/Logic/eq_ind.con cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/eq_rec.con + cic:/Coq/Init/Logic/eq_rec_r.con + cic:/Coq/Init/Logic/eq_rect.con + cic:/Coq/Init/Logic/eq_rect_r.con cic:/Coq/Init/Logic/f_equal.con cic:/matita/legacy/coq/f_equal1.con. diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index 510f0c5c6..01c60e8fc 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -60,6 +60,18 @@ theorem eq_elim_r: intros. elim (sym_eq ? ? ? H1).assumption. qed. +theorem eq_elim_r': + \forall A:Type.\forall x:A. \forall P: A \to Set. + P x \to \forall y:A. y=x \to P y. +intros. elim (sym_eq ? ? ? H).assumption. +qed. + +theorem eq_elim_r'': + \forall A:Type.\forall x:A. \forall P: A \to Type. + P x \to \forall y:A. y=x \to P y. +intros. elim (sym_eq ? ? ? H).assumption. +qed. + theorem eq_f: \forall A,B:Type.\forall f:A\to B. \forall x,y:A. x=y \to f x = f y. intros.elim H.apply refl_eq. @@ -81,6 +93,10 @@ default "equality" cic:/matita/logic/equality/transitive_eq.con cic:/matita/logic/equality/eq_ind.con cic:/matita/logic/equality/eq_elim_r.con + cic:/matita/logic/equality/eq_rec.con + cic:/matita/logic/equality/eq_elim_r'.con + cic:/matita/logic/equality/eq_rect.con + cic:/matita/logic/equality/eq_elim_r''.con cic:/matita/logic/equality/eq_f.con (* *) cic:/matita/logic/equality/eq_OF_eq.con. diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index c60b4d1ed..479c7a424 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -810,30 +810,35 @@ theorem apply_morphism_compatibility_Left2Right: ] ] qed. -(* + definition interp : ∀Hole,dir,Out,dir'. carrier_of_relation_class ? Hole → Morphism_Context Hole dir Out dir' → carrier_of_relation_class ? Out. intros (Hole dir Out dir' H t). apply - (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class S) + (Morphism_Context_rect2 Hole dir (λS,xx,yy. carrier_of_relation_class ? S) (λxx,L,fcl.product_of_arguments L)); - intros. - exact (apply_morphism ? ? (Function m) X). - exact H. - exact c. - exact x. - simpl; - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - split. - rewrite <- + intros; + [8: apply t + |7: skip + | exact (apply_morphism ? ? (Function ? ? m) p) + | exact H + | exact c + | exact x + | simplify; + rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - exact X0. + exact c1 + | split; + [ rewrite < + (about_carrier_of_relation_class_and_relation_class_of_argument_class S); + exact c1 + | exact p + ] + ] qed. +(* (*CSC: interp and interp_relation_class_list should be mutually defined. since the proof term of each one contains the proof term of the other one. However I cannot do that interactively (I should write the Fix by hand) *) diff --git a/helm/software/matita/tests/paramodulation/BOO075-1.ma b/helm/software/matita/tests/paramodulation/BOO075-1.ma index f5cfc7c31..f266b1a94 100644 --- a/helm/software/matita/tests/paramodulation/BOO075-1.ma +++ b/helm/software/matita/tests/paramodulation/BOO075-1.ma @@ -12,6 +12,18 @@ theorem eq_elim_r: intros. elim (sym_eq ? ? ? H1).assumption. qed. +theorem eq_elim_r': + \forall A:Type.\forall x:A. \forall P: A \to Set. + P x \to \forall y:A. eq A y x \to P y. +intros. elim (sym_eq ? ? ? H).assumption. +qed. + +theorem eq_elim_r'': + \forall A:Type.\forall x:A. \forall P: A \to Type. + P x \to \forall y:A. eq A y x \to P y. +intros. elim (sym_eq ? ? ? H).assumption. +qed. + theorem trans_eq : \forall A:Type.\forall x,y,z:A. eq A x y \to eq A y z \to eq A x z. intros.elim H1.assumption. @@ -23,6 +35,10 @@ default "equality" cic:/matita/TPTP/BOO075-1/trans_eq.con cic:/matita/TPTP/BOO075-1/eq_ind.con cic:/matita/TPTP/BOO075-1/eq_elim_r.con + cic:/matita/TPTP/BOO075-1/eq_rec.con + cic:/matita/TPTP/BOO075-1/eq_elim_r'.con + cic:/matita/TPTP/BOO075-1/eq_rect.con + cic:/matita/TPTP/BOO075-1/eq_elim_r''.con cic:/matita/TPTP/BOO075-1/eq_f.con cic:/matita/TPTP/BOO075-1/eq_f1.con. -- 2.39.2