Skip to content

Trunk+abstracting injection flags #677

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot merged 2 commits into from
Oct 27, 2017
Merged

Trunk+abstracting injection flags #677

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
925c434
Delay use of flag "Discriminate Introduction" from interp to executio…
herbelin Dec 24, 2016
91e9e1c
Passing around the flag for injection so that tactics calling inj at
herbelin Dec 22, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 11 additions & 6 deletions API/API.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5337,6 +5337,11 @@ sig
| Naive
| FirstSolved
| AllMatches
type inj_flags = {
keep_proof_equalities : bool; (* One may want it or not *)
injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *)
injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
}

val build_selector :
Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
Expand All @@ -5345,20 +5350,20 @@ sig
val general_rewrite :
orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
val general_multi_rewrite :
Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list ->
Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
val discr_tac : Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
val injClause : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic

val simpleInjClause : Misctypes.evars_flag ->
val simpleInjClause : inj_flags option -> Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option ->
unit Proofview.tactic
val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
Expand Down Expand Up @@ -5392,8 +5397,8 @@ sig
?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val discrHyp : Names.Id.t -> unit Proofview.tactic
val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool
val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
end

Expand Down
2 changes: 2 additions & 0 deletions CHANGES
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ Tactics
such as "x := 5 : Z" (see BZ#148). This could be disabled via
Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
- Tactic "decide equality" now able to manage constructors which
contain proofs.

Changes from 8.7+beta2 to 8.7.0
===============================
Expand Down
6 changes: 6 additions & 0 deletions dev/doc/changes.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,12 @@ We renamed the following datatypes:

- `Pp.std_ppcmds` -> `Pp.t`

Some tactics and related functions now support static configurability, e.g.:

- injectable, dEq, etc. takes an argument ~keep_proofs which,
- if None, tells to behave as told with the flag Keep Proof Equalities
- if Some b, tells to keep proof equalities iff b is true

## Changes between Coq 8.6 and Coq 8.7

### Ocaml
Expand Down
9 changes: 7 additions & 2 deletions plugins/funind/invfun.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -570,6 +570,11 @@ let rec reflexivity_with_destruct_cases g =
with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
let eq_ind = make_eq () in
let my_inj_flags = Some {
Equality.keep_proof_equalities = false;
injection_in_context = false; (* for compatibility, necessary *)
injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *)
} in
let discr_inject =
Tacticals.onAllHypsAndConcl (
fun sc g ->
Expand All @@ -580,8 +585,8 @@ let rec reflexivity_with_destruct_cases g =
| App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
else if Equality.injectable (pf_env g) (project g) t1 t2
then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
Expand Down
30 changes: 15 additions & 15 deletions plugins/ltac/extratactics.ml4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c =
(fun c -> tac with_evars (Some (None,ElimOnConstr c)))

TACTIC EXTEND simplify_eq
[ "simplify_eq" ] -> [ dEq false None ]
| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ]
[ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
END
TACTIC EXTEND esimplify_eq
| [ "esimplify_eq" ] -> [ dEq true None ]
| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
END

let discr_main c = elimOnConstrWithHoles discr_tac false c
Expand All @@ -117,31 +117,31 @@ let discrHyp id =
discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))

let injection_main with_evars c =
elimOnConstrWithHoles (injClause None) with_evars c
elimOnConstrWithHoles (injClause None None) with_evars c

TACTIC EXTEND injection
| [ "injection" ] -> [ injClause None false None ]
| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
| [ "injection" ] -> [ injClause None None false None ]
| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
END
TACTIC EXTEND einjection
| [ "einjection" ] -> [ injClause None true None ]
| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
| [ "einjection" ] -> [ injClause None None true None ]
| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
END
TACTIC EXTEND injection_as
| [ "injection" "as" intropattern_list(ipat)] ->
[ injClause (Some ipat) false None ]
[ injClause None (Some ipat) false None ]
| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
[ mytclWithHoles (injClause (Some ipat)) false c ]
[ mytclWithHoles (injClause None (Some ipat)) false c ]
END
TACTIC EXTEND einjection_as
| [ "einjection" "as" intropattern_list(ipat)] ->
[ injClause (Some ipat) true None ]
[ injClause None (Some ipat) true None ]
| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
[ mytclWithHoles (injClause (Some ipat)) true c ]
[ mytclWithHoles (injClause None (Some ipat)) true c ]
END
TACTIC EXTEND simple_injection
| [ "simple" "injection" ] -> [ simpleInjClause false None ]
| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
END

