From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jan 2003 16:54:44 +0000 (+0000)
Subject: Generalize now works on a list of convertible terms, generalizing all of
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06fb3694ba485d761586c1a90f97f15b8915a277;p=helm.git

Generalize now works on a list of convertible terms, generalizing all of
them at once.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 293bed93c..27c6ca17b 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2292,7 +2292,7 @@ let split = call_tactic ProofEngine.split;;
 let left = call_tactic ProofEngine.left;;
 let right = call_tactic ProofEngine.right;;
 let assumption = call_tactic ProofEngine.assumption;;
-let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
+let generalize = call_tactic_with_goal_inputs ProofEngine.generalize;;
 let absurd = call_tactic_with_input ProofEngine.absurd;;
 let contradiction = call_tactic ProofEngine.contradiction;;
 let decompose =
diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 4751cb23f..313790a7f 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -229,7 +229,7 @@ let right () = apply_tactic IntroductionTactics.right_tac
 
 let assumption () = apply_tactic VariousTactics.assumption_tac
 
-let generalize term = apply_tactic (VariousTactics.generalize_tac ~term)
+let generalize terms = apply_tactic (VariousTactics.generalize_tac ~terms)
 
 let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
 let contradiction () = apply_tactic NegationTactics.contradiction_tac
diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 8f8b1261d..59ed974ca 100644
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -79,7 +79,7 @@ val right : unit -> unit
 
 val assumption : unit -> unit
 
-val generalize : Cic.term -> unit
+val generalize : Cic.term list -> unit
 
 val absurd : Cic.term -> unit
 val contradiction : unit -> unit
diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index a51ab3909..5cc513deb 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -261,88 +261,98 @@ let replace_lifting ~equality ~what ~with_what ~where =
   substaux 1 what where
 ;;
 
-(* replaces in a term a term with another one. *)
-(* Lifting are performed as usual.             *)
+(* replaces in a term a list of terms with other ones. *)
+(* Lifting are performed as usual.                     *)
 let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
