From cc1de1c6d57a657d2d94636ff54fb9222b286df1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jan 2003 18:02:57 +0000
Subject: [PATCH] replace_lifting generalized to the simultaneous replacement
 of n terms.

---
 helm/ocaml/tactics/equalityTactics.ml       |  4 +-
 helm/ocaml/tactics/proofEngineReduction.ml  | 43 ++++++++++++++-------
 helm/ocaml/tactics/proofEngineReduction.mli |  2 +-
 3 files changed, 33 insertions(+), 16 deletions(-)

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 36704b441..8cb794ff6 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -56,7 +56,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
@@ -118,7 +118,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) =
      let gty'' =
       ProofEngineReduction.replace_lifting
        ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
      in
       C.Lambda
        (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 5cc513deb..c70be1fb7 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -183,12 +183,24 @@ let replace ~equality ~what ~with_what ~where =
 (* replaces in a term a term with another one. *)
 (* Lifting are performed as usual.             *)
 let replace_lifting ~equality ~what ~with_what ~where =
- let rec substaux k what =
-  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 -> t
+ let module C = Cic in
+ let module S = CicSubstitution in
+  let find_image what 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 what t =
+   try
+    S.lift (k-1) (find_image what t)
+   with Not_found ->
+    match t with
+      C.Rel n as t -> t
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
@@ -207,11 +219,14 @@ let replace_lifting ~equality ~what ~with_what ~where =
     | C.Implicit as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
     | C.Prod (n,s,t) ->
-       C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+       C.Prod
+        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
     | C.Lambda (n,s,t) ->
-       C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+       C.Lambda
+        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
     | C.LetIn (n,s,t) ->
-       C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+       C.LetIn
+        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k what) tl in
@@ -244,8 +259,9 @@ let replace_lifting ~equality ~what ~with_what ~where =
        let substitutedfl =
         List.map
          (fun (name,i,ty,bo) ->
-           (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
-          fl
+           (name, i, substaux k what ty,
+             substaux (k+len) (List.map (S.lift len) what) bo)
+         ) fl
        in
         C.Fix (i, substitutedfl)
     | C.CoFix (i,fl) ->
@@ -253,8 +269,9 @@ let replace_lifting ~equality ~what ~with_what ~where =
        let substitutedfl =
         List.map
          (fun (name,ty,bo) ->
-           (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
-          fl
+           (name, substaux k what ty,
+             substaux (k+len) (List.map (S.lift len) what) bo)
+         ) fl
        in
         C.CoFix (i, substitutedfl)
  in
diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index e3bdfd49e..02e56ba6a 100644
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -40,7 +40,7 @@ val replace :
   what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val replace_lifting :
   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 replace_lifting_csc :
   int -> equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
-- 
2.39.2