Delift used to produce not well typed substitutions. In turn, this

led to tactics that were not failing immediately, but only at Qed.

Fixed by adding the appropriate check to the delift function.

Note:
 - pass the metavariable number (-1) to avoid the check when you know what
   you are doing (e.g. when delift is just used to restrict a term or to
   replace a term with a convertible one). This used to be 0 (not -1).
 - in some cases (algebraic universes and implicits used to stop chains of
   metavariables) the check is relaxed
 - to make the CerCo script pass (in very "reasonable" and "frequent" cases),
   the algorithm needs to solve the following unification problem:
     S (?[n]) == ?[(S n)]
   Our algorithm used to delift S(?[n]) w.r.t. (S n), yielding x |- ? := x.
   By chance, this was the right solution since S (?[n]) becomes (S n) and
   also ?[(S n)] becomes (S n). However, the two solutions were both added
   to the subst (first bug) and they could even be different (second bug).
   We fix this by checking that they are not different.
   However, at the moment, the solution still occurs twice in the subst....

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 03f4affdf64dd672ff82996b8dd26e944317f21c..73cc91892788b5b2c033f6fc39b17562f0530bbe 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -53,16 +53,17 @@ let newmeta,maxmeta =
   (fun () -> !maxmeta)
 ;;
 
-exception NotInTheList;;
+exception NotFound of [`NotInTheList | `NotWellTyped];;
 
 let position to_skip n (shift, lc) =
   match lc with
   | NCic.Irl _ when to_skip > 0 -> assert false  (* unclear to me *)
-  | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
+  | NCic.Irl len when n <= shift || n > shift + len ->
+     raise (NotFound `NotInTheList)
   | NCic.Irl _ -> n - shift
   | NCic.Ctx tl ->
       let rec aux to_skip k = function 
-         | [] -> raise NotInTheList
+         | [] -> raise (NotFound `NotInTheList)
          | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl
          | (NCic.Rel m)::_ when m + shift = n -> k
          | _::tl -> aux to_skip (k+1) tl 
@@ -303,6 +304,7 @@ let int_of_out_scope_tag tag =
 
 
 exception Found;;
