out of TCB

src/ecCoreLib.ml

@@ -241,6 +241,7 @@ module CI_Logic = struct
   let p_and_proj_r    = _Logic "andWr"
   let p_anda_proj_l   = _Logic "andaWl"
   let p_anda_proj_r   = _Logic "andaWr"
+  let p_anda_proj_rs  = _Logic "andaWrs"
   let p_or_elim       = _Logic "orW"
   let p_ora_elim      = _Logic "oraW"
   let p_iff_elim      = _Logic "iffW"
@@ -249,6 +250,7 @@ module CI_Logic = struct
   let p_true_intro    = _Logic "trueI"
   let p_and_intro     = _Logic "andI"
   let p_anda_intro    = _Logic "andaI"
+  let p_anda_intro_s  = _Logic "andaIs"
   let p_or_intro_l    = _Logic "orIl"
   let p_ora_intro_l   = _Logic "oraIl"
   let p_or_intro_r    = _Logic "orIr"

src/ecCoreLib.mli

@@ -213,6 +213,7 @@ module CI_Logic : sig
   val p_and_proj_r    : path
   val p_anda_proj_l   : path
   val p_anda_proj_r   : path
+  val p_anda_proj_rs  : path
   val p_or_elim       : path
   val p_ora_elim      : path
   val p_iff_elim      : path
@@ -221,6 +222,7 @@ module CI_Logic : sig
   val p_true_intro    : path
   val p_and_intro     : path
   val p_anda_intro    : path
+  val p_anda_intro_s  : path
   val p_or_intro_l    : path
   val p_ora_intro_l   : path
   val p_or_intro_r    : path

src/ecLowGoal.ml

@@ -1515,15 +1515,15 @@ let t_elim_iso_or ?reduce tc =
 let t_split_and_i (i : int) (f : form) (tc : tcenv1) =
   assert (0 <= i);
 
-  let fsl, fsr =
+  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
-        | _ -> assert false in
+        | _ -> tc_error !!tc ~catchable:true  "not enought conjunctions" in
 
     destr [] i f in
 
@@ -1534,65 +1534,54 @@ let t_split_and_i (i : int) (f : form) (tc : tcenv1) =
       | (b, f) :: fs ->
           (match b with `Asym -> f_anda | `Sym -> f_and) f (doit fs) in
 
-    doit fsl in
+    doit xfsl 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
 
-  tc
-
-  (*
-(* -------------------------------------------------------------------- *)
-require import AllCore.
-
-lemma test : forall a b c d, a && (b /\ (c /\ d)).
-proof.
-move => *.
-split 1.
-admit.
-
-gl = a && b
-gr = c /\ d
-
-proja2 gl = b
-
-conja (proja1 gl) (conj (proja2 gl) gr) = a && (b /\ (c /\ d))
-
-
-
-admit.
-
-
-
-admit.
-
-
+  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
 
-abort.
+  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 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
 
+  let pt =
+    List.fold_right
+      (fun (sym, ptproj) pt ->
+        `App (`G (pintro sym, []), [`H_; `H_; `Sub ptproj; `Sub pt]))
+      projs (`HD gr :> prept) in
 
-  FApi.xmutate1
-    tc (fun hd -> VConv (hd, Sid.empty)) [fsl; fsr]
-*)
+  let pt = pt_of_prept_r pte pt in
 
-(*
-  if i <= 0 then begin
-    let tc =
-      FApi.mutate1 tc (fun hd -> VConv (hd, Sid.empty))
-        (EcFol.f_and f1 f2)
-    in
-    t_and_intro_s opsym (f1, f2) tc
-  end else begin
-    match sform_of_form f2 with
-    | SFand (b, (f1', f2')) ->
-      t_and_i (i - 1) b (EcFol.f_and f1 f1', f2') tc
-    | _ ->
-      t_and_intro_s opsym (f1, f2) tc
-  end
-  *)
+  FApi.t_first (Apply.t_apply_bwd_r pt) tc
 
 (* -------------------------------------------------------------------- *)
 let t_split ?(i = 0) ?(closeonly = false) ?reduce (tc : tcenv1) =

src/ecMatching.ml

@@ -487,10 +487,10 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
           with EcUnify.UnificationFailure _ -> failure ()
       end
 
-      | Flocal x, _ ->
+      | Flocal x, _ when EV.mem x !ev.evm_form ->
           var_form_match (x, f1.f_ty) f2
 
-      | _, Flocal y ->
+      | _, Flocal y when EV.mem y !ev.evm_form ->
           var_form_match (y, f2.f_ty) f1
 
       | Fapp (f1, fs1), Fapp (f2, fs2) ->

src/ecProofTerm.ml

@@ -746,7 +746,6 @@ and apply_pterm_to_oarg ?loc ({ ptev_env = pe; ptev_pt = rawpt; } as pt) oarg =
 
   let oarg = oarg |> omap (fun arg -> arg.ptea_arg) in
 
-
   match PT.destruct_product pe.pte_hy (get_head_symbol pe pt.ptev_ax) with
   | None   -> tc_pterm_apperror ?loc pe AE_NotFunctional
   | Some t ->
@@ -757,6 +756,7 @@ and apply_pterm_to_oarg ?loc ({ ptev_env = pe; ptev_pt = rawpt; } as pt) oarg =
             | PVASub arg -> begin
               try
                 pf_form_match ~mode:EcMatching.fmdelta pe ~ptn:f1 arg.ptev_ax;
+
                 (f2, PASub (Some arg.ptev_pt))
               with EcMatching.MatchFailure ->
                 tc_pterm_apperror ?loc pe (AE_InvalidArgProof (arg.ptev_ax, f1))
@@ -911,6 +911,7 @@ type prept = [
   | `G    of EcPath.path * ty list
   | `UG   of EcPath.path
   | `HD   of handle
+  | `PE   of pt_ev
   | `App  of prept * prept_arg list
 ]
 
