Library Waterproof.Tactics.Take
Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Local Ltac2 concat_list (ls : message list) : message :=
List.fold_right concat (of_string "") ls.
Require Import Util.Binders.
Require Import Util.Constr.
Require Import Util.Goals.
Require Import Util.Hypothesis.
Require Import Util.MessagesToUser.
Local Ltac2 too_many_of_type_message (t : constr) :=
concat_list [of_string "Tried to introduce too many variables of type ";
of_constr t; of_string "."].
Local Ltac2 expected_of_type_instead_of_message (e : constr) (t : constr) :=
concat_list [of_string "Expected variable of type "; of_constr e;
of_string " instead of "; of_constr t; of_string "."].
Introduces a variable.
Arguments:
- id : ident : variable to introduce.
- type: constr: type of the variable id.
- Introduces the variable id.
- If the current goal does not require the introduction of a variable of type type, including coercions of type.
Local Ltac2 intro_ident (id : ident) (type : constr) :=
let current_goal := Control.goal () in
match Constr.Unsafe.kind current_goal with
| Constr.Unsafe.Prod b a =>
let ct := get_coerced_type type in
match check_constr_equal (Constr.Binder.type b) ct with
| true => ()
| false => throw (too_many_of_type_message type)
end;
check_binder_name current_goal id;
intro $id
| _ => throw (too_many_of_type_message type)
end.
let current_goal := Control.goal () in
match Constr.Unsafe.kind current_goal with
| Constr.Unsafe.Prod b a =>
let ct := get_coerced_type type in
match check_constr_equal (Constr.Binder.type b) ct with
| true => ()
| false => throw (too_many_of_type_message type)
end;
check_binder_name current_goal id;
intro $id
| _ => throw (too_many_of_type_message type)
end.
Introduces a list of variables of single type.
Arguments:
Does:
Raises fatal exceptions:
- pair : (ident list * constr): list of variables paired with their type.
- Introduces the variables in pair.
- If the current goal does not require the introduction of a variable of type type, including coercions of type.
Local Ltac2 intro_per_type (pair : ident list * constr) :=
let (ids, type) := pair in
lazy_match! goal with
| [ |- forall _ : ?u, _] =>
let sort_u := get_value_of_hyp u in
match check_constr_equal sort_u constr:(Prop) with
| false =>
let ct := get_coerced_type type in
match check_constr_equal u ct with
| true => List.iter (fun id => intro_ident id type) ids
| false => throw (expected_of_type_instead_of_message u type)
end
| true => throw (of_string "Tried to introduce too many variables.")
end
| [ |- _ ] => throw (of_string "Tried to introduce too many variables.")
end.
let (ids, type) := pair in
lazy_match! goal with
| [ |- forall _ : ?u, _] =>
let sort_u := get_value_of_hyp u in
match check_constr_equal sort_u constr:(Prop) with
| false =>
let ct := get_coerced_type type in
match check_constr_equal u ct with
| true => List.iter (fun id => intro_ident id type) ids
| false => throw (expected_of_type_instead_of_message u type)
end
| true => throw (of_string "Tried to introduce too many variables.")
end
| [ |- _ ] => throw (of_string "Tried to introduce too many variables.")
end.
Checks whether variables need to be introduced, attempts to introduce a list of variables of certain types.
Local Ltac2 take (x : (ident list * constr) list) :=
lazy_match! goal with
| [ |- forall _ : ?u, _] =>
let sort_u := get_value_of_hyp u in
match check_constr_equal sort_u constr:(Prop) with
| false => List.iter intro_per_type x
| true => throw (of_string "`Take ...` cannot be used to prove an implication (⇨). Use `Assume that ...` instead.")
end
| [ |- _ ] => throw (of_string "`Take ...` can only be used to prove a `for all`-statement (∀) or to construct a map (→).")
end.
Ltac2 Notation "Take" x(list1(seq(list1(ident, ","), ":", constr), "and")) :=
panic_if_goal_wrapped ();
take x.
lazy_match! goal with
| [ |- forall _ : ?u, _] =>
let sort_u := get_value_of_hyp u in
match check_constr_equal sort_u constr:(Prop) with
| false => List.iter intro_per_type x
| true => throw (of_string "`Take ...` cannot be used to prove an implication (⇨). Use `Assume that ...` instead.")
end
| [ |- _ ] => throw (of_string "`Take ...` can only be used to prove a `for all`-statement (∀) or to construct a map (→).")
end.
Ltac2 Notation "Take" x(list1(seq(list1(ident, ","), ":", constr), "and")) :=
panic_if_goal_wrapped ();
take x.