[tactic] Actually improve one-sided match robustness (fixes #799)

Author: Cameron-Low

src/phl/ecPhlCond.ml

@@ -190,10 +190,12 @@ end = struct
         let discharge_post tc =
           let+ tc =
             if   Option.is_some side
-            then EcLowGoal.t_intros_n 3 tc
-            else EcLowGoal.t_intros_n 2 tc
+            then EcLowGoal.t_intros_n 2 tc
+            else EcLowGoal.t_intros_n 1 tc
           in
-          EcLowGoal.t_assumption `Alpha tc
+          let t_imp = EcLowGoal.t_intros_n 1 @! EcLowGoal.t_assumption `Alpha in
+          let t_iff = EcLowGoal.t_split @! t_imp in
+          tc |> FApi.t_or t_imp t_iff
         in
 
         let pre = oget (EcLowPhlGoal.get_pre (FApi.tc1_goal tc)) in

tests/single_match.ec

@@ -1,3 +1,5 @@
+require import AllCore.
+
 op w : unit option.
 
 module M = {
@@ -9,10 +11,46 @@ module M = {
   }
 }.
 
-hoare L: M.f: exists x, x = true ==> true.
+hoare L1: M.f: exists x, x = true ==> true.
+proof.
+proc.
+match.
++ by skip.
++ by skip.
+qed.
+
+phoare L2: [M.f: exists x, x = true ==> true] <= 1%r.
+proof.
+proc.
+match.
++ by skip.
++ by skip.
+qed.
+
+phoare L3: [M.f: exists x, x = true ==> true] = 1%r.
 proof.
 proc.
 match.
 + by skip.
 + by skip.
 qed.
+
+phoare L4: [M.f: exists x, x = true ==> true] >= 1%r.
+proof.
+proc.
+match.
++ by skip.
++ by skip.
+qed.
+
+equiv L5: M.f ~ M.f: exists x, x = true ==> true.
+proof.
+proc.
+match {1}.
++ match {2}.
+  + by skip.
+  + by skip.
++ match {2}.
+  + by skip.
+  + by skip.
+qed.