Permalink
Browse files

induction/destruct : nicer syntax for generating equations (solves #2…

…741)

 The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:

  destruct x eqn:H
  destruct x as [ ] eqn:H

 Some with induction. Of course, the pattern behind "as" is arbitrary.
 For an anonymous version, H could be replaced by ?. The old syntax
 with "_eqn" still works for the moment, by triggers a warning.

 For making this new syntax work, we had to change the seldom-used
 "induction x y z using foo" into "induction x, y, z using foo".
 Now, only one "using" can be used per command instead of one per
 comma-separated group earlier, but I doubt this will bother anyone.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 06d096b commit f3870c96a192ff52449db9695b1c160834ff023f letouzey committed Jul 9, 2012
View
@@ -25,6 +25,9 @@ Tactics
version of "tauto".
- Similarly, "intuition" has been made more uniform and, where it now
fails, "dintuition" can be used.
+- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
+ or "induction" to make it generate equations in the spirit of "case_eq".
+ The former syntax "_eqn" is discontinued.
Program
View
@@ -1765,15 +1765,15 @@ \subsection{\tt induction \term
{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
{\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
-\item{\tt induction {\term} as {\namingintropattern}}
+\item{\tt induction {\term} eqn:{\namingintropattern}}
This behaves as {\tt induction {\term}} but adds an equation between
{\term} and the value that {\term} takes in each of the induction
case. The name of the equation is built according to
{\namingintropattern} which can be an identifier, a ``?'', etc, as
indicated in Section~\ref{intros-pattern}.
-\item{\tt induction {\term} as {\namingintropattern} {\disjconjintropattern}}
+\item{\tt induction {\term} as {\disjconjintropattern} eqn:{\namingintropattern}}
This combines the two previous forms.
@@ -1802,7 +1802,7 @@ \subsection{\tt induction \term
This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but
also providing instances for the premises of the type of {\term$_2$}.
-\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+\item \texttt{induction {\term}$_1$, $\ldots$, {\term}$_n$ using {\qualid}}
This syntax is used for the case {\qualid} denotes an induction principle
with complex predicates as the induction principles generated by
@@ -1818,14 +1818,14 @@ \subsection{\tt induction \term
When an occurrence clause is given, an equation between {\term} and
the value it gets in each case of the induction is added to the
context of the subgoals corresponding to the induction cases (even
- if no clause {\tt as {\namingintropattern}} is given).
+ if no clause {\tt eqn:{\namingintropattern}} is given).
-\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
- {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+ {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
These are the most general forms of {\tt induction} and {\tt
einduction}. It combines the effects of the {\tt with}, {\tt as},
- {\tt using}, and {\tt in} clauses.
+ {\tt eqn:}, {\tt using}, and {\tt in} clauses.
\item {\tt elim \term}\label{elim}
@@ -1946,6 +1946,10 @@ \subsection{\tt destruct \term
\end{itemize}
\begin{Variants}
+\item{\tt destruct \term$_1$, \ldots, \term$_n$}
+
+ This is a shortcut for {\tt destruct \term$_1$; \ldots; destruct \term$_n$}.
+
\item{\tt destruct {\term} as {\disjconjintropattern}}
This behaves as {\tt destruct {\term}} but uses the names in
@@ -1964,20 +1968,13 @@ \subsection{\tt destruct \term
% It is recommended to use this variant of {\tt destruct} for
% robust proof scripts.
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn}
+\item{\tt destruct {\term} eqn:{\namingintropattern}}
This behaves as {\tt destruct {\term}} but adds an equation between
{\term} and the value that {\term} takes in each of the possible
- cases. The name of the equation is chosen by Coq. If
- {\disjconjintropattern} is simply {\tt []}, it is automatically considered
- as a disjunctive pattern of the appropriate size.
-
-\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn: {\namingintropattern}}
-
- This behaves as {\tt destruct {\term} as
- {\disjconjintropattern} \_eqn} but use {\namingintropattern} to
- name the equation (see Section~\ref{intros-pattern}). Note that spaces
- can generally be removed around {\tt \_eqn}.
+ cases. The name of the equation is specified by {\namingintropattern}
+ (see Section~\ref{intros-pattern}), in particular {\tt ?} can be
+ used to let Coq generate a fresh name.
\item{\tt destruct {\term} with \bindinglist}
@@ -2011,11 +2008,11 @@ \subsection{\tt destruct \term
context of the subgoals corresponding to the cases (even
if no clause {\tt as {\namingintropattern}} is given).
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
- {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+ {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} eqn:{\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
These are the general forms of {\tt destruct} and {\tt edestruct}.
- They combine the effects of the {\tt with}, {\tt as}, {\tt using},
+ They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
and {\tt in} clauses.
\item{\tt case \term}\label{case}\tacindex{case}
View
@@ -359,13 +359,15 @@ let rec mlexpr_of_atomic_tactic = function
$mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacInductionDestruct (isrec,ev,l) ->
<:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
- $mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple
- (mlexpr_of_list mlexpr_of_induction_arg)
- (mlexpr_of_option mlexpr_of_constr_with_binding)
- (mlexpr_of_pair
- (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
- (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
- (mlexpr_of_option mlexpr_of_clause) l$ >>
+ $mlexpr_of_triple
+ (mlexpr_of_list
+ (mlexpr_of_pair
+ mlexpr_of_induction_arg
+ (mlexpr_of_pair
+ (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
+ (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
+ (mlexpr_of_option mlexpr_of_constr_with_binding)
+ (mlexpr_of_option mlexpr_of_clause) l$ >>
(* Context management *)
| Tacexpr.TacClear (b,l) ->
View
@@ -58,11 +58,14 @@ type 'id message_token =
| MsgIdent of 'id
type 'constr induction_clause =
- ('constr with_bindings induction_arg list * 'constr with_bindings option *
- (intro_pattern_expr located option * intro_pattern_expr located option))
+ 'constr with_bindings induction_arg *
+ (intro_pattern_expr located option (* eqn:... *)
+ * intro_pattern_expr located option) (* as ... *)
type ('constr,'id) induction_clause_list =
- 'constr induction_clause list * 'id clause_expr option
+ 'constr induction_clause list
+ * 'constr with_bindings option (* using ... *)
+ * 'id clause_expr option (* in ... *)
type multi =
| Precisely of int
View
@@ -134,21 +134,19 @@ let induction_arg_of_constr (c,lbind as clbind) =
else ElimOnConstr clbind
let mkTacCase with_evar = function
- | [([ElimOnConstr cl],None,(None,None))],None ->
+ | [ElimOnConstr cl,(None,None)],None,None ->
TacCase (with_evar,cl)
(* Reinterpret numbers as a notation for terms *)
- | [([(ElimOnAnonHyp n)],None,(None,None))],None ->
+ | [ElimOnAnonHyp n,(None,None)],None,None ->
TacCase (with_evar,
(CPrim (Loc.ghost, Numeral (Bigint.of_string (string_of_int n))),
NoBindings))
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
- | [([ElimOnIdent id],None,(None,None))],None ->
+ | [ElimOnIdent id,(None,None)],None,None ->
TacCase (with_evar,(CRef (Ident id),NoBindings))
| ic ->
- if List.exists (fun (cl,a,b) ->
- List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl)
- (fst ic)
+ if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic)
then
error "Use of numbers as direct arguments of 'case' is not supported.";
TacInductionDestruct (false,with_evar,ic)
@@ -283,11 +281,6 @@ GEXTEND Gram
| "*" -> loc, IntroForthcoming true
| "**" -> loc, IntroForthcoming false ] ]
;
- intropattern_modifier:
- [ [ IDENT "_eqn";
- id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
- -> id ] ]
- ;
simple_intropattern:
[ [ pat = disjunctive_intropattern -> pat
| pat = naming_intropattern -> pat
@@ -459,10 +452,12 @@ GEXTEND Gram
[ [ "as"; ipat = simple_intropattern -> Some ipat
| -> None ] ]
;
- with_induction_names:
- [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier
- -> (eq,Some ipat)
- | -> (None,None) ] ]
+ eqn_ipat:
+ [ [ IDENT "eqn"; ":"; id = naming_intropattern -> Some id
+ | IDENT "_eqn"; ":"; id = naming_intropattern ->
+ let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn\"" in
+ msg_warning (strbrk msg); Some id
+ | -> None ] ]
;
as_name:
[ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
@@ -491,14 +486,11 @@ GEXTEND Gram
[ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ]
;
induction_clause:
- [ [ lc = LIST1 induction_arg; ipats = with_induction_names;
- el = OPT eliminator -> (lc,el,ipats) ] ]
- ;
- one_induction_clause:
- [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ]
+ [ [ c = induction_arg; pat = as_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ]
;
induction_clause_list:
- [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ]
+ [ [ ic = LIST1 induction_clause SEP ",";
+ el = OPT eliminator; cl = opt_clause -> (ic,el,cl) ] ]
;
move_location:
[ [ IDENT "after"; id = id_or_meta -> MoveAfter id
@@ -592,9 +584,9 @@ GEXTEND Gram
(* Derived basic tactics *)
| IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
TacSimpleInductionDestruct (true,h)
- | IDENT "induction"; ic = one_induction_clause ->
+ | IDENT "induction"; ic = induction_clause_list ->
TacInductionDestruct (true,false,ic)
- | IDENT "einduction"; ic = one_induction_clause ->
+ | IDENT "einduction"; ic = induction_clause_list ->
TacInductionDestruct(true,true,ic)
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
View
@@ -338,11 +338,15 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
let pr_with_bindings prlc prc (c,bl) =
hov 1 (prc c ++ pr_bindings prlc prc bl)
+let pr_as_ipat pat = str "as " ++ pr_intro_pattern pat
+let pr_eqn_ipat pat = str "eqn:" ++ pr_intro_pattern pat
+
let pr_with_induction_names = function
| None, None -> mt ()
- | eqpat, ipat ->
- spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++
- pr_opt pr_intro_pattern ipat)
+ | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
+ | None, Some ipat -> spc () ++ hov 1 (pr_as_ipat ipat)
+ | Some eqpat, Some ipat ->
+ spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
let pr_as_intro_pattern ipat =
spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
@@ -714,14 +718,14 @@ and pr_atom1 = function
| TacSimpleInductionDestruct (isrec,h) ->
hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
++ pr_arg pr_quantified_hypothesis h)
- | TacInductionDestruct (isrec,ev,(l,cl)) ->
+ | TacInductionDestruct (isrec,ev,(l,el,cl)) ->
hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
spc () ++
- prlist_with_sep pr_comma (fun (h,e,ids) ->
- prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
- pr_with_induction_names ids ++
- pr_opt pr_eliminator e) l ++
- pr_opt_no_spc (pr_clauses None pr_ident) cl)
+ prlist_with_sep pr_comma (fun (h,ids) ->
+ pr_induction_arg pr_lconstr pr_constr h ++
+ pr_with_induction_names ids) l ++
+ pr_opt pr_eliminator el ++
+ pr_opt_no_spc (pr_clauses None pr_ident) cl)
| TacDoubleInduction (h1,h2) ->
hov 1
(str "double induction" ++
View
@@ -84,12 +84,12 @@ let out_indarg = function
| ElimOnAnonHyp n -> ElimOnAnonHyp n
let h_induction_destruct isrec ev lcl =
- let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in
+ let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
(induction_destruct isrec ev lcl)
-let h_new_induction ev c e idl cl =
- h_induction_destruct true ev ([c,e,idl],cl)
-let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl)
+let h_new_induction ev c idl e cl =
+ h_induction_destruct true ev ([c,idl],e,cl)
+let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
View
@@ -68,19 +68,19 @@ val h_simple_induction : quantified_hypothesis -> tactic
val h_simple_destruct : quantified_hypothesis -> tactic
val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
val h_new_induction : evars_flag ->
- (evar_map * constr with_bindings) induction_arg list ->
- constr with_bindings option ->
+ (evar_map * constr with_bindings) induction_arg ->
intro_pattern_expr located option * intro_pattern_expr located option ->
+ constr with_bindings option ->
Locus.clause option -> tactic
val h_new_destruct : evars_flag ->
- (evar_map * constr with_bindings) induction_arg list ->
- constr with_bindings option ->
+ (evar_map * constr with_bindings) induction_arg ->
intro_pattern_expr located option * intro_pattern_expr located option ->
+ constr with_bindings option ->
Locus.clause option -> tactic
val h_induction_destruct : rec_flag -> evars_flag ->
- ((evar_map * constr with_bindings) induction_arg list *
- constr with_bindings option *
+ ((evar_map * constr with_bindings) induction_arg *
(intro_pattern_expr located option * intro_pattern_expr located option)) list
+ * constr with_bindings option
* Locus.clause option -> tactic
val h_specialize : int option -> constr with_bindings -> tactic
View
@@ -732,12 +732,12 @@ let rec intern_atomic lf ist x =
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
- | TacInductionDestruct (ev,isrec,(l,cls)) ->
- TacInductionDestruct (ev,isrec,(List.map (fun (lc,cbo,(ipato,ipats)) ->
- (List.map (intern_induction_arg ist) lc,
- Option.map (intern_constr_with_bindings ist) cbo,
+ | TacInductionDestruct (ev,isrec,(l,el,cls)) ->
+ TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) ->
+ (intern_induction_arg ist c,
(Option.map (intern_intro_pattern lf ist) ipato,
Option.map (intern_intro_pattern lf ist) ipats))) l,
+ Option.map (intern_constr_with_bindings ist) el,
Option.map (clause_app (intern_hyp_location ist)) cls))
| TacDoubleInduction (h1,h2) ->
let h1 = intern_quantified_hypothesis ist h1 in
@@ -2424,17 +2424,17 @@ and interp_atomic ist gl tac =
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
- | TacInductionDestruct (isrec,ev,(l,cls)) ->
+ | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
let sigma, l =
- list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) ->
- let lc = List.map (interp_induction_arg ist gl) lc in
- let sigma,cbo =
- Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
- (sigma,(lc,cbo,
+ list_fold_map (fun sigma (c,(ipato,ipats)) ->
+ let c = interp_induction_arg ist gl c in
+ (sigma,(c,
(Option.map (interp_intro_pattern ist gl) ipato,
Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in
+ let sigma,el =
+ Option.fold_map (interp_constr_with_bindings ist env) sigma el in
let cls = Option.map (interp_clause ist gl) cls in
- tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls)
+ tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
@@ -2862,10 +2862,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) as x -> x
- | TacInductionDestruct (isrec,ev,(l,cls)) ->
- TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) ->
- List.map (subst_induction_arg subst) lc,
- Option.map (subst_glob_with_bindings subst) cbo, ids) l, cls))
+ | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
+ let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in
+ let el' = Option.map (subst_glob_with_bindings subst) el in
+ TacInductionDestruct (isrec,ev,(l',el',cls))
| TacDoubleInduction (h1,h2) as x -> x
| TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c)
| TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c)
View
@@ -3207,12 +3207,19 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
end
let induction_destruct isrec with_evars = function
- | [],_ -> tclIDTAC
- | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl)
- | (a,b,c)::l,cl ->
+ | [],_,_ -> tclIDTAC
+ | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl)
+ | (a,b)::l,None,cl ->
tclTHEN
- (induct_destruct isrec with_evars (a,b,c,cl))
- (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l)
+ (induct_destruct isrec with_evars ([a],None,b,cl))
+ (tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l)
+ | l,Some el,cl ->
+ let check_basic_using = function
+ | a,(None,None) -> a
+ | _ -> error "Unsupported syntax for \"using\"."
+ in
+ let l' = List.map check_basic_using l in
+ induct_destruct isrec with_evars (l', Some el, (None,None), cl)
let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls)
let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
Oops, something went wrong.

0 comments on commit f3870c9

Please sign in to comment.