+exception TypeNotGood;;
 
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense in case of unification
@@ -359,7 +361,7 @@ let delift status ~unify metasenv subst context n l t =
           match List.nth context (n-1) with
           | _,NCic.Def (bo,_) -> 
                 (try ms, NCic.Rel ((position in_scope (n-k) l) + k)
-                 with NotInTheList ->
+                 with (NotFound `NotInTheList) ->
                 (* CSC: This bit of reduction hurts performances since it is
                  * possible to  have an exponential explosion of the size of the
                  * proof. required for nat/nth_prime.ma *)
@@ -443,7 +445,7 @@ let delift status ~unify metasenv subst context n l t =
                           let ms, t = aux (context,k,in_scope) ms t in 
                           ms, tbr, t::tl
                         with
-                        | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
+                        | (NotFound `NotInTheList) | MetaSubstFailure _ -> ms, j::tbr, tl
                   in
                   let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
                   pp (lazy ("TO BE RESTRICTED: " ^ 
@@ -467,25 +469,71 @@ let delift status ~unify metasenv subst context n l t =
   in
 (*
   prerr_endline (
-    "DELIFTO " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
-    String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) ( 
+    "DELIFTO " ^ status#ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
+    status#ppterm ~metasenv ~subst ~context (NCic.Meta(n,l)) ^ " i.e. " ^
+    String.concat ", " (List.map (status#ppterm ~metasenv ~subst ~context) ( 
       let shift, lc = l in
-      (List.map (NCicSubstitution.lift shift) 
+      (List.map (NCicSubstitution.lift status shift) 
         (NCicUtils.expand_local_context lc))
   )));
 *)
-   try aux (context,0,0) (metasenv,subst) t
-   with NotInTheList ->
+   try
+(*assert (try n = -1 or (ignore(NCicUtils.lookup_meta n metasenv); true) with NCicUtils.Meta_not_found _ -> false);*)
+    let ((metasenv,subst),t) as res = aux (context,0,0) (metasenv,subst) t in
+    if (try n <> -1 && (ignore(NCicUtils.lookup_meta n metasenv); false)
+        with NCicUtils.Meta_not_found _ -> true)
+    then
+     let _,context,bo,_ = NCicUtils.lookup_subst n subst in
+      match unify metasenv subst context bo t with
+         None -> raise (NotFound `NotWellTyped)
+       | Some (metasenv,subst) -> (metasenv,subst),t
+    else
+    (try
+      let _,context,ty = NCicUtils.lookup_meta n metasenv in
+      let ty' =
+       match t with
+          NCic.Sort _ -> (* could be algebraic *) NCic.Implicit `Closed
+        | _ -> NCicTypeChecker.typeof status ~subst ~metasenv context t in
+       (match ty,ty' with
+           NCic.Implicit _,_ ->
+            (match ty' with
+                NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
+              | _ -> raise TypeNotGood)
+         | _,NCic.Implicit _ ->
+            (match ty with
+                NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
+              | _ -> raise TypeNotGood)
+         | _ ->
+           if
+            NCicReduction.are_convertible status ~metasenv ~subst context ty' ty
+           then
+            res
+           else
+            raise TypeNotGood)
+     with
+        NCicUtils.Meta_not_found _ ->
+         (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
+         assert (n = -1); res
+      | TypeNotGood
+      | NCicTypeChecker.AssertFailure _
+      | NCicReduction.AssertFailure _
+      | NCicTypeChecker.TypeCheckerFailure _ ->
+         raise (NotFound `NotWellTyped))
+   with NotFound reason ->
       (* This is the case where we fail even first order unification. *)
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
+      let reason =
+       match reason with
+          `NotInTheList -> "some variable cannot be delifted"
+        | `NotWellTyped -> "the unifier found is not well typed" in
       let msg = (lazy (Printf.sprintf
-        ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
-        "abstract over bound variables") (status#ppterm ~metasenv ~subst
+        ("Error trying to abstract %s over [%s]: %s")
+        (status#ppterm ~metasenv ~subst
         ~context t) (String.concat "; " (List.map (status#ppterm ~metasenv
         ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
-        status shift) (NCicUtils.expand_local_context lc))))))
+        status shift) (NCicUtils.expand_local_context lc)))) reason))
       in
       let shift, lc = l in
       let lc = NCicUtils.expand_local_context lc in

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index d26edf6d9d3bd40783963909cc84bd9dcaaa1d13..bb90cf7215ec0ed2bc85d94e6c22de69e65a4075 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t =
               ~unify:(fun m s c t1 t2 ->
                 try Some (NCicUnification.unify status m s c t1 t2)
                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
-              metasenv subst context 0 (0,NCic.Irl 0) typ
+              metasenv subst context (-1) (0,NCic.Irl 0) typ
             with
               NCicMetaSubst.MetaSubstFailure _
             | NCicMetaSubst.Uncertain _ ->

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index c8f67f1769e523fd53df6f7c067d99c68bcfa915..064a5f6ad08a7c9c99c7933c26991e8a0f484a12 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -913,7 +913,7 @@ and delift_type_wrt_terms status metasenv subst context t args =
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx lc) t
+      metasenv subst context (-1) (0,NCic.Ctx lc) t
    with
       NCicMetaSubst.MetaSubstFailure _
     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 9a6358baaf3e98ee5d4de13bd12e3ee9c02e2e61..143aac98e6294e9e35825bf9450e5a5fab8f4ba0 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -157,7 +157,7 @@ let relocate status destination (source,t as orig) =
             let u, d, metasenv, subst, o = status#obj in
             pp(lazy("delifting as " ^ 
               status#ppterm ~metasenv ~subst ~context:source 
-               (NCic.Meta (0,lc))));
+               (NCic.Meta (-1,lc))));
             let (metasenv, subst), t =
               NCicMetaSubst.delift status
                  ~unify:(fun m s c t1 t2 -> 
@@ -165,7 +165,7 @@ let relocate status destination (source,t as orig) =
                    with 
                     | NCicUnification.UnificationFailure _ 
                     | NCicUnification.Uncertain _ -> None) 
-               metasenv subst source 0 lc t
+               metasenv subst source (-1) lc t
             in
             let status = status#set_obj (u, d, metasenv, subst, o) in
             status, (ctx,t))