fix tac_solve (fix Deducteam#1041) (Deducteam#1052)

src/core/libMeta.ml

@@ -3,6 +3,11 @@
 open Lplib
 open Term
 open Timed
+open Common
+
+(** Logging function for unification. *)
+let log = Logger.make 'a' "meta" "metavariables"
+let log = log.pp
 
 let meta_counter : int Stdlib.ref = Stdlib.ref (-1)
 
@@ -11,12 +16,13 @@ let reset_meta_counter () = Stdlib.(meta_counter := -1)
 
 (** [fresh p ?name a n] creates a fresh metavariable of type [a] and arity [n]
    with the optional name [name], and adds it to [p]. *)
-let fresh : problem -> term -> int -> meta =
-  fun p a n ->
+let fresh : problem -> term -> int -> meta = fun p a n ->
   let m = {meta_key = Stdlib.(incr meta_counter; !meta_counter);
-           meta_type = ref a; meta_arity = n;
-           meta_value = ref None } in
-  p := {!p with metas = MetaSet.add m !p.metas}; m
+           meta_type = ref a; meta_arity = n; meta_value = ref None } in
+  if Logger.log_enabled() then log "fresh ?%d" m.meta_key;
+  p := {!p with metas = MetaSet.add m !p.metas};
+  if Logger.log_enabled() then log "%a" Print.problem p;
+  m
 
 (** [fresh_box p a n] is the boxed counterpart of [fresh_meta]. It is
     only useful in the rare cases where the type of a metavariable
@@ -40,8 +46,7 @@ let set : problem -> meta -> tmbinder -> unit = fun p m v ->
 
 (** [make p ctx a] creates a fresh metavariable term of type [a] in the
    context [ctx], and adds it to [p]. *)
-let make : problem -> ctxt -> term -> term =
-  fun p ctx a ->
+let make : problem -> ctxt -> term -> term = fun p ctx a ->
   let a, k = Ctxt.to_prod ctx a in
   let m = fresh p a k in
   let get_var (x,_,d) = if d = None then Some (mk_Vari x) else None in
@@ -51,8 +56,7 @@ let make : problem -> ctxt -> term -> term =
     a fresh {e boxed} metavariable in {e boxed} context [bctx] of {e
     boxed} type [a]. It is the same as [lift (make p c b)] (provided that
     [bctx] is boxed [c] and [a] is boxed [b]), but more efficient. *)
-let bmake : problem -> bctxt -> tbox -> tbox =
-  fun p bctx a ->
+let bmake : problem -> bctxt -> tbox -> tbox = fun p bctx a ->
   let (a, k) = Ctxt.to_prod_box bctx a in
   let m = fresh_box p a k in
   let get_var (x, _) = _Vari x in

src/core/unif.ml

@@ -8,8 +8,8 @@ open LibTerm
 open Print
 
 (** Logging function for unification. *)
