Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sun, Feb 08, 2015 at 03:38:17PM +0100, Enrico Tassi wrote:
> > I am experimenting with machine-learning assisted automated theorem
> > proving in Coq. Right now my system gets stuck on some simple lemmas
> > from ssreflect that involve rewriting an instance of a pattern besides
> > the first, because I have not been able to systematically enumerate a
> > sufficient action space.
> 
> Ok, I'll look at the code and try to see if I can give you a decent API.

I have a patch (in attachment) for ssr 1.5 for Coq 8.5beta1

  http://ssr.msr-inria.inria.fr/FTP/

Example:

  Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

  Lemma test : 3 + 6 = 3 + (0 + 6).
  Proof.

  ssrinstancesoftpat (_ + _). (*
  BEGIN INSTANCES
  instance: (3 + 6) matches: (3 + 6)
  instance: (3 + 6) matches: (3 + (0 + 6))
  instance: (3 + (0 + 6)) matches: (3 + 6)
  instance: (3 + (0 + 6)) matches: (3 + (0 + 6))
  instance: (0 + 6) matches: (0 + 6)
  END INSTANCES *)

  ssrinstancesofruleL2R (addnC,add0n). (*
  BEGIN INSTANCES
  instance: (addnC 3 6) matches: (3 + 6)
  instance: (addnC 3 6) matches: (3 + (0 + 6))
  instance: (addnC 3 (0 + 6)) matches: (3 + 6)
  instance: (addnC 3 (0 + 6)) matches: (3 + (0 + 6))
  instance: (addnC 0 6) matches: (0 + 6)
  instance: (add0n 6) matches: (0 + 6)
  END INSTANCES *)

Note that some results are "semantically" duplicates, but not
syntactically.  The "multi rule" example is just to show that you
can put there any lemma (some lemmas are multi rules).

If someone suggests a less horrible syntax we could even keep
these functionalities, they could help beginners.

Hope it helps,
-- 
Enrico Tassi
diff --git a/ssreflect/v8.5/src/ssreflect.ml4 
b/ssreflect/v8.5/src/ssreflect.ml4
index 804302f..f598c21 100644
--- a/ssreflect/v8.5/src/ssreflect.ml4
+++ b/ssreflect/v8.5/src/ssreflect.ml4
@@ -4636,7 +4636,7 @@ END
 let simplintac occ rdx sim gl = 
   let simptac gl = 
     let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
-    let simp env c _ = red_safe Tacred.simpl env sigma0 c in
+    let simp env c _ _ = red_safe Tacred.simpl env sigma0 c in
     Proofview.V82.of_tactic
       (convert_concl_no_check (eval_pattern env0 sigma0 concl0 rdx occ simp))
       gl in
@@ -4674,8 +4674,8 @@ let unfoldintac occ rdx t (kt,_) gl =
     let ise, u = mk_tpattern env0 sigma0 (ise,t) all_ok L2R t in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
-    (fun env c h -> 
-      try find_T env c h (fun env c _ -> body env t c)
+    (fun env c _ h -> 
+      try find_T env c h (fun env c _ _ -> body env t c)
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm (str"No occurrence of "
         ++ pr_constr_pat t ++ spc() ++ str "in " ++ pr_constr c)),
@@ -4683,7 +4683,7 @@ let unfoldintac occ rdx t (kt,_) gl =
       | NoMatch when easy -> fake_pmatcher_end () 
       | NoMatch -> anomaly "unfoldintac")
   | _ -> 