@@ -923,14 +924,13 @@ and prept_arg =  [
 ]
 
 (* -------------------------------------------------------------------- *)
-let pt_of_prept tc (pt : prept) =
-  let ptenv = ptenv_of_penv (FApi.tc1_hyps tc) !!tc in
-
-  let rec build_pt = function
+let pt_of_prept_r (ptenv : pt_env) : prept -> pt_ev =
+  let rec build_pt : prept -> pt_ev = function
     | `Hy  id         -> pt_of_hyp_r ptenv id
     | `G   (p, tys)   -> pt_of_global_r ptenv p tys
     | `UG  p          -> pt_of_global_r ptenv p []
     | `HD  hd         -> pt_of_handle_r ptenv hd
+    | `PE  pe         -> pe
     | `App (pt, args) -> List.fold_left app_pt_ev (build_pt pt) args
 
   and app_pt_ev pt_ev = function
@@ -940,7 +940,12 @@ let pt_of_prept tc (pt : prept) =
     | `Sub pt -> apply_pterm_to_arg_r pt_ev (PVASub (build_pt pt))
     | `H_     -> apply_pterm_to_hole pt_ev
 
-  in build_pt pt
+  in fun pt -> build_pt pt
+
+(* -------------------------------------------------------------------- *)
+let pt_of_prept (tc : tcenv1) (pt : prept) : pt_ev =
+  let ptenv = ptenv_of_penv (FApi.tc1_hyps tc) !!tc in
+  pt_of_prept_r ptenv pt
 
 (* -------------------------------------------------------------------- *)
 module Prept = struct

src/ecProofTerm.mli

@@ -166,6 +166,7 @@ type prept = [
   | `G    of EcPath.path * ty list
   | `UG   of EcPath.path
   | `HD   of handle
+  | `PE   of pt_ev
   | `App  of prept * prept_arg list
 ]
 
@@ -177,6 +178,7 @@ and prept_arg =  [
   | `H_
 ]
 
+val pt_of_prept_r: pt_env -> prept -> pt_ev
 val pt_of_prept: tcenv1 -> prept -> pt_ev
 
 (* -------------------------------------------------------------------- *)

tests/split.ec

@@ -0,0 +1,35 @@
+(* -------------------------------------------------------------------- *)
+require import AllCore.
+
+print andWr.
+
+lemma test : forall a b c d e f, a && b /\ c && d /\ e /\ f.
+proof.
+move=> *.
+
+split 5.
+split.
+admit.
+
+
+
+gl = a && b
+gr = c /\ d
+
+proja2 gl = b
+
+conja (proja1 gl) (conj (proja2 gl) gr) = a && (b /\ (c /\ d))
+
+
+
+admit.
+
+
+
+admit.
+
+
+
+
+abort.
+

theories/prelude/Tactics.ec

@@ -28,8 +28,10 @@ lemma andaW a b c : (a => b => c) => (a && b) => c by smt().
 
 lemma andaWl a b : (a && b) => a by smt().
 lemma andaWr a b : (a && b) => (a => b) by smt().
+lemma andaWrs a b : (a && b) => b by smt().
 
 lemma andaI a b : a => (a => b) => (a && b) by smt().
+lemma andaIs a b : a => b => (a && b) by smt().
 
 (* -------------------------------------------------------------------- *)
 lemma oraW a b c : (a => c) => (!a => b => c) => (a || b) => c by smt().