Library Waterproof.Tactics.Unfold
Require Import Ltac2.Ltac2.
Require Import Ltac2.Std.
Require Import Ltac2.Message.
Local Ltac2 concat_list (ls : message list) : message :=
List.fold_right concat (of_string "") ls.
Require Import Util.Goals.
Require Import Util.MessagesToUser.
Local Ltac2 _is_empty (ls : 'a list) :=
match ls with
| _::_ => false
| [] => true
end.
Ltac2 Type exn ::= [ Inner ].
Attemtps to unfold definition(s) in a statement according to specified method.
If succesful it also throws a fatal error suggesting the user to replace this
command by an alternative, suitable tactic with the unfolded statement.
E.g. if the statement corresponds with the proof goal,
the user is suggested to use
'We need to show that (statement with unfolded definiton)'.
Arguments:
Raises fatal exceptions:
- unfold method: constr -> constr, method to be used for unfolding unfolding is deemed to be succesful if unfold_method statement =\= statement
- def_name: string, optional string used for error message when unfolding is unsuccesful
- statement : constr, term in which definitions are to be unfolded.
- always if throw_error = true, because it indicates that the user needs to remove this line from the proof script.
- none if throw_error = false.
Ltac2 unfold_in_statement (unfold_method: constr -> constr)
(def_name : string option) (statement : constr) (throw_error : bool) :=
let unfolded_statement := unfold_method statement in
match Constr.equal statement unfolded_statement with
| false =>
match! goal with
| [ |- ?g] =>
match Constr.equal g statement with
| false => Control.zero Inner
| true =>
let msg (unfolded : constr) := concat_list
[of_string "replace line with: We need to show that "; of_constr unfolded; of_string "."] in
print (msg unfolded_statement)
end
| [_ : ?hyp |- _ ] =>
match Constr.equal hyp statement with
| false => Control.zero Inner
| true =>
let msg (unfolded : constr) := concat_list
[of_string "replace line with: It holds that "; of_constr unfolded; of_string "."] in
print (msg unfolded_statement)
end
| [ |- _ ] =>
let msg (unfolded : constr) := concat_list
[of_string "result: "; of_constr unfolded] in
print (msg unfolded_statement)
end
| true =>
match def_name with
| None => print (concat_list
[of_string "definition does not appear in "; of_constr statement; of_string "."])
| Some def_name => print (concat_list
[of_string "'"; of_string def_name; of_string "'";
of_string " does not appear in "; of_constr statement; of_string "."])
end
end;
if throw_error
then throw (of_string "Remove this line in the final version of your proof.")
else ().
(def_name : string option) (statement : constr) (throw_error : bool) :=
let unfolded_statement := unfold_method statement in
match Constr.equal statement unfolded_statement with
| false =>
match! goal with
| [ |- ?g] =>
match Constr.equal g statement with
| false => Control.zero Inner
| true =>
let msg (unfolded : constr) := concat_list
[of_string "replace line with: We need to show that "; of_constr unfolded; of_string "."] in
print (msg unfolded_statement)
end
| [_ : ?hyp |- _ ] =>
match Constr.equal hyp statement with
| false => Control.zero Inner
| true =>
let msg (unfolded : constr) := concat_list
[of_string "replace line with: It holds that "; of_constr unfolded; of_string "."] in
print (msg unfolded_statement)
end
| [ |- _ ] =>
let msg (unfolded : constr) := concat_list
[of_string "result: "; of_constr unfolded] in
print (msg unfolded_statement)
end
| true =>
match def_name with
| None => print (concat_list
[of_string "definition does not appear in "; of_constr statement; of_string "."])
| Some def_name => print (concat_list
[of_string "'"; of_string def_name; of_string "'";
of_string " does not appear in "; of_constr statement; of_string "."])
end
end;
if throw_error
then throw (of_string "Remove this line in the final version of your proof.")
else ().
Attempts to unfold definition(s) in every statement according to specified method.
If succesful it prints a list of suitable tactics
that can be used to incorporate the unfolded statements into the user's proof script.
E.g. if the defition was unfolded in the proof goal, the list will include
'We need to show that (statement with unfolded definiton)'.
Arguments:
Raises fatal exceptions:
- unfold method: constr -> constr, method to be used for unfolding unfolding is deemed to be succesful if unfold_method statement =\= statement
- def_name: string, optional string used for error message when unfolding is unsuccesful
- throw_error : bool, whether the tactic should throw an error which suggests user to remove this tactic in final version of the proof.
- always/none depending on value of throw_error.
Ltac2 unfold_in_all (unfold_method: constr -> constr)
(def_name : string option) (throw_error : bool) :=
let goal := Control.goal () in
let unfolded_goal := unfold_method goal in
let did_unfold_goal := Bool.neg (Constr.equal unfolded_goal goal) in
let hyps := List.map (fun (i, def, t) => t) (Control.hyps ()) in
let unfolded_hyps := List.map unfold_method hyps in
let only_unfolded_hyps :=
List.map (fun (uh, h) => uh) (
List.filter_out (fun (uh, h) => Constr.equal uh h) (
List.combine unfolded_hyps hyps
)
) in
if (Bool.or did_unfold_goal (Bool.neg (_is_empty only_unfolded_hyps)))
then
print (of_string "Expanded definition in statements where applicable.");
print (of_string "To include these statements, use (one of):");
if did_unfold_goal
then
print (of_string "");
print (concat_list [of_string " We need to show that ";
of_constr unfolded_goal; of_string "."])
else ();
if (Bool.neg (_is_empty only_unfolded_hyps))
then
print (of_string "");
let it_holds_msg := fun (x : constr) => concat_list
[of_string " It holds that "; of_constr x; of_string "."] in
List.fold_left (fun _ unfolded_h => print (it_holds_msg unfolded_h))
only_unfolded_hyps ()
else ()
else
match def_name with
| None => print (of_string "Definition does not appear in any statement.")
| Some def_name => print (concat_list
[of_string "'"; of_string def_name; of_string "'";
of_string " does not appear in any statement."])
end;
if throw_error
then throw (of_string "Remove this line in the final version of your proof.")
else ().
Either attempts to unfold definition(s) in every statement according to specified method, or
attempts to unfold definition(s) in the provided statement.
If succesful it prints a list of suitable tactics
that can be used to incorporate the unfolded statements into the user's proof script.
E.g. if the defition was unfolded in the proof goal, the list will include
'We need to show that (statement with unfolded definiton)'.
Arguments:
Raises fatal exceptions:
- unfold method: constr -> constr, method to be used for unfolding unfolding is deemed to be succesful if unfold_method statement =\= statement
- def_name: string, optional string used for error message when unfolding is unsuccesful
- throw_error : bool, whether the tactic should throw an error which suggests user to remove this tactic in final version of the proof.
- x : constr option, optional statement in which definitions are to be unfolded. If None, definitions are unfolded in every statement.
- always/none depending on value of throw_error.
Ltac2 wp_unfold (unfold_method: constr -> constr)
(def_name : string option) (throw_error : bool) (x : constr option) :=
panic_if_goal_wrapped ();
match x with
| Some a => unfold_in_statement unfold_method def_name a throw_error
| None => unfold_in_all unfold_method def_name throw_error
end.
Ltac2 Notation "Expand" "the" "definition" "of" targets(list1(seq(reference, occurrences), ","))
x(opt(seq("in", constr))) :=
wp_unfold (eval_unfold targets) None true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" targets(list1(seq(reference, occurrences), ",")) x(opt(seq("in", constr))) :=
wp_unfold (eval_unfold targets) None false x.
(def_name : string option) (throw_error : bool) (x : constr option) :=
panic_if_goal_wrapped ();
match x with
| Some a => unfold_in_statement unfold_method def_name a throw_error
| None => unfold_in_all unfold_method def_name throw_error
end.
Ltac2 Notation "Expand" "the" "definition" "of" targets(list1(seq(reference, occurrences), ","))
x(opt(seq("in", constr))) :=
wp_unfold (eval_unfold targets) None true x.
Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" targets(list1(seq(reference, occurrences), ",")) x(opt(seq("in", constr))) :=
wp_unfold (eval_unfold targets) None false x.