#with_goal tactic

CHANGES.md

@@ -21,6 +21,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `first_hyp t` which iterates parameterized tactic term t with each hypothsis as parameter until it succeeds.
 - Tactic `#print` to print a symbol or the current goal.
 - Export to Lean.
+- Tactic `#with_goal t` which calls term tactic t with current goal of type Prop as parameter.
 
 ### Changed
 
@@ -32,6 +33,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - LSP server: position of the error is removed from diagnostics when the error occurs in the file currently open in the editor.
 - Syntax of search query is modified as follows : `in` is used instead of `|` (filtering). `with` is used instead of `,` (conjunction). `|` is used instead of `;` (disjunction).
 - Type of `#assume` in order to generate a new symbol and use it inside a tactic term.
+- Type of `#refine' is in fact `String -> Tactic`
 
 ### Fixed
 

doc/structure.rst

@@ -87,6 +87,7 @@ Overview of directories and files
 
   * ``command.ml``: command handling
   * ``compile.ml``: file parsing and compiling (.lpo files)
+  * ``gconf.ml``: builtins needed to build current goal (tactic #with_goal)
   * ``inductive.ml``: generation of induction principles
   * ``query.ml``: handling of queries (commands that do not change the signature or the proof state)
 

doc/tacticals.rst

@@ -38,6 +38,7 @@ The BNF grammar of tactics is in `lambdapi.bnf <https://raw.githubusercontent.co
    builtin "symmetry" ≔ …; // : T
    builtin "try" ≔ …; // : T → T
    builtin "why3" ≔ …; // : T
+   builtin "with_goal" ≔ …; // (Prop → T) → T
 
 The tactics taking a string as argument need the ``"String"`` :ref:`builtin` to be set. The string argument of ``refine`` is parsed as a term, and thus can contain underscores. If the builtin ``"and"`` is mapped to some symbol, say ``&``, then ``& t u`` is interpreted as follows: the tactic ``t`` is applied and, in case of success, the tactic ``u`` is applied. All other symbols are interpreted by the corresponding tactics.
 