-    (fun env (c as orig_c) h ->
+    (fun env (c as orig_c) _ h ->
       if const then
           let rec aux c = 
             match kind_of_term c with
@@ -4721,10 +4721,10 @@ let foldtac occ rdx ft gl =
     let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in
     let find_T, end_T =
       mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in
-    (fun env c h -> try find_T env c h (fun env t _ -> t) with NoMatch -> c),
+    (fun env c _ h -> try find_T env c h (fun env t _ _ -> t) with NoMatch 
->c),
     (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ())
   | _ -> 
-    (fun env c h -> try let sigma = unify_HO env sigma c t in fs sigma t
+    (fun env c _ h -> try let sigma = unify_HO env sigma c t in fs sigma t
     with _ -> errorstrm (str "fold pattern " ++ pr_constr_pat t ++ spc ()
       ++ str "does not match redex " ++ pr_constr_pat c)), 
     fake_pmatcher_end in
@@ -4889,7 +4889,7 @@ let closed0_check cl p gl =
   if closed0 cl then
     errorstrm (str"No occurrence of redex "++pf_pr_constr gl (project gl) p)
 
-let rwrxtac occ rdx_pat dir rule gl =
+let rwprocess_rule dir rule gl =
   let env = pf_env gl in
   let coq_prod = lz_coq_prod () in
   let is_setoid = ssr_is_setoid env in
@@ -4960,7 +4960,13 @@ let rwrxtac occ rdx_pat dir rule gl =
         in
     let sigma, r = rule in
     let t = Retyping.get_type_of env sigma r in
-    loop dir sigma r t [] 0 in
+    loop dir sigma r t [] 0
+  in
+    r_sigma, rules
+
+let rwrxtac occ rdx_pat dir rule gl =
+  let env = pf_env gl in
+  let r_sigma, rules = rwprocess_rule dir rule gl in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
@@ -4985,11 +4991,11 @@ let rwrxtac occ rdx_pat dir rule gl =
         sigma, pats @ [pat] in
       let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
       let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats 
in
-      find_R ~k:(fun _ _ h -> mkRel h), 
+      (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), 
       fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx
   | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T 
(e,_,_))) ->
       let r = ref None in
-      (fun env c h -> do_once r (fun () -> find_rule c, c); mkRel h),
+      (fun env c _ h -> do_once r (fun () -> find_rule c, c); mkRel h),
       (fun concl -> closed0_check concl e gl; assert_done r) in
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
@@ -5002,6 +5008,32 @@ let rwrxtac occ rdx_pat dir rule gl =
   prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl
 ;;
 
+let ssrinstancesofrule ist dir arg gl =
+  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
+  let rule = interp_term ist gl arg in
+  let r_sigma, rules = rwprocess_rule dir rule gl in
+  let find, conclude =
+    let upats_origin = dir, snd rule in
+    let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
+      let sigma, pat =
+        mk_tpattern env sigma0 (sigma,r) (rw_progress rhs) d lhs in
+      sigma, pats @ [pat] in
+    let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
+    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None 
~upats_origin rpats in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p 
++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  ppnl (str"BEGIN INSTANCES");
+  try
+    while true do
+      ignore(find env0 concl0 1 ~k:print)
+    done; raise NoMatch
+  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+
+TACTIC EXTEND ssrinstofruleL2R
+| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ Proofview.V82.tactic 
(ssrinstancesofrule ist L2R arg) ]
+END
+TACTIC EXTEND ssrinstofruleR2L
+| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ Proofview.V82.tactic 
(ssrinstancesofrule ist R2L arg) ]
+END
 
 (* Resolve forward reference *)
 let _ = 
diff --git a/ssreflect/v8.5/src/ssrmatching.ml4 
b/ssreflect/v8.5/src/ssrmatching.ml4
index 29580a6..2fd0fe6 100644
--- a/ssreflect/v8.5/src/ssrmatching.ml4
+++ b/ssreflect/v8.5/src/ssrmatching.ml4
@@ -619,7 +619,7 @@ let match_upats_FO upats env sigma0 ise c =
 ;;
 
 
-let match_upats_HO upats env sigma0 ise c =
+let match_upats_HO ~on_instance upats env sigma0 ise c =
  let it_did_match = ref false in
  let rec aux upats env sigma0 ise c =
   let f, a = splay_app ise c in let i0 = ref (-1) in
@@ -648,7 +648,7 @@ let match_upats_HO upats env sigma0 ise c =
         let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a 
in
         let lhs = mkSubApp f i a in
         let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in