let injHyp id =
Expand Down
2 changes: 1 addition & 1 deletion plugins/ssr/ssrelim.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -396,7 +396,7 @@ let revtoptac n0 gl =

let equality_inj l b id c gl =
let msg = ref "" in
try Proofview.V82.of_tactic (Equality.inj l b None c) gl
try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
| Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)
Expand Down
8 changes: 7 additions & 1 deletion tactics/eqdecide.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) =
clear_last;
intros]

let inj_flags = Some {
Equality.keep_proof_equalities = true; (* necessary *)
Equality.injection_in_context = true; (* does not matter here *)
Equality.injection_pattern_l2r_order = true; (* does not matter here *)
}

let discrHyp id =
let c env sigma = (sigma, (mkVar id, NoBindings)) in
let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
Expand Down Expand Up @@ -136,7 +142,7 @@ let eqCase tac =

let injHyp id =
let c env sigma = (sigma, (mkVar id, NoBindings)) in
let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in
Tacticals.New.tclDELAYEDWITHHOLES false c tac

let diseqCase hyps eqonleft =
Expand Down
98 changes: 56 additions & 42 deletions tactics/equality.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,12 @@ module NamedDecl = Context.Named.Declaration

(* Options *)

type inj_flags = {
keep_proof_equalities : bool;
injection_in_context : bool;
injection_pattern_l2r_order : bool;
}

let discriminate_introduction = ref true

let discr_do_intro () = !discriminate_introduction
Expand All @@ -63,7 +69,9 @@ let _ =

let injection_pattern_l2r_order = ref true

let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
let use_injection_pattern_l2r_order = function
| None -> !injection_pattern_l2r_order
| Some flags -> flags.injection_pattern_l2r_order

let _ =
declare_bool_option
Expand All @@ -75,9 +83,9 @@ let _ =

let injection_in_context = ref false

let use_injection_in_context () =
!injection_in_context
&& Flags.version_strictly_greater Flags.V8_5
let use_injection_in_context = function
| None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5

@maximedenes maximedenes Jul 26, 2017

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is this option and why do flags have priority over it? I'm not saying anything is wrong, just trying to understand.

@herbelin herbelin Jul 26, 2017

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The Boolean injection_in_context is the dynamic value of the Structural Injection option.

The flags is the static configuration, defaulting to the dynamic configuration when None. If Some, the static configuration takes priority. See discussion at ceps #29.

| Some flags -> flags.injection_in_context

let _ =
declare_bool_option
Expand Down Expand Up @@ -721,7 +729,14 @@ let _ =
optread = (fun () -> !keep_proof_equalities_for_injection) ;
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }

let find_positions env sigma ~no_discr t1 t2 =
let keep_proof_equalities = function
| None -> !keep_proof_equalities_for_injection
| Some flags -> flags.keep_proof_equalities

(* [keep_proofs] is relevant for types in Prop with elimination in Type *)
(* In particular, it is relevant for injection but not for discriminate *)

let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
let s = get_sort_family_of env sigma ty1 in
Expand Down Expand Up @@ -768,20 +783,22 @@ let find_positions env sigma ~no_discr t1 t2 =
project env sorts posn t1_0 t2_0
in
try
let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
else [InSet;InType]
in
let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in
Inr (findrec sorts [] t1 t2)
with DiscrFound (path,c1,c2) ->
Inl (path,c1,c2)

let use_keep_proofs = function
| None -> !keep_proof_equalities_for_injection
| Some b -> b

let discriminable env sigma t1 t2 =
match find_positions env sigma ~no_discr:false t1 t2 with
match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inl _ -> true
| _ -> false

