Library Waterproof.Tactics.Choose
Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Require Import Util.Binders.
Require Import Util.Goals.
Require Import Util.MessagesToUser.
Require Import Util.Evars.
Local Ltac2 concat_list (ls : message list) : message :=
List.fold_right concat (of_string "") ls.
Local Ltac2 _binder_name_equal (name : ident) (b : binder) :=
match Constr.Binder.name b with
| None => false
| Some binder_name => Ident.equal name binder_name
end.
Choose
- s: ident, an ident for naming an idefined constr/variable.
- t: constr, the requirted constr that needs to be instantiated.
- instantiates the constr t under the name s.
- If the goal is not an exists goal.
Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
lazy_match! goal with
| [ |- ex ?a] =>
check_binder_name a s;
set ($s := $t);
let v := Control.hyp s in
let w := Fresh.fresh (Fresh.Free.of_goal ()) @_defeq in
match Constr.has_evar t with
| true =>
rename_blank_evars_in_term (Ident.to_string s) t;
warn (concat_list [of_string "Please come back later to make a definitive choice for "; of_ident s; of_string "."; fnl ();
of_string "For now you can use that "; of_constr constr:($v = $t); of_string "."])
| _ => ()
end;
exists $v;
assert ($w : $v = $t) by reflexivity
| [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
end.
lazy_match! goal with
| [ |- ex ?a] =>
check_binder_name a s;
set ($s := $t);
let v := Control.hyp s in
let w := Fresh.fresh (Fresh.Free.of_goal ()) @_defeq in
match Constr.has_evar t with
| true =>
rename_blank_evars_in_term (Ident.to_string s) t;
warn (concat_list [of_string "Please come back later to make a definitive choice for "; of_ident s; of_string "."; fnl ();
of_string "For now you can use that "; of_constr constr:($v = $t); of_string "."])
| _ => ()
end;
exists $v;
assert ($w : $v = $t) by reflexivity
| [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
end.
Instantiate a variable in an exists goal, according to a given constr, without renaming said constr. The constr can contain blanks, which are filled in
with freshly named evars, so that the user can refer to them later.
Arguments:
Does:
Raises fatal exceptions:
- t: constr, the requirted constr that needs to be instantiated.
- instantiates the constr t under the same name.
- If the goal is not an exists goal.
Ltac2 choose_variable_in_exists_no_renaming (t:constr) :=
lazy_match! goal with
| [ |- ex ?a] =>
let name :=
match Constr.Unsafe.kind a with
| Constr.Unsafe.Lambda b _ =>
match Constr.Binder.name b with
| Some x => Ident.to_string x
| None => "x"
end
| _ => "x"
end
in
match Constr.has_evar t with
| true =>
rename_blank_evars_in_term name t;
warn (concat_list [of_string "Please come back later to make a definite choice."]);
eexists $t
| false => exists $t
end
| [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
end.
Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(open_constr) :=
panic_if_goal_wrapped ();
match s with
| None => choose_variable_in_exists_no_renaming t
| Some s => choose_variable_in_exists_goal_with_renaming s t
end.
lazy_match! goal with
| [ |- ex ?a] =>
let name :=
match Constr.Unsafe.kind a with
| Constr.Unsafe.Lambda b _ =>
match Constr.Binder.name b with
| Some x => Ident.to_string x
| None => "x"
end
| _ => "x"
end
in
match Constr.has_evar t with
| true =>
rename_blank_evars_in_term name t;
warn (concat_list [of_string "Please come back later to make a definite choice."]);
eexists $t
| false => exists $t
end
| [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
end.
Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(open_constr) :=
panic_if_goal_wrapped ();
match s with
| None => choose_variable_in_exists_no_renaming t
| Some s => choose_variable_in_exists_goal_with_renaming s t
end.