From 437a4e9f75fb5168324dedbaf988febfab243aee Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@mpi-sp.org>
Date: Tue, 24 Dec 2024 01:37:21 +0100
Subject: [PATCH] Fix Asym split

---
 src/ecLowGoal.ml | 97 +++++++++++++++++++++++++-----------------------
 1 file changed, 50 insertions(+), 47 deletions(-)

diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
index 8dca6526c..91411d112 100644
--- a/src/ecLowGoal.ml
+++ b/src/ecLowGoal.ml
@@ -1511,72 +1511,77 @@ let t_elim_iso_or ?reduce tc =
 
 
 (* -------------------------------------------------------------------- *)
-let t_split_and_i (i : int) (f : form) (tc : tcenv1) =
-  assert (0 <= i);
-
-  let xfsl, fsr =
-    let rec destr (acc : ([`Asym | `Sym] * form) list) (i  : int) (f : form) =
-      if i < 0 then
-        (List.rev acc, f)
-      else
-        match sform_of_form f with
-        | SFand (b, (f1, f2)) ->
-            destr ((b, f1) :: acc) (i - 1) f2
-        | _ -> tc_error !!tc ~catchable:true  "not enought conjunctions" in
-
-    destr [] i f in
+let t_split_and_i i b f1 f2 tc =
+  (* if i <= 0 then *)
+  (*   t_and_intro_s b (f1, f2) tc *)
+  (* else *)
+  let i = i - 1 in
+  let rec destr acc_sym acc_f i f =
+    if i < 0 then
+      acc_sym, acc_f, f
+    else
+      match sform_of_form f with
+      | SFand (b, (f1, f2)) ->
+        destr (b :: acc_sym) (f1 :: acc_f) (i - 1) f2
+      | _ -> tc_error !!tc ~catchable:true  "not enought conjunctions" in
 
-  let fsl =
-    let rec doit = function
-      | [] -> assert false
-      | [_, f] -> f
-      | (b, f) :: fs ->
-          (match b with `Asym -> f_anda | `Sym -> f_and) f (doit fs) in
+  let rec constr l_sym l_f =
+    match l_sym, l_f with
+    | [_], [f] -> f
+    | `Asym :: sym , f :: fs -> f_anda f (constr sym fs)
+    | `Sym :: sym,  f :: fs -> f_and f (constr sym fs)
+    | _, _ -> assert false in
 
-    doit xfsl in
+  let l_sym , l_f, fsr = destr [b] [f1] i f2 in
+  let fsl = constr (List.rev l_sym) (List.rev l_f) in
 
   let tc = FApi.tcenv_of_tcenv1 tc in
   let tc, gl = FApi.newgoal tc fsl in
-  let tc, gr = FApi.newgoal tc fsr in
+
+  let sym = List.hd l_sym in
+  let syms = List.rev (List.tl l_sym) in
+
+  let tc, gr =
+    match sym with
+    | `Asym ->
+      let fsr = f_imp fsl fsr in
+      let tc, gr = FApi.newgoal tc fsr in
+      tc,`App (`HD gr, [`Sub (`HD gl:>prept)])
+    | `Sym ->
+      let tc, gr = FApi.newgoal tc fsr in
+      tc,(`HD gr:>prept)
+  in
 
   let pelim (sym : [`Sym | `Asym]) (side : [`L | `R]) =
     match sym, side with
     | `Sym , `L -> LG.p_and_proj_l
     | `Sym , `R -> LG.p_and_proj_r
     | `Asym, `L -> LG.p_anda_proj_l
-    | `Asym, `R -> LG.p_anda_proj_rs
-  in
-
-  let pintro (sym  : [`Sym | `Asym]) =
-    match sym with
-    | `Sym  -> LG.p_and_intro
-    | `Asym -> LG.p_anda_intro_s in
+    | `Asym, `R -> LG.p_anda_proj_rs in
 
   let pte = ptenv_of_penv (FApi.tc_hyps tc) !$tc in
 
-  let projs =
-    let xfsl, sym =
-      match List.rev xfsl with
-      | [] -> assert false
-      | (sym, _) :: tl -> List.rev tl, sym in
-
-    let proj, projs =
-      List.fold_left_map (fun h (sym, _) ->
+  let proj, projs =
+    List.fold_left_map (fun h sym ->
         let j : prept = `App (`G (pelim sym `L, []), [`H_; `H_; `Sub h]) in
         let h : prept = `App (`G (pelim sym `R, []), [`H_; `H_; `Sub h]) in
         let j = pt_of_prept_r pte j in
         let h = pt_of_prept_r pte h in
-        assert (PT.can_concretize j.ptev_env);
-        assert (PT.can_concretize h.ptev_env);
         (`PE h, (sym, `PE j))
-      ) (`HD gl :> prept) xfsl
-    in projs @ [sym, proj] in
+      ) (`HD gl :> prept) syms in
+
+  let projs = projs @ [sym, proj] in
+
+  let pintro (sym  : [`Sym | `Asym]) =
+    match sym with
+    | `Sym  -> LG.p_and_intro
+    | `Asym -> LG.p_anda_intro_s in
 
   let pt =
     List.fold_right
       (fun (sym, ptproj) pt ->
-        `App (`G (pintro sym, []), [`H_; `H_; `Sub ptproj; `Sub pt]))
-      projs (`HD gr :> prept) in
+         `App (`G (pintro sym, []), [`H_; `H_; `Sub ptproj; `Sub pt]))
+      projs gr in
 
   let pt = pt_of_prept_r pte pt in
 
@@ -1590,10 +1595,8 @@ let t_split ?(i = 0) ?(closeonly = false) ?reduce (tc : tcenv1) =
     match sform_of_form fp with
     | SFtrue ->
         t_true tc
-    | SFand (b, (f1,f2)) when not closeonly && i = 0 ->
-        t_and_intro_s b (f1, f2) tc
-    | SFand _ when not closeonly ->
-        t_split_and_i i fp tc
+    | SFand (b, (f1,f2)) when not closeonly ->
+        t_split_and_i i b f1 f2 tc
     | SFiff (f1, f2) when not closeonly ->
         t_iff_intro_s (f1, f2) tc
     | SFeq (f1, f2) when not closeonly && (is_tuple f1 && is_tuple f2) ->