-let log_unif = Logger.make 'u' "unif" "unification"
-let log_unif = log_unif.pp
+let log = Logger.make 'u' "unif" "unification"
+let log = log.pp
 
 (** Given a meta [m] of type [Πx1:a1,..,Πxn:an,b], [set_to_prod p m] sets [m]
    to a product term of the form [Πy:m1[x1;..;xn],m2[x1;..;xn;y]] with [m1]
@@ -32,7 +32,7 @@ let set_to_prod : problem -> meta -> unit = fun p m ->
   (* result *)
   let r = _Prod a b in
   if Logger.log_enabled () then
-    log_unif (red "%a ≔ %a") meta m term (Bindlib.unbox r);
+    log (red "%a ≔ %a") meta m term (Bindlib.unbox r);
   LibMeta.set p m (Bindlib.unbox (Bindlib.bind_mvar vs r))
 
 (** [type_app c a ts] returns [Some u] where [u] is a type of [add_args x ts]
@@ -46,14 +46,14 @@ let rec type_app : ctxt -> term -> term list -> term option = fun c a ts ->
 
 (** [add_constr p c] adds the constraint [c] into [p.to_solve]. *)
 let add_constr : problem -> constr -> unit = fun p c ->
-  if Logger.log_enabled () then log_unif (mag "add %a") constr c;
+  if Logger.log_enabled () then log (mag "add %a") constr c;
   p := {!p with to_solve = c::!p.to_solve}
 
 (** [try_unif_rules p c s t] tries to simplify the unification problem [c
    ⊢ s ≡ t] with the user-defined unification rules. *)
 let try_unif_rules : problem -> ctxt -> term -> term -> bool =
   fun p c s t ->
-  if Logger.log_enabled () then log_unif "check unif_rules";
+  if Logger.log_enabled () then log "check unif_rules";
   let exception No_match in
   let open Unif_rule in
   try
@@ -82,10 +82,10 @@ let try_unif_rules : problem -> ctxt -> term -> term -> bool =
           Error.fatal_no_pos "Untypable unification problem."
     in
     let cs = List.map (fun (t,u) -> sanitise (c,t,u)) (unpack rhs) in
-    if Logger.log_enabled () then log_unif "rewrites to: %a" constrs cs;
+    if Logger.log_enabled () then log "rewrites to: %a" constrs cs;
     true
   with No_match ->
-    if Logger.log_enabled () then log_unif "found no unif_rule";
+    if Logger.log_enabled () then log "found no unif_rule";
     false
 
 (** [instantiable c m ts u] tells whether, in a problem [m[ts]=u], [m] can
@@ -115,36 +115,35 @@ let do_type_check = Stdlib.ref true
    metavariables of [p]. *)
 let instantiate : problem -> ctxt -> meta -> term array -> term -> bool =
   fun p c m ts u ->
-  if Logger.log_enabled () then log_unif "try instantiate";
+  if Logger.log_enabled () then log "try instantiate";
   match instantiation c m ts u with
   | Some b when Bindlib.is_closed b ->
-      let do_instantiate() =
-        if Logger.log_enabled () then
-          log_unif (red "%a ≔ %a") meta m term u;
+      let do_instantiate p =
+        if Logger.log_enabled () then log (red "%a ≔ %a") meta m term u;
         LibMeta.set p m (Bindlib.unbox b);
         p := {!p with recompute = true}; true
       in
       if Stdlib.(!do_type_check) then
         begin
-          if Logger.log_enabled () then log_unif "check typing";
+          if Logger.log_enabled () then log "check typing";
           let typ_mts =
             match type_app c !(m.meta_type) (Array.to_list ts) with
             | Some a -> a
             | None -> assert false
           in
-          if Infer.check_noexn p c u typ_mts <> None then do_instantiate()
-          else (if Logger.log_enabled () then log_unif "typing failed"; false)
+          if Infer.check_noexn p c u typ_mts <> None then do_instantiate p
+          else (if Logger.log_enabled () then log "typing failed"; false)
         end
-      else do_instantiate()
+      else do_instantiate p
   | i ->
       if Logger.log_enabled () then
         begin
           match i with
           | None ->
-              if LibMeta.occurs m c u then log_unif "occur check failed"
-              else log_unif "arguments are not distinct variables: %a"
+              if LibMeta.occurs m c u then log "occur check failed"
+              else log "arguments are not distinct variables: %a"
                      (Array.pp term "; ") ts
-          | Some _ -> log_unif "not closed"
+          | Some _ -> log "not closed"
         end;
       false
 
@@ -155,17 +154,17 @@ let instantiate : problem -> ctxt -> meta -> term array -> term -> bool =
 let add_to_unsolved : problem -> ctxt -> term -> term -> unit =
   fun p c t1 t2 ->
   if Eval.pure_eq_modulo c t1 t2 then
-    (if Logger.log_enabled () then log_unif "equivalent terms")
+    (if Logger.log_enabled () then log "equivalent terms")
   else if not (try_unif_rules p c t1 t2) then
-    (if Logger.log_enabled () then log_unif "move to unsolved";
+    (if Logger.log_enabled () then log "move to unsolved";
      p := {!p with unsolved = (c,t1,t2)::!p.unsolved})
 
 (** [decompose p c ts1 ts2] tries to decompose a problem of the form [h ts1 ≡
    h ts2] into the problems [t1 ≡ u1; ..; tn ≡ un], assuming that [ts1 =
    [t1;..;tn]] and [ts2 = [u1;..;un]]. *)
 let decompose : problem -> ctxt -> term list -> term list -> unit =
   fun p c ts1 ts2 ->
-    if Logger.log_enabled () && ts1 <> [] then log_unif "decompose";
+    if Logger.log_enabled () && ts1 <> [] then log "decompose";
     List.iter2 (fun a b -> add_constr p (c,a,b)) ts1 ts2
 
 (** For a problem of the form [h1 ≡ h2] with [h1 = m[ts]], [h2 = Πx:_,_] (or
@@ -174,7 +173,7 @@ let decompose : problem -> ctxt -> term list -> term list -> unit =
    [p]. *)
 let imitate_prod : problem -> ctxt -> meta -> term -> term -> unit =
   fun p c m h1 h2 ->
-  if Logger.log_enabled () then log_unif "imitate_prod %a" meta m;
+  if Logger.log_enabled () then log "imitate_prod %a" meta m;
   set_to_prod p m; add_constr p (c,h1,h2)
 
 (** For a problem [m[vs] ≡ s(ts)] in context [c], where [vs] are distinct
@@ -189,7 +188,7 @@ let imitate_inj :
       -> bool =
   fun p c m vs us s ts ->
   if Logger.log_enabled () then
-    log_unif "imitate_inj %a ≡ %a" term (add_args (mk_Meta(m,vs)) us)
+    log "imitate_inj %a ≡ %a" term (add_args (mk_Meta(m,vs)) us)
                                    term (add_args (mk_Symb s) ts);
   let exception Cannot_imitate in
   try
@@ -216,7 +215,7 @@ let imitate_inj :
         | _ -> raise Cannot_imitate
       in build (List.length ts) [] !(s.sym_type)
     in
-    if Logger.log_enabled () then log_unif (red "%a ≔ %a") meta m term t;
+    if Logger.log_enabled () then log (red "%a ≔ %a") meta m term t;
     LibMeta.set p m (binds vars lift t); true
   with Cannot_imitate | Invalid_argument _ -> false
 
@@ -242,7 +241,7 @@ let imitate_lam_cond : term -> term list -> bool = fun h ts ->
    a new metavariable of arity [n+1] and type
    [Πx1:a1,..,Πxn:an,Πx:m2[x1,..,xn],TYPE], and do as in the previous case. *)
 let imitate_lam : problem -> ctxt -> meta -> unit = fun p c m ->
-    if Logger.log_enabled () then log_unif "imitate_lam %a" meta m;
+    if Logger.log_enabled () then log "imitate_lam %a" meta m;
     let n = m.meta_arity in
     let env, t = Env.of_prod_nth c n !(m.meta_type) in
     let of_prod a b =
@@ -280,19 +279,19 @@ let imitate_lam : problem -> ctxt -> meta -> unit = fun p c m ->
     let xu1 = _Abst a (Bindlib.bind_var x u1) in
     let v = Bindlib.bind_mvar (Env.vars env) xu1 in
     if Logger.log_enabled () then
-      log_unif (red "%a ≔ %a") meta m term (Bindlib.unbox xu1);
+      log (red "%a ≔ %a") meta m term (Bindlib.unbox xu1);
     LibMeta.set p m (Bindlib.unbox v)
 
 (** [inverse_opt s ts v] returns [Some(t, inverse s v)] if [ts=[t]], [s] is
    injective and [inverse s v] does not fail, and [None] otherwise. *)
 let inverse_opt : sym -> term list -> term -> (term * term) option =
   fun s ts v ->
-  if Logger.log_enabled () then log_unif "try inverse %a" sym s;
+  if Logger.log_enabled () then log "try inverse %a" sym s;
   try
     match ts with
     | [t] when is_injective s -> Some (t, Inverse.inverse s v)
     | _ -> raise Not_found
-  with Not_found -> if Logger.log_enabled () then log_unif "failed"; None
+  with Not_found -> if Logger.log_enabled () then log "failed"; None
 
 (** Exception raised when a constraint is not solvable. *)
 exception Unsolvable
@@ -316,7 +315,7 @@ let inverse : problem -> ctxt -> term -> sym -> term list -> term -> unit =
         match unfold t2 with
         | Prod _ when is_constant s -> error t1 t2
         | _ ->
-            if Logger.log_enabled () then log_unif "move to unsolved";
+            if Logger.log_enabled () then log "move to unsolved";
             p := {!p with unsolved = (c, t1, t2)::!p.unsolved}
 
 (** [sym_sym_whnf p c t1 s1 ts1 t2 s2 ts2 p] handles the case [s1(ts1) =
@@ -341,24 +340,25 @@ let sym_sym_whnf :
 Otherwise, [p.to_solve] is empty but [p.unsolved] may still contain
 constraints that could not be simplified. *)
 let solve : problem -> unit = fun p ->
-  while !p.to_solve <> [] || (!p.recompute && !p.unsolved <> []) do
+  while !p.to_solve <> [] || (!p.recompute && !p.unsolved <> []) do begin
+  log "solve %a" problem p;
   match !p.to_solve with
   | [] ->
-      if Logger.log_enabled () then log_unif "recompute";
+      if Logger.log_enabled () then log "recompute";
       p := {!p with to_solve = !p.unsolved; unsolved = []; recompute = false}
   | (c,t1,t2)::to_solve ->
   (*if Logger.log_enabled () then
-    log_unif "%d constraints" (1 + List.length to_solve);*)
+    log "%d constraints" (1 + List.length to_solve);*)
 
   (* We remove the first constraint from [p] for not looping. *)
   p := {!p with to_solve};
 
   (* We first try without normalizing wrt user-defined rules. *)
   let tags = [`NoRw; `NoExpand] in
   let t1 = Eval.whnf ~tags c t1 and t2 = Eval.whnf ~tags c t2 in
-  if Logger.log_enabled () then log_unif (gre "solve %a") constr (c,t1,t2);
+  if Logger.log_enabled () then log (gre "solve %a") constr (c,t1,t2);
   if Eval.pure_eq_modulo ~tags c t1 t2 then
-    (if Logger.log_enabled () then log_unif "equivalent terms")
+    (if Logger.log_enabled () then log "equivalent terms")
   else
   let h1, ts1 = get_args t1 and h2, ts2 = get_args t2 in
 
@@ -369,7 +369,7 @@ let solve : problem -> unit = fun p ->
   | Prod(a1,b1), Prod(a2,b2)
   | Abst(a1,b1), Abst(a2,b2) ->
       (* [ts1] and [ts2] must be empty because of typing or normalization. *)
-      if Logger.log_enabled () then log_unif "decompose";
+      if Logger.log_enabled () then log "decompose";
       add_constr p (c,a1,a2);
       let (x,b1,b2) = Bindlib.unbind2 b1 b2 in
       let c' = (x,a1,None)::c in
@@ -414,9 +414,9 @@ let solve : problem -> unit = fun p ->
 
   | _ ->
   (* We normalize wrt user-defined rules and try again. *)
-  if Logger.log_enabled () then log_unif "whnf";
+  if Logger.log_enabled () then log "whnf";
   let t1 = Eval.whnf c t1 and t2 = Eval.whnf c t2 in
-  if Logger.log_enabled () then log_unif (gre "solve %a") constr (c,t1,t2);
+  if Logger.log_enabled () then log (gre "solve %a") constr (c,t1,t2);
   let h1, ts1 = get_args t1 and h2, ts2 = get_args t2 in
 
   match h1, h2 with
@@ -426,7 +426,7 @@ let solve : problem -> unit = fun p ->
   | Prod(a1,b1), Prod(a2,b2)
   | Abst(a1,b1), Abst(a2,b2) ->
       (* [ts1] and [ts2] must be empty because of typing or normalization. *)
-      if Logger.log_enabled () then log_unif "decompose";
+      if Logger.log_enabled () then log "decompose";
       add_constr p (c,a1,a2);
       let (x,b1,b2) = Bindlib.unbind2 b1 b2 in
       let c' = (x,a1,None)::c in
@@ -482,7 +482,7 @@ let solve : problem -> unit = fun p ->
   | _, Symb s -> inverse p c t2 s ts2 t1
 
   | _ -> add_to_unsolved p c t1 t2
-  done
+  end done
 
 (** [solve_noexn ~type_check p] tries to simplify the constraints of [p]. It
    returns [false] if it finds a constraint that cannot be

src/handle/tactic.ml

@@ -75,24 +75,38 @@ let tac_admit: Sig_state.t -> popt -> proof_state -> goal_typ -> proof_state =
    state [ps] and fails if constraints are unsolvable. *)
 let tac_solve : popt -> proof_state -> proof_state = fun pos ps ->
   if Logger.log_enabled () then log "@[<v>tac_solve@ %a@]" goals ps;
+  (* convert the proof_state into a problem *)
   let gs_typ, gs_unif = List.partition is_typ ps.proof_goals in
   let p = new_problem() in
-  let f ms = function
+  let add_meta ms = function
     | Unif _ -> ms
     | Typ gt -> MetaSet.add gt.goal_meta ms
   in
-  p := {!p with metas = List.fold_left f MetaSet.empty gs_typ
+  p := {!p with metas = List.fold_left add_meta MetaSet.empty gs_typ
               ; to_solve = List.rev_map get_constr gs_unif};
+  (* try to solve the problem *)
   if not (Unif.solve_noexn p) then
     fatal pos "Unification goals are unsatisfiable.";
-  (* remove in [gs_typ] the goals that have been instantiated, and simplify
-     the others. *)
-  let not_instantiated = function
-    | Typ gt when !(gt.goal_meta.meta_value) <> None -> None
-    | gt -> Some (Goal.simpl Eval.simplify gt)
+  (* compute the new list of goals by preserving the order of initial goals
+     and adding the new goals at the end *)
+  let non_instantiated = function
+    | Typ gt -> !(gt.goal_meta.meta_value) = None
+    | _ -> assert false
   in
-  let gs_typ = List.filter_map not_instantiated gs_typ in
-  {ps with proof_goals = List.map (fun c -> Unif c) !p.unsolved @ gs_typ}
+  let gs_typ = List.filter non_instantiated gs_typ in
+  let is_eq_goal_meta m = function
+    | Typ gt -> m == gt.goal_meta
+    | _ -> assert false
+  in
+  let add_goal m gs =
+    if List.exists (is_eq_goal_meta m) gs_typ then gs
+    else Goal.of_meta m :: gs
+  in
+  let proof_goals =
+    gs_typ @ MetaSet.fold add_goal (!p).metas
+               (List.map (fun c -> Unif c) (!p).unsolved)
+  in
+  {ps with proof_goals}
 
 (** [tac_refine pos ps gt gs p t] refines the typing goal [gt] with [t]. [p]
    is the set of metavariables created by the scoping of [t]. *)

tests/KO/1041.lp

@@ -0,0 +1,43 @@
+constant symbol Prop : TYPE;
+builtin "Prop" ≔ Prop;
+injective symbol π : Prop → TYPE; // `p
+builtin "P" ≔ π;
+
+constant symbol Set : TYPE;
+injective symbol τ : Set → TYPE;
+builtin "T" ≔ τ;
+
+constant symbol ⊥ : Prop; // \bot
+
+constant symbol ⇒ : Prop → Prop → Prop; notation ⇒ infix right 5; // =>
+rule π ($p ⇒ $q) ↪ π $p → π $q;
+
+symbol ¬ p ≔ p ⇒ ⊥; // ~~ or \neg
+notation ¬ prefix 35;
+
+constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall
+rule π (∀ $f) ↪ Π x, π ($f x);
+
+injective symbol πᶜ p ≔ π (¬ ¬ p);
+
+flag "print_implicits" on;
+flag "print_domains" on;
+//flag "print_meta_types" on;
+
+symbol ∀ᶜ [a] p ≔ `∀ x : τ a, ¬ ¬ (p x); notation ∀ᶜ quantifier;
+
+//debug +hiuta;
+opaque symbol ∀ᶜᵢ p : (Π x, πᶜ (p x)) → πᶜ (∀ᶜ p) ≔
+begin
+  print;
+  //debug -hiuta;
+  assume p Hnnpx Hnnnpx;
+  apply Hnnnpx;
+  assume x Hnnp;
+  apply Hnnpx x;
+  assume Hnp;
+  apply Hnnp;
+  apply Hnp;
+end;
+
+print ∀ᶜᵢ;