The why3 encoding is wrong for the quantifier and predicates

[NotBad4U]

Hi everyone,
I know that the why3 support is quite experimental. I am playing with it because I want to reconstruct some proof steps where I do not have a trace. During my experimentation, I noticed that the why3 encoding does not use the quantified variable in its formula.
Consider the example in the test why3_quantifier.lp:

opaque symbol thm_ex : P (ex o (λ a: T o, imp a a))
≔ begin 
  why3; 
end;

It is translated into

theory Task
 predicate p
 type o
 goal main_goal : exists a:o. p -> p
end

but the correct translation should be:

theory Task
 type o
 goal main_goal : exists a:o. a -> a  (* use the quantified value a and do not generate a predicate p *)
end

I also face a problem with predicates. Consider the Lambdapi goal below:

0 : πᶜ ((`∀ᶜ x1, ¬ (a <=> x1) ∨ᶜ p x1) = (¬ (a <=> a) ∨ᶜ p a))

the why3 encoding output this Task:

 theory Task
         
         predicate p
         
         predicate p1
         
         predicate p2
         
         predicate p3
         
         type U
         
         goal main_goal :
           (forall x1:U. not (p3 <-> p2) \/ p1) <-> not (p3 <-> p3) \/ p
         
       end

First, the encoding should use the bounded variable x1 and not create a predicate p3. Second, it should not create a predicate p1, but a predicate that can take a bool as argument to encode p x1 and p a.

I am interested to contribute to fix this issue whereas I am lacking of time. Anyone who wants to help me fix this issue will be welcome.

---

If you want to print a task in Lambdapi, this is my (partial) git diff of why3_tactic.ml for printing the Task with debug +y activated:

@@ -138,14 +146,14 @@ let translate_term : config -> cnst_table -> TyTable.t -> term ->
           close [vid] [] t
         in
         (tbl, ty_tbl, tquant)
-    | _ ->
+    | _a, _args ->
         (* If the term [p] is mapped in [tbl] then use it. *)
         try
           let sym = List.assoc_eq (Eval.eq_modulo []) t tbl in
           (tbl, ty_tbl, Why3.Term.ps_app sym [])
         with Not_found ->
           (* Otherwise generate a new constant in why3. *)
-          let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "P") [] in
+          let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "p") [] in
           ((t, sym)::tbl, ty_tbl, Why3.Term.ps_app sym [])
   in
   match get_args t with
@@ -191,7 +199,9 @@ let encode : Sig_state.t -> Pos.popt -> Env.env -> term -> Why3.Task.task =
   (* Add the goal itself. *)
   let goal = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "main_goal") in
   (* Return the task that contains the encoded lambdapi formula in Why3. *)
-  Why3.Task.add_prop_decl tsk Why3.Decl.Pgoal goal why3_term
+  let tsk = Why3.Task.add_prop_decl tsk Why3.Decl.Pgoal goal why3_term in
+  log_why3 "@[task 1 is:@\n%a@]@." Why3.Pretty.print_task tsk;
+  tsk