- let rec substaux k =
-  let module C = Cic in
-  let module S = CicSubstitution in
-   function
-      t when (equality t what) -> S.lift (k-1) with_what
-    | C.Rel n as t ->
-       if n < k then C.Rel n else C.Rel (n + nnn)
-    | C.Var (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-        C.Var (uri,exp_named_subst')
-    | C.Meta (i, l) as t -> 
-       let l' =
-        List.map
-         (function
-             None -> None
-           | Some t -> Some (substaux k t)
-         ) l
-       in
-        C.Meta(i,l')
-    | C.Sort _ as t -> t
-    | C.Implicit as t -> t
-    | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
-    | C.Prod (n,s,t) ->
-       C.Prod (n, substaux k s, substaux (k + 1) t)
-    | C.Lambda (n,s,t) ->
-       C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) ->
-       C.LetIn (n, substaux k s, substaux (k + 1) t)
-    | C.Appl (he::tl) ->
-       (* Invariant: no Appl applied to another Appl *)
-       let tl' = List.map (substaux k) tl in
-        begin
-         match substaux k he with
-            C.Appl l -> C.Appl (l@tl')
-          | _ as he' -> C.Appl (he'::tl')
-        end
-    | C.Appl _ -> assert false
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-       C.Const (uri,exp_named_subst')
-    | C.MutInd (uri,i,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-        C.MutInd (uri,i,exp_named_subst')
-    | C.MutConstruct (uri,i,j,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
-       in
-        C.MutConstruct (uri,i,j,exp_named_subst')
-    | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,substaux k outt, substaux k t,
-        List.map (substaux k) pl)
-    | C.Fix (i,fl) ->
-       let len = List.length fl in
-       let substitutedfl =
-        List.map
-         (fun (name,i,ty,bo) ->
-           (name, i, substaux k ty, substaux (k+len) bo))
-          fl
-       in
-        C.Fix (i, substitutedfl)
-    | C.CoFix (i,fl) ->
-       let len = List.length fl in
-       let substitutedfl =
-        List.map
-         (fun (name,ty,bo) ->
-           (name, substaux k ty, substaux (k+len) bo))
-          fl
-       in
-        C.CoFix (i, substitutedfl)
+ let module C = Cic in
+ let module S = CicSubstitution in
+  let find_image t =
+   let rec find_image_aux =
+    function
+       [],[] -> raise Not_found
+     | what::tl1,with_what::tl2 ->
+        if equality t what then with_what else find_image_aux (tl1,tl2)
+     | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
+   in
+    find_image_aux (what,with_what)
+  in
+  let rec substaux k t =
+   try
+    S.lift (k-1) (find_image t)
+   with Not_found ->
+    match t with
+       C.Rel n as t ->
+        if n < k then C.Rel n else C.Rel (n + nnn)
+     | C.Var (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+         C.Var (uri,exp_named_subst')
+     | C.Meta (i, l) as t -> 
+        let l' =
+         List.map
+          (function
+              None -> None
+            | Some t -> Some (substaux k t)
+          ) l
+        in
+         C.Meta(i,l')
+     | C.Sort _ as t -> t
+     | C.Implicit as t -> t
+     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
+     | C.Prod (n,s,t) ->
+        C.Prod (n, substaux k s, substaux (k + 1) t)
+     | C.Lambda (n,s,t) ->
+        C.Lambda (n, substaux k s, substaux (k + 1) t)
+     | C.LetIn (n,s,t) ->
+        C.LetIn (n, substaux k s, substaux (k + 1) t)
+     | C.Appl (he::tl) ->
+        (* Invariant: no Appl applied to another Appl *)
+        let tl' = List.map (substaux k) tl in
+         begin
+          match substaux k he with
+             C.Appl l -> C.Appl (l@tl')
+           | _ as he' -> C.Appl (he'::tl')
+         end
+     | C.Appl _ -> assert false
+     | C.Const (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+        C.Const (uri,exp_named_subst')
+     | C.MutInd (uri,i,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+         C.MutInd (uri,i,exp_named_subst')
+     | C.MutConstruct (uri,i,j,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+        in
+         C.MutConstruct (uri,i,j,exp_named_subst')
+     | C.MutCase (sp,i,outt,t,pl) ->
+        C.MutCase (sp,i,substaux k outt, substaux k t,
+         List.map (substaux k) pl)
+     | C.Fix (i,fl) ->
+        let len = List.length fl in
+        let substitutedfl =
+         List.map
+          (fun (name,i,ty,bo) ->
+            (name, i, substaux k ty, substaux (k+len) bo))
+           fl
+        in
+         C.Fix (i, substitutedfl)
+     | C.CoFix (i,fl) ->
+        let len = List.length fl in
+        let substitutedfl =
+         List.map
+          (fun (name,ty,bo) ->
+            (name, substaux k ty, substaux (k+len) bo))
+           fl
+        in
+         C.CoFix (i, substitutedfl)
  in
-let res =  
   substaux 1 where
-in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
 ;;
 
 (* Takes a well-typed term and fully reduces it. *)
diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index 2c210b677..e3bdfd49e 100644
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -43,6 +43,6 @@ val replace_lifting :
   what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val replace_lifting_csc :
   int -> equality:(Cic.term -> Cic.term -> bool) ->
-  what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
+  what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term
diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index f0a3070f7..f24f7904c 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -50,68 +50,40 @@ let assumption_tac ~status:((proof,goal) as status) =
 
 (* ANCORA DA DEBUGGARE *)
 
+exception AllSelectedTermsMustBeConvertible;;
+
 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
-let generalize_tac ~term ~status:((proof,goal) as status) =
+let generalize_tac ~terms ~status:((proof,goal) as status) =
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-(*
-     let found = false in
-     let rec new_context context ty = 
-      if ty == term then let found = true in context
-       else match ty with
-             C.Rel _
-           | C.Var _ 
-           | C.Meta _ (* ???? *)
-           | C.Sort s 
-           | C.Implicit -> context                   
-           | C.Cast (val,typ) -> 
-              let tmp_context = new_context context val in 
-               tmp_context @ (new_context tmp_context typ)
-           | C.Prod (binder, source, target) -> 
-           | C.Lambda (binder, source, target) -> 
-              let tmp_context = new_context context source in 
-               tmp_context @ (new_context tmp_context binder)
-           | C.LetIn (binder, term, target) ->
-           | C.Appl applist -> 
-              let rec aux context = 
-               match applist with 
-                  [] -> context
-                | hd::tl -> 
-                   let tmp_context = (new_context context hd)
-                   in aux tmp_context tl 
-              in aux context applist
-           | C.Const (uri, exp_named_subst)
-           | C.MutInd (uri, typeno, exp_named_subst)
-           | C.MutConstruct (uri, typeno, consno, exp_named_subst) -> 
-              match exp_named_subst with
-                 [] -> context
-               | (uri,t)::_ -> new_context context (type_of_aux' context t)
-               | _ -> assert false
-           | C.MutCase (uri, typeno, outtype, iterm, patterns) 
-           | C.Fix (funno, funlist) 
-           | C.CoFix (funno, funlist) ->
-              match funlist with
-                 [] -> context (* caso possibile? *)
-               | (name, index, type, body)::_ -> 
-                  let tmp_context = ~
-     in
-*)
+   let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let typ =
+     match terms with
+        [] -> assert false
+      | he::tl ->
+         (* We need to check that all the convertibility of all the terms *)
+         List.iter
+          (function t ->
+            if not (CicReduction.are_convertible context he t) then 
+             raise AllSelectedTermsMustBeConvertible
+          ) tl ;
+         (CicTypeChecker.type_of_aux' metasenv context he)
+    in
      T.thens 
       ~start:
         (P.cut_tac 
          (C.Prod(
            (C.Name "dummy_for_gen"), 
-           (CicTypeChecker.type_of_aux' metasenv context term),
+           typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==) 
-             ~what:term 
-             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)  
+             ~what:terms
+             ~with_what:(List.map (function _ -> C.Rel 1) terms)
              ~where:ty)
          )))
       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli
index 27b59682f..b08b33fac 100644
--- a/helm/ocaml/tactics/variousTactics.mli
+++ b/helm/ocaml/tactics/variousTactics.mli
@@ -23,9 +23,10 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val assumption_tac: ProofEngineTypes.tactic
+exception AllSelectedTermsMustBeConvertible;;
 
-val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic
+val assumption_tac: ProofEngineTypes.tactic
+val generalize_tac: terms:Cic.term list -> ProofEngineTypes.tactic
 
 (*
 val decide_equality_tac: ProofEngineTypes.tactic