add manual trivial application to conseq variant

Author: oskgo

src/ecPrinting.ml

@@ -620,7 +620,10 @@ let pp_modtype1 (ppe : PPEnv.t) fmt mty =
 
 (* -------------------------------------------------------------------- *)
 let pp_local (ppe : PPEnv.t) fmt x =
-  Format.fprintf fmt "%s" (EcIdent.name x)
+  if debug_mode then
+    Format.fprintf fmt "%s<%s>" (EcIdent.name x) (EcIdent.tostring_internal x)
+  else
+    Format.fprintf fmt "%s" (EcIdent.name x)
 
 (* -------------------------------------------------------------------- *)
 let pp_local ?fv (ppe : PPEnv.t) fmt x =

src/phl/ecPhlConseq.ml

@@ -1120,7 +1120,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
                   t_intros_i [m;h0] @! t_cutdef
                     (ptlocal ~args:[pamemory m; palocal h0] hi)
                     mpre @! EcLowGoal.t_trivial;
-                  t_mytrivial;
+                  t_mytrivial @! t_intros_i [m; h0] @! t_apply_hyp h0;
                   t_apply_hyp hh];
                 tac pre posta @+ [
                   t_apply_hyp hi;

tests/conseq_phoare_hoare.ec

@@ -0,0 +1,14 @@
+require import Real.
+
+module Foo = {proc foo() = {}}.
+
+lemma foo_ll : islossless Foo.foo by islossless.
+
+op [opaque] p = predT<:int>.
+
+lemma foo_h: hoare [ Foo.foo : true ==> forall j, p j]. 
+proof. by proc; auto => /> j; rewrite /p. qed.
+
+lemma foo_p: phoare[ Foo.foo : true ==> forall j, p j] = 1%r.
+by conseq foo_ll foo_h.
+qed.