let injectable env sigma t1 t2 =
match find_positions env sigma ~no_discr:true t1 t2 with
let injectable env sigma ~keep_proofs t1 t2 =
match find_positions env sigma ~keep_proofs:(use_keep_proofs keep_proofs) ~no_discr:true t1 t2 with
| Inl _ -> assert false
| Inr [] | Inr [([],_,_)] -> false
| Inr _ -> true
Expand Down Expand Up @@ -1024,7 +1041,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
match find_positions env sigma ~no_discr:false t1 t2 with
match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inr _ ->
tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
Expand Down Expand Up @@ -1069,19 +1086,16 @@ let discr with_evars = onEquality with_evars discrEq
let discrClause with_evars = onClause (discrSimpleClause with_evars)

let discrEverywhere with_evars =
(*
tclORELSE
*)
tclTHEN (Proofview.tclUNIT ())
(* Delay the interpretation of side-effect *)
(if discr_do_intro () then
(tclTHEN
(tclREPEAT introf)
(tryAllHyps
(fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
else (* <= 8.2 compat *)
tryAllHypsAndConcl (discrSimpleClause with_evars))
(* (fun gls ->
user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities."))
*)

let discr_tac with_evars = function
| None -> discrEverywhere with_evars
| Some c -> onInductionArg (fun clear_flag -> discr with_evars) c
Expand Down Expand Up @@ -1403,15 +1417,15 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))

let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
match find_positions env sigma ~no_discr:true t1 t2 with
match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with
| Inl _ ->
assert false
| Inr [] ->
let suggestion =
if !keep_proof_equalities_for_injection then
if keep_proofs then
"" else
" You can try to use option Set Keep Proof Equalities." in
tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
Expand All @@ -1430,13 +1444,13 @@ let get_previous_hyp_position id gl =
in
aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))

let injEq ?(old=false) with_evars clear_flag ipats =
let injEq flags ?(old=false) with_evars clear_flag ipats =
(* Decide which compatibility mode to use *)
let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with
| None when not old && use_injection_in_context () ->
| None when not old && use_injection_in_context flags ->
Some [], true, true, true
| None -> None, false, false, false
| _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in
| _ -> let b = use_injection_pattern_l2r_order flags in ipats, b, b, b in
(* Built the post tactic depending on compatibility mode *)
let post_tac c n =
match ipats_style with
Expand All @@ -1456,26 +1470,26 @@ let injEq ?(old=false) with_evars clear_flag ipats =
tclTHEN clear_tac intro_tac
end
| None -> tclIDTAC in
injEqThen post_tac l2r
injEqThen (keep_proof_equalities flags) post_tac l2r

let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
let inj flags ipats with_evars clear_flag = onEquality with_evars (injEq flags with_evars clear_flag ipats)

let injClause ipats with_evars = function
| None -> onNegatedEquality with_evars (injEq with_evars None ipats)
| Some c -> onInductionArg (inj ipats with_evars) c
let injClause flags ipats with_evars = function
| None -> onNegatedEquality with_evars (injEq flags with_evars None ipats)
| Some c -> onInductionArg (inj flags ipats with_evars) c

let simpleInjClause with_evars = function
| None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None)
| Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
let simpleInjClause flags with_evars = function
| None -> onNegatedEquality with_evars (injEq flags ~old:true with_evars None None)
| Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c

let injConcl = injClause None false None
let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
let injConcl flags = injClause flags None false None
let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))

let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter begin fun gl ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
match find_positions env sigma ~no_discr:false t1 t2 with
match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
Expand All @@ -1485,18 +1499,18 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
(ntac (clenv_value clause))
end

let dEqThen with_evars ntac = function
| None -> onNegatedEquality with_evars (decompEqThen (ntac None))
| Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c
let dEqThen ~keep_proofs with_evars ntac = function
| None -> onNegatedEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac None))
| Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac clear_flag))) c

let dEq with_evars =
dEqThen with_evars (fun clear_flag c x ->
let dEq ~keep_proofs with_evars =
dEqThen ~keep_proofs with_evars (fun clear_flag c x ->
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))

let intro_decomp_eq tac data (c, t) =
Proofview.Goal.enter begin fun gl ->
let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
decompEqThen (fun _ -> tac) data cl
decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl
end

let _ = declare_intro_decomp_eq intro_decomp_eq
Expand Down
Loading