-        raise (FoundUnif (ungen_upat lhs pt' u))
+        on_instance (ungen_upat lhs pt' u)
       with FoundUnif _ as sigma_u -> raise sigma_u 
       | NoProgress -> it_did_match := true
       | _ -> () in
@@ -661,8 +661,8 @@ let match_upats_HO upats env sigma0 ise c =
  if !it_did_match then raise NoProgress
 
 let prof_HO = mk_profiler "match_upats_HO";;
-let match_upats_HO upats env sigma0 ise c =
-  prof_HO.profile (match_upats_HO upats env sigma0) ise c
+let match_upats_HO ~on_instance upats env sigma0 ise c =
+  prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c
 ;;
 
 
@@ -675,7 +675,14 @@ let do_once r f = match !r with Some _ -> () | None -> r 
:= Some (f ())
 let assert_done r = 
   match !r with Some x -> x | None -> Errors.anomaly (str"do_once never 
called")
 
-type subst = Environ.env -> Term.constr -> int -> Term.constr
+let assert_done_multires r = 
+  match !r with
+  | None -> Errors.anomaly (str"do_once never called")
+  | Some (n, xs) ->
+      r := Some (n+1,xs);
+      try List.nth xs n with Failure _ -> raise NoMatch
+
+type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr
 type find_P = 
   Environ.env -> Term.constr -> int ->
   k:subst ->
@@ -684,7 +691,7 @@ type conclude = unit ->
   Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * 
Term.constr)
 
 (* upats_origin makes a better error message only            *)
-let mk_tpattern_matcher
+let mk_tpattern_matcher ?(all_instances=false)
   ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats)
 =
   let nocc = ref 0 and skip_occ = ref false in
@@ -727,13 +734,35 @@ let source () = match upats_origin, upats with
       pr_constr_pat rule ++ spc()
   | _, [] | None, _::_::_ ->
       Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
+let on_instance, instances =
+  let instances = ref [] in
+  (fun x ->
+    if all_instances then instances := !instances @ [x]
+    else raise (FoundUnif x)),
+  (fun () -> !instances) in
+let rec uniquize = function
+  | [] -> []
+  | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs ->
+    let t = Reductionops.nf_evar sigma t in
+    let f = Reductionops.nf_evar sigma f in
+    let a = Array.map (Reductionops.nf_evar sigma) a in
+    let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) =
+      let t1 = Reductionops.nf_evar sigma1 t1 in
+      let f1 = Reductionops.nf_evar sigma1 f1 in
+      let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in
+      not (Term.eq_constr t t1 &&
+           Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in
+    x :: uniquize (List.filter neq xs) in
+
 ((fun env c h ~k -> 
   do_once upat_that_matched (fun () -> 
     try
-      match_upats_FO upats env sigma0 ise c;
-      match_upats_HO upats env sigma0 ise c;
+      if not all_instances then match_upats_FO upats env sigma0 ise c;
+      match_upats_HO ~on_instance upats env sigma0 ise c;
       raise NoMatch
-    with FoundUnif sigma_u -> sigma_u
+    with FoundUnif sigma_u -> 0,[sigma_u]
+    | (NoMatch|NoProgress) when all_instances && instances () <> [] ->
+      0, uniquize (instances ())
     | NoMatch when (not raise_NoMatch) ->
       errorstrm (source () ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
@@ -742,9 +771,11 @@ let source () = match upats_origin, upats with
         errorstrm (str"all matches of "++source()++
           str"are equal to the " ++ pr_dir_side (inv_dir dir))
     | NoProgress -> raise NoMatch);
-  let sigma, _, ({up_f = pf; up_a = pa} as u) = assert_done 
upat_that_matched in
+  let sigma, _, ({up_f = pf; up_a = pa} as u) =
+    if all_instances then assert_done_multires upat_that_matched
+    else List.hd (snd(assert_done upat_that_matched)) in
   pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma));
-  if !skip_occ then (ignore(k env u.up_t 0); c) else
+  if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else
   let match_EQ = match_EQ env sigma u in
   let pn = Array.length pa in
   let rec subst_loop (env,h as acc) c' =
@@ -753,7 +784,7 @@ let source () = match upats_origin, upats with
     if Array.length a >= pn && match_EQ f && unif_EQ_args env sigma pa a then
       let a1, a2 = Array.chop (Array.length pa) a in
       let fa1 = mkApp (f, a1) in
-      let f' = if subst_occ () then k env u.up_t h else fa1 in
+      let f' = if subst_occ () then k env u.up_t fa1 h else fa1 in
       mkApp (f', Array.map_left (subst_loop acc) a2)
     else
       (* TASSI: clear letin values to avoid unfolding *)
@@ -764,7 +795,7 @@ let source () = match upats_origin, upats with
 ((fun () ->
   let sigma, uc, ({up_f = pf; up_a = pa} as u) =
     match !upat_that_matched with
-    | Some x -> x | None when raise_NoMatch -> raise NoMatch
+    | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch
     | None -> Errors.anomaly (str"companion function never called") in
   let p' = mkApp (pf, pa) in
   if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
@@ -1081,7 +1112,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 
pattern occ do_subst =
     let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma 
t) in
     sigma, [pat] in
   match pattern with
-  | None -> do_subst env0 concl0 1
+  | None -> do_subst env0 concl0 concl0 1
   | Some (sigma, (T rp | In_T rp)) -> 
     let rp = fs sigma rp in
     let ise = create_evar_defs sigma in
@@ -1100,7 +1131,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 
pattern occ do_subst =
     (* we start from sigma, so hole is considered a rigid head *)
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in
-    let concl = find_T env0 concl0 1 (fun env c h ->
+    let concl = find_T env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
       fs p_sigma (find_X env (fs sigma p) h 
@@ -1116,10 +1147,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 
pattern occ do_subst =
     let find_X, end_X = mk_tpattern_matcher sigma noindex holep in
     let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in
     let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in
-    let concl = find_T env0 concl0 1 (fun env c h ->
+    let concl = find_T env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c h ->
+      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
         find_E env e_body h do_subst))) in
     let _ = end_E () in let _ = end_X () in let _ = end_T () in
     concl
@@ -1133,13 +1164,13 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 
pattern occ do_subst =
     let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher sigma occ holep in
-    let concl = find_TE env0 concl0 1 (fun env c h ->
+    let concl = find_TE env0 concl0 1 (fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) c p in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c h ->
+      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
         let e_sigma = unify_HO env sigma e_body e in
         let e_body = fs e_sigma e in
-        do_subst env e_body h))) in
+        do_subst env e_body e_body h))) in
     let _ = end_X () in let _ = end_TE () in
     concl
 ;;
