Fix why3 tactic (#1174)

- why3_tactic.ml: many fixes (fix #1165) and changes
- fol.ml: add fields symb_Prop and sym_Set (domains of symb_P and symb_T), and symb_eqv
- tests: merged why3_quantifiers.lp into why3.lp
- rewrite.ml: make get_eq_data return a list instead of an array, and rename local function check_t_or_p into check_codomain_is_Type
- tactic.ml: introduce the functions get_prod_ids and gen_valid_idopts, and improve assume so that it uses the user-defined variable names instead of h1, h2, etc.
- base.ml: add char
- list: add assoc_eq_opt

As before, the why3 tactic starts by doing some assume. Then, the tactic tries to translate the environment as much as possible, and then the goal. The tactic fails if the goal cannot be translated.

A term [t:Set] is translated to a Why3 type if it is algebraic (i.e. built from function applications and variables only) and its variables are in the environment.

A term [t:T _] is translated to a Why3 term if it is algebraic and its variables are in the environment or are quantified variables.

A term [t:P _] is translated to a Why3 formula if it has the form of a formula in predicate calculus. Subterms that are not in predicate calculus are replaced by fresh propositions.

TODO:
- [ ] when abstracting a subformula, compute its free variables, check that they are quantified, and replace the subterm by the application of a fresh predicate applied to those variables. Example:
```opaque symbol test11 a p x q : π ((`∀ x:τ a, p x ⇒ (λ y, q y) x) ⇒ p x ⇒ (λ y, q y) x) ≔ begin why3 end;```
- [ ] make translate_term abstract non-Why3 subterms too. Example:
```opaque symbol test12 a p x q : π ((`∀ x:τ a, p x ⇒ q ((λ y,y)x)) ⇒ p x ⇒ q ((λ y,y)x)) ≔ begin why3 end;```
- [ ] take into account rule on T and P; make the translation invariant by reduction

src/common/debug.ml

@@ -26,7 +26,7 @@ module D = struct
     | Some x -> out ppf "Some(%a)" elt x
 
   let pair : 'a pp -> 'b pp -> ('a * 'b) pp = fun elt1 elt2 ppf (x1,x2) ->
-    out ppf "%a,%a" elt1 x1 elt2 x2
+    out ppf "(%a,%a)" elt1 x1 elt2 x2
 
   let list : 'a pp -> 'a list pp = fun elt ppf l ->
     match l with

src/handle/fol.ml

@@ -1,15 +1,18 @@
 (** Configuration for tactics based on first-order logic. *)
 
-open Common
+open Common open Error
 open Core open Term
 
 (** Builtin configuration for propositional logic. *)
 type config =
-  { symb_P   : sym (** Encoding of propositions. *)
+  { 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_or  : sym (** Disjunction(∨) symbol. *)
   ; symb_and : sym (** Conjunction(∧) symbol. *)
   ; symb_imp : sym (** Implication(⇒) symbol. *)
+  ; symb_eqv : sym (** Equivalence(⇔) symbol. *)
   ; symb_bot : sym (** Bot(⊥) symbol. *)
   ; symb_top : sym (** Top(⊤) symbol. *)
   ; symb_not : sym (** Not(¬) symbol. *)
@@ -19,11 +22,38 @@ type config =
 (** [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
-  { symb_P   = builtin "P"
-  ; symb_T   = builtin "T"
+  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_or  = builtin "or"
   ; symb_and = builtin "and"
   ; symb_imp = builtin "imp"
+  ; symb_eqv = builtin "eqv"
   ; symb_bot = builtin "bot"
   ; symb_top = builtin "top"
   ; symb_not = builtin "not"

src/handle/rewrite.ml

@@ -30,7 +30,7 @@ let get_eq_config : Sig_state.t -> popt -> eq_config = fun ss pos ->
 
 (* Register checks for the builtin symbols related to rewriting. *)
 let _ =
-  let check_t_or_p _ss pos sym =
+  let check_codomain_is_Type _ss pos sym =
     let valid =
       match Eval.whnf [] !(sym.sym_type) with
       | Prod(_, b) -> Eval.eq_modulo [] (snd (Bindlib.unbind b)) mk_Type
@@ -40,9 +40,9 @@ let _ =
       fatal pos "The type of [%s] is not of the form [_ → TYPE]." sym.sym_name
   in
   (* The type of the builtin ["T"] should be [U → TYPE]. *)
-  Builtin.register "T" check_t_or_p;
+  Builtin.register "T" check_codomain_is_Type;
   (* The type of the builtin ["P"] should be [Prop → TYPE]. *)
-  Builtin.register "P" check_t_or_p;
+  Builtin.register "P" check_codomain_is_Type;
   let get_domain_of_type s =
     match Eval.whnf [] !(s.sym_type) with
     | Prod(a,_) -> a
@@ -109,7 +109,7 @@ let _ =
 (** [get_eq_data pos cfg a] returns [((a,l,r),[v1;..;vn])] if [a ≡ Π v1:A1,
    .., Π vn:An, P (eq a l r)] and fails otherwise. *)
 let get_eq_data :
-  eq_config -> popt -> term -> (term * term * term) * tvar array = fun cfg ->
+  eq_config -> popt -> term -> (term * term * term) * tvar list = fun cfg ->
   let exception Not_eq of term in
   let get_eq_args u =
     if Logger.log_enabled () then log_rewr "get_eq_args %a" term u;
@@ -118,14 +118,14 @@ let get_eq_data :
     | _ -> raise (Not_eq u)
   in
   let exception Not_P of term in
-  let return vs r = r, Array.of_list (List.rev vs) in
+  let return vs r = r, List.rev vs in
   let rec get_eq vs t notin_whnf =
     if Logger.log_enabled () then log_rewr "get_eq %a" term t;
     match get_args t with
     | Prod(_,t), _ -> let v,t = Bindlib.unbind t in get_eq (v::vs) t true
     | p, [u] when is_symb cfg.symb_P p ->
       begin
-        let u = Eval.whnf ~tags:[`NoRw; `NoExpand] [] u in
+        let u = Eval.whnf ~tags:[`NoRw;`NoExpand] [] u in
         try return vs (get_eq_args u)
         with Not_eq _ ->
           (try return vs (get_eq_args (Eval.whnf [] u))
@@ -327,7 +327,8 @@ let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool ->
   let (t, t_type) = Query.infer pos p g_ctxt t in
 
   (* Check that [t_type ≡ Π x1:a1, ..., Π xn:an, P (eq a l r)]. *)
-  let (a, l, r), vars  = get_eq_data cfg pos t_type in
+  let (a, l, r), vars = get_eq_data cfg pos t_type in
+  let vars = Array.of_list vars in
 
   (* Apply [t] to the variables of [vars] to get a witness of the equality. *)
   let t = Array.fold_left (fun t x -> mk_Appl(t, mk_Vari x)) t vars in

src/handle/tactic.ml

@@ -185,6 +185,33 @@ let count_products : ctxt -> term -> int = fun c ->
     | _ -> acc
   in count 0
 
+(** [get_prod_ids env do_whnf t] returns the list [v1;..;vn] if [do_whnf] is
+    true and [whnf t] is of the form [Π v1:A1, .., Π vn:An, u] with [u] not a
+    product, or if [do_whnf] is false and [t] is of the form [Π v1:A1, .., Π
+    vn:An, u] with [u] not a product. *)
+let get_prod_ids env =
+  let rec aux acc do_whnf t =
+    match get_args t with
+    | Prod(_,b), _ ->
+        let x,b = Bindlib.unbind b in
+        aux (Bindlib.name_of x::acc) do_whnf b
+    | _ ->
+        if do_whnf then aux acc false (Eval.whnf (Env.to_ctxt env) t)
+        else List.rev acc
+  in aux []
+
+(** [gen_valid_idopts env ids] generates a list of pairwise distinct
+    identifiers distinct from those of [env] to replace [ids]. *)
+let gen_valid_idopts env ids =
+  let add_decl ids (s,_) = Extra.StrSet.add s ids in
+  let idset = ref (List.fold_left add_decl Extra.StrSet.empty env) in
+  let f id idopts =
+    let id = Extra.get_safe_prefix id !idset in
+    idset := Extra.StrSet.add id !idset;
+    Some(Pos.none id)::idopts
+  in
+  List.fold_right f ids []
+
 (** [handle ss sym_pos prv ps tac] applies tactic [tac] in the proof state
    [ps] and returns the new proof state. *)
 let rec handle :
@@ -209,26 +236,17 @@ let rec handle :
   | Unif _ -> fatal pos "Not a typing goal."
   | Typ ({goal_hyps=env;_} as gt) ->
   let scope t = Scope.scope_term ~mok:(Proof.meta_of_key ps) prv ss env t in
+  (* Function to apply the assume tactic several times without checking the
+     validity of identifiers. *)
+  let assume idopts =
+    match idopts with
+    | [] -> ps
+    | _ -> tac_refine pos ps gt gs (new_problem())
+             (scope (P.abst_list idopts P.wild))
+  in
   (* Function for checking that an identifier is not already in use. *)
   let check id =
     if Env.mem id.elt env then fatal id.pos "Identifier already in use." in
-  (* Function to apply [n] times the assume tactic. *)
-  let assume n =
-    if n <= 0 then ps
-    else
-      let add_decl strings (s,_) = Extra.StrSet.add s strings in
-      let strings = List.fold_left add_decl Extra.StrSet.empty env in
-      let h = Extra.get_safe_prefix "h" strings in
-      let rec mk_idopts acc k =
-        if k <= 0 then acc
-        else
-          let idopt = Some (Pos.make pos (h ^ string_of_int k)) in
-          mk_idopts (idopt::acc) (k-1)
-      in
-      let t = P.abst_list (mk_idopts [] n) P.wild in
-      let p = new_problem() in
-      tac_refine pos ps gt gs p (scope t)
-  in
   match elt with
   | P_tac_fail
   | P_tac_query _
@@ -257,8 +275,7 @@ let rec handle :
       List.iter (Option.iter check) idopts;
       (* Check that the given identifiers are pairwise distinct. *)
       Syntax.check_distinct_idopts idopts;
-      let p = new_problem() in
-      tac_refine pos ps gt gs p (scope (P.abst_list idopts P.wild))
+      assume idopts
   | P_tac_generalize {elt=id; pos=idpos} ->
       (* From a goal [e1,id:a,e2 ⊢ ?[e1,id,e2] : u], generate a new goal [e1 ⊢
          ?m[e1] : Π id:a, Π e2, u], and refine [?[e]] with [?m[e1] id e2]. *)
@@ -330,20 +347,19 @@ let rec handle :
   | P_tac_induction -> tac_induction pos ps gt gs
   | P_tac_refine t -> tac_refine pos ps gt gs (new_problem()) (scope t)
   | P_tac_refl ->
-      let cfg = Rewrite.get_eq_config ss pos in
-      let (a,l,_), vs = Rewrite.get_eq_data cfg pos gt.goal_type in
-      (* We first do [n] times the [assume] tactic. *)
-      let ps = assume (Array.length vs) in
-      (* We then apply reflexivity. *)
-      begin match ps.proof_goals with
-      | Typ gt::gs ->
-        let a,l =
-          if Array.length vs = 0 then a,l
-          else let (a,l,_),_ = Rewrite.get_eq_data cfg pos gt.goal_type in a,l
-        in
-        let prf = add_args (mk_Symb cfg.symb_refl) [a; l] in
-        tac_refine pos ps gt gs (new_problem()) prf
-      | _ -> assert false
+      begin
+        let cfg = Rewrite.get_eq_config ss pos in
+        let _,vs = Rewrite.get_eq_data cfg pos gt.goal_type in
+        let idopts = gen_valid_idopts env (List.map Bindlib.name_of vs) in
+        let ps = assume idopts in
+        match ps.proof_goals with
+        | [] -> assert false
+        | Unif _::_ -> assert false
+        | Typ gt::gs ->
+            let cfg = Rewrite.get_eq_config ss pos in
+            let (a,l,_),_ = Rewrite.get_eq_data cfg pos gt.goal_type in
+            let prf = add_args (mk_Symb cfg.symb_refl) [a; l] in
+            tac_refine pos ps gt gs (new_problem()) prf
       end
   | P_tac_remove ids ->
       (* Remove hypothesis [id] in goal [g]. *)
@@ -389,27 +405,26 @@ let rec handle :
         (Rewrite.rewrite ss p pos gt l2r pat (scope eq))
   | P_tac_sym ->
       let cfg = Rewrite.get_eq_config ss pos in
-      let (a,l,r), vs = Rewrite.get_eq_data cfg pos gt.goal_type in
-      let a,l,r =
-        if Array.length vs = 0 then a,l,r
-        else fst (Rewrite.get_eq_data cfg pos gt.goal_type)
-      in
+      let (a,l,r),_ = Rewrite.get_eq_data cfg pos gt.goal_type in
       let p = new_problem() in
       let prf =
-        let mt =
-          mk_Appl(mk_Symb cfg.symb_P,
-                  add_args (mk_Symb cfg.symb_eq) [a; r; l]) in
+        let mt = mk_Appl(mk_Symb cfg.symb_P,
+                         add_args (mk_Symb cfg.symb_eq) [a;r;l]) in
         let meta_term = LibMeta.make p (Env.to_ctxt env) mt in
         (* The proofterm is [eqind a r l M (λx,eq a l x) (refl a l)]. *)
         Rewrite.swap cfg a r l meta_term
       in
       tac_refine pos ps gt gs p prf
   | P_tac_why3 cfg ->
-      let ps = assume (count_products (Env.to_ctxt env) gt.goal_type) in
-      (match ps.proof_goals with
-       | Typ gt::_ ->
-         Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
-       | _ -> assert false)
+      begin
+        let ids = get_prod_ids env false gt.goal_type in
+        let idopts = gen_valid_idopts env ids in
+        let ps = assume idopts in
+        match ps.proof_goals with
+        | Typ gt::_ ->
+            Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
+        | _ -> assert false
+      end
   | P_tac_try tactic ->
     try handle ss sym_pos prv ps tactic
     with Fatal(_, _s) -> ps