* '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

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index d8af91a6f01b4dc0dab2d3708306784a67733891..579c21eede3a9f2f2e44023d180377fcf2282341 100644 (file)
--- 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 0bf8bfea56f165d4d23b5de91e6f6acc67db6958..f0d8e4631baa309212b73ab7be9b49f927b41484 100644 (file)
--- 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 839d0532a401d44a9e159ae11cacc97a8651948e..f2760c30f33f394daded905bc246cc63446e7321 100644 (file)
--- 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 0b7687bddf7630d8fdfc8c30766fc40959e891ba..ce57b6e5e30f0a6be75ed38985627f23fc8ce1dc 100644 (file)
--- 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 9860c63e29137b8c4d1d409d6ac18486ea03574a..4ea9919f1741299c1c1d55722af07c2a30bf0770 100644 (file)
--- 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 510f0c5c6fe3144b395840770c1f8dbe15084163..01c60e8fc9b17c40c720b235be2bcac605e2a8e9 100644 (file)
--- 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 c60b4d1edc7c610f2fa7fe9b38854ddeb8671084..479c7a424740d9d215317cfff33af9cba92b58d7 100644 (file)
--- 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 f5cfc7c31c45c37dd0df4c6ada0081e3c14d507e..f266b1a94ac307245a87fc6ab87af4efea589b17 100644 (file)
--- 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.