@@ -90,3 +91,8 @@ An example of use is given in `Tactic.lp <https://github.com/Deducteam/lambdapi/
 -------
 
 ``try t`` applies ``t``. If ``t`` fails, then ``try t`` leaves the goal unchanged.
+
+``with_goal``
+-------------
+
+``with_goal t`` calls term tactic ``t`` on the current goal seen as a Prop. builtins must be defined to map Prf, El, => and forAll.

src/handle/gconf.ml

@@ -0,0 +1,48 @@
+(** Configuration for tactics based on first-order logic. *)
+
+open Common open Error
+open Core open Term
+
+type config =
+  { symb_Prop: sym (** Type of propositions. *)
+  ; symb_P   : sym (** Encoding of propositions. *)
+  ; symb_Set : sym (** Type of sets. *)
+  ; symb_T   : sym (** Encoding of types. *)
+  ; symb_imp : sym (** Implication(⇒) symbol. *)
+  ; symb_all : sym (** Forall(∀) symbol. *)
+   }
+
+(** [get_config ss pos] build the configuration using [ss]. *)
+let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos ->
+  let builtin = Builtin.get ss pos [] in
+  let symb_P = builtin "P" and symb_T = builtin "T" in
+  let symb_Prop =
+    match unfold Timed.(!(symb_P.sym_type)) with
+    | Prod(a,_) ->
+        begin
+          match unfold a with
+          | Symb s -> s
+          | _ ->
+              fatal pos "The type of %a is not of the form Prop → _ \
+                         with Prop a symbol." Print.sym symb_P
+        end
+    | _ -> fatal pos "The type of %a is not a product" Print.sym symb_P
+  and symb_Set =
+    match unfold Timed.(!(symb_T.sym_type)) with
+    | Prod(a,_) ->
+        begin
+          match unfold a with
+          | Symb s -> s
+          | _ ->
+              fatal pos "The type of %a is not of the form Prop → _ \
+                         with Prop a symbol." Print.sym symb_T
+        end
+    | _ -> fatal pos "The type of %a is not a product" Print.sym symb_T
+  in
+  { symb_Prop
+  ; symb_P
+  ; symb_Set
+  ; symb_T
+  ; symb_imp = builtin "imp"
+  ; symb_all = builtin "all"
+  }

src/handle/tactic.ml

@@ -194,6 +194,56 @@ let get_prod_ids env =
         else List.rev acc
   in aux []
 
+(** [get_goal pos ps gt] tries to build a goal [g] such as typing goal
+   [gt] = [Prf p]. It uses builtins P, T, imp and all.
+*)
+let get_goal: popt -> Sig_state.t -> goal_typ -> Term.term = fun pos ss gt ->
+  let cfg = Gconf.get_config ss pos in
+  let imp = mk_Symb (cfg.symb_imp) in
+  let all = mk_Symb (cfg.symb_all) in
+
+  (* Extract the term from the goal type (get “u” from “Prf u”). *)
+  let is_prf g =
+    match get_args g with
+    | t, (u::_) when is_symb cfg.symb_P t -> Some u
+    | _ -> None
+  in
+  let is_set g =
+    match get_args g with
+    | t, (u::_) when is_symb cfg.symb_T t -> Some u
+    | _ -> None
+  in
+  let rec as_prop g =
+    match is_prf g with
+    | Some u -> u
+    | None -> match g with
+              | Prod(p,bi) when binder_name bi = "_" ->
+                  begin
+                    let (_,q) = unbind bi in
+                    match is_prf p with
+                      Some u -> mk_Appl(mk_Appl (imp,u), as_prop q)
+                    | None ->
+                        fatal pos "Goal %a not of the form (%a _ [-> ...])."
+                          term gt.goal_type sym cfg.symb_P
+                  end
+              | Prod(p,bi) ->
+                  begin
+                    let (v,q) = unbind bi in
+                    match is_set p with
+                      Some u ->
+                        let q = as_prop q in
+                        mk_Appl(mk_Appl(all, u), mk_Abst(p,bind_var v q))
+                    | None ->
+                        fatal pos "Goal %a not of the form (%a _ [-> ...])."
+                          term gt.goal_type sym cfg.symb_P
+                  end
+              | _ -> fatal pos "Goal %a not of the form (%a _ [-> ...])."
+                       term gt.goal_type sym cfg.symb_P
+  in
+  let r = as_prop gt.goal_type in
+  (* wrn None "goal [%a]" term r; *)
+  r
+
 (** Builtin tactic names. *)
 type tactic =
   | T_admit
@@ -222,6 +272,7 @@ type tactic =
   | T_symmetry
   | T_try
   | T_why3
+  | T_with_goal
 
 type config = (string,tactic) Hashtbl.t
 
@@ -258,6 +309,7 @@ let get_config (ss:Sig_state.t) (pos:Pos.popt) : config =
   add "symmetry" T_symmetry;
   add "try" T_try;
   add "why3" T_why3;
+  add "with_goal" T_with_goal;
   t
 
 (** [p_term pos t] converts the term [t] into a p_term at position [pos]. *)
@@ -363,8 +415,8 @@ let p_tactic (ss:Sig_state.t) (g:goal) (env:Env.t) (pos:Pos.popt) (t:term)
             | T_apply, [_;t] -> P_tac_apply (p_term t)
             | T_apply, _ -> assert false
             | T_assume, [prefix;_;Abst (_, t)] ->
-              let v = new_var (string_of_term pos prefix) in
-              let n = Pos.make pos (uniq_name v) in
+              let v = uniq_name (new_var (string_of_term pos prefix)) in
+              let n = Pos.make pos v and v = new_var v in
               P_tac_and (Pos.make pos (P_tac_assume [Some n]),
                          tac_eval (subst t (mk_Vari v)))
             | T_assume, _ -> assert false
@@ -420,6 +472,8 @@ let p_tactic (ss:Sig_state.t) (g:goal) (env:Env.t) (pos:Pos.popt) (t:term)
             | T_try, [t] -> P_tac_try(tac_eval t)
             | T_try, _ -> assert false
             | T_why3, _ -> P_tac_why3 None
+            | T_with_goal, [t] -> P_tac_with_goal (p_term t)
+            | T_with_goal, _ -> assert false
           with Not_found ->
             fatal pos "Unhandled tactic expression: %a." term t
         end
@@ -717,6 +771,12 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
             Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
         | _ -> assert false
       end
+  | P_tac_with_goal t ->
+      let goal = get_goal pos ss gt in
+      let t = scope t in
+      let t = mk_Appl (t, goal) in
+      if (Logger.log_enabled ()) then log "WITH_GOAL [%a]\n" term t;
+      handle ps (p_tactic ss g env pos t)
   | P_tac_try t ->
       begin try handle ps t with Fatal _ -> ps end
   | P_tac_orelse(t1,t2) ->

src/parsing/pretty.ml

@@ -341,6 +341,7 @@ let rec tactic : p_tactic pp = fun ppf { elt;  _ } ->
   | P_tac_why3 p ->
       let prover ppf s = out ppf " \"%s\"" s in
       out ppf "why3%a" (Option.pp prover) p
+  | P_tac_with_goal t -> out ppf "with_goal %a" term t
   end
 
 let rec subproof : p_subproof pp = fun ppf sp ->

src/parsing/syntax.ml

@@ -291,6 +291,7 @@ type p_tactic_aux =
   | P_tac_sym
   | P_tac_try of p_tactic
   | P_tac_why3 of string option
+  | P_tac_with_goal of p_term
 
 and p_tactic = p_tactic_aux loc
 
@@ -455,6 +456,7 @@ let eq_simp_flag : simp_flag eq = fun s1 s2 ->
 let eq_p_tactic : p_tactic eq = fun {elt=t1;_} {elt=t2;_} ->
   match t1, t2 with
   | P_tac_first_hyp t1, P_tac_first_hyp t2
+  | P_tac_with_goal t1, P_tac_with_goal t2
   | P_tac_apply t1, P_tac_apply t2
   | P_tac_refine t1, P_tac_refine t2 -> eq_p_term t1 t2
   | P_tac_have(i1,t1), P_tac_have(i2,t2) ->
@@ -673,6 +675,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
     | P_tac_refl
     | P_tac_sym
     | P_tac_why3 _
+    | P_tac_with_goal _
     | P_tac_solve
     | P_tac_fail
     | P_tac_focus _

tests/OK/Tactic.lp

@@ -46,7 +46,8 @@ builtin "induction" ≔ #induction;
 constant symbol #orelse : Tactic → Tactic → Tactic;
 builtin "orelse" ≔ #orelse;
 
-constant symbol #refine [p] : π p → Tactic;
+/*constant symbol #refine [p] : π p → Tactic;*/
+constant symbol #refine: String → Tactic;
 builtin "refine" ≔ #refine;
 
 constant symbol #reflexivity : Tactic;
@@ -82,6 +83,9 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
+constant symbol #with_goal : (Prop → Tactic) → Tactic;
+builtin "with_goal" ≔ #with_goal;
+
 constant symbol #change : Tactic;
 builtin "change" ≔ #change;
 

tests/OK/with_goal.lp

@@ -0,0 +1,24 @@
+require open tests.OK.Tactic;
+
+injective symbol σ: Prop → Set;
+rule π $P ↪ τ (σ $P);
+
+constant symbol ∀[T]: (τ T → Prop) → Prop;
+notation ∀ quantifier;
+rule π (@∀ $T $P) ↪ Π (x: τ $T), π ($P x);
+constant symbol ⇒: Prop → Prop → Prop;
+notation ⇒ infix right 7;
+builtin "imp" ≔ ⇒;
+builtin "all" ≔ ∀;
+constant symbol T: Set;
+constant symbol P: τ T → Prop;
+
+sequential symbol prove: Prop → Tactic;
+rule prove (@∀ $T $P) ↪ #assume "x" (λ (x: τ $T), prove ($P x))
+with prove ($P ⇒ $Q) ↪ #assume "h" (λ (h: π $P), prove $Q)
+with prove _ ↪ #print "" & #assumption;
+
+symbol test : Π x,  π (P x) → π (P x) ≔
+begin
+  eval (#with_goal prove);
+end;

tests/export_dk.sh

@@ -48,7 +48,7 @@ do
         # use builtin strings
         Tactic|1374);;
         # requires an excluded file
-        assume|first_hyp);;
+        assume|first_hyp|with_goal);;
         # default case
         *) translate $f.lp;;
     esac

tests/export_raw_dk.sh

@@ -59,7 +59,7 @@ do
         # module alias
         alias);;
         # proofs
-        why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp);;
+        why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|with_goal);;
         # "open"
         triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|1374|Option|String|HOL|Impred|PropExt|Classic|Comp|Pos|Z|1217|1151|B1|B2|C1|C2|C3|Epsilon|1313|FunExt|Prod);;
         # "inductive"