@@ -1155,7 +1186,7 @@ let redex_of_pattern ?(resolve_typeclasses=false) env 
(sigma, p) =
 
 let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
   let find_R, conclude = let r = ref None in
-    (fun env c h' -> do_once r (fun () -> c, 
Evd.empty_evar_universe_context);
+    (fun env c _ h' -> do_once r (fun () -> c, 
Evd.empty_evar_universe_context);
                      mkRel (h'+h-1)),
     (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) 
in
   let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in
@@ -1173,7 +1204,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in
  let find_U, end_U =
    mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
- let concl = find_U env concl h (fun _ _ -> mkRel) in
+ let concl = find_U env concl h (fun _ _ _ -> mkRel) in
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, p, concl, rdx
 
@@ -1228,6 +1259,27 @@ TACTIC EXTEND ssrat
 | [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic 
(ssrpatterntac ist arg) ]
 END
 
+let ssrinstancesof ist arg gl =
+  let ok rhs lhs ise = true in
+(*   not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *)
+  let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
+  let sigma0, cpat = interp_cpattern ist gl arg None in
+  let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in
+  let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in
+  let find, conclude =
+    mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true
+      sigma None (etpat,[tpat]) in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p 
++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  ppnl (str"BEGIN INSTANCES");
+  try
+    while true do
+      ignore(find env concl 1 ~k:print)
+    done; raise NoMatch
+  with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
+
+TACTIC EXTEND ssrinstoftpat
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic 
(ssrinstancesof ist arg) ]
+END
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
diff --git a/ssreflect/v8.5/src/ssrmatching.mli 
b/ssreflect/v8.5/src/ssrmatching.mli
index b355dc1..e8b4d81 100644
--- a/ssreflect/v8.5/src/ssrmatching.mli
+++ b/ssreflect/v8.5/src/ssrmatching.mli
@@ -76,9 +76,9 @@ val interp_cpattern :
  *  to signal the complement of this set (i.e. {-1 3}) *)
 type occ = (bool * int list) option
 
-(** Substitution function. The [int] argument is the number of binders
-    traversed so far *)
-type subst = env -> constr -> int -> constr
+(** [subst e p t i]. [i] is the number of binders
+    traversed so far, [p] the term from the pattern, [t] the matched one *)
+type subst = env -> constr -> constr -> int -> constr
 
 (** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on 
every
     [occ] occurrence of [pat]. The [int] argument is the number of 
@@ -119,7 +119,7 @@ val pr_dir_side : ssrdir -> Pp.std_ppcmds
 (** a pattern for a term with wildcards *)
 type tpattern
 
-(** [mk_tpattern env sigma0 sigma_t ok p_origin dir p] compiles a term [t] 
+(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] 
     living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern].
     The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok]
     callback is used to filter occurrences.
@@ -160,6 +160,7 @@ type conclude =
     be passed to tune the [UserError] eventually raised (useful if the 
     pattern is coming from the LHS/RHS of an equation) *)
 val mk_tpattern_matcher :
+  ?all_instances:bool ->
   ?raise_NoMatch:bool ->
   ?upats_origin:ssrdir * constr ->
   evar_map -> occ -> evar_map * tpattern list ->