Library Waterproof.Tactics.Help
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.Constr.
Require Import Util.Goals.
Require Import Util.Hypothesis.
Require Import Util.MessagesToUser.
Require Import Notations.Sets.
Require Import Waterprove.
Open Scope subset_scope.
Local Ltac2 goal_impl_msg (premise: constr) :=
info_notice (concat_list [of_string "The goal is to show an implication (⇒). Assume the premise "; of_constr premise; of_string "."]);
replace_msg "Assume that ...." "Assume that ${0:0 = 0}.${1}".
Local Ltac2 goal_func_msg (var_type: constr) :=
info_notice (concat_list [of_string "The goal is to construct a map (⇒). Introduce an arbitrary variable of type "; of_constr var_type; of_string "."]);
replace_msg "Take ... : ...." "Take ${0:x} : ${1:X}.${2}".
Local Ltac2 goal_forall_msg (var_type: constr) :=
info_notice (concat_list [of_string "The goal is to show a ‘for all’-statement (∀). Introduce an arbitrary variable of type "; of_constr var_type; of_string "."]);
replace_msg "Take ... : ...." "Take ${0:x} : ${1:X}.${2}".
Ltac2 goal_forall_gt_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'for all'-statement (∀). Introduce an arbitrary variable strictly larger than "; of_constr y; of_string "."]);
replace_msg "Take ... > ...." "Take ${0:x} > ${1:0}.${2}".
Local Ltac2 goal_forall_ge_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'for all'-statement (∀). Introduce an arbitrary variable larger than or equal to "; of_constr y; of_string "."]);
replace_msg "Take ... ≥ ...." "Take ${0:x} ≥ ${1:0}.${2}".
Local Ltac2 goal_forall_lt_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'for all'-statement (∀). Introduce an arbitrary variable strictly less than "; of_constr y; of_string "."]);
replace_msg "Take ... < ...." "Take ${0:x} < ${1:0}.${2}".
Local Ltac2 goal_forall_le_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'for all'-statement (∀). Introduce an arbitrary variable less than or equal to "; of_constr y; of_string "."]);
replace_msg "Take ... ≤ ...." "Take ${0:x} ≤ ${1:0}.${2}".
Local Ltac2 goal_forall_ne_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a ‘for all’-statement (∀). Introduce an arbitrary variable not equal to "; of_constr y; of_string "."]);
replace_msg "Take ... ≠ ...." "Take ${0:x} ≠ ${1:0}.${2}".
Local Ltac2 goal_forall_pred_msg (q: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'for all'-statement (∀). Introduce an arbitrary variable that is (a/an) "; of_constr q; of_string "."]);
replace_msg "Take ... ...." "Take ${0:x} ${1:0 = 0}.${2}".
Local Ltac2 goal_exists_el_msg (var_type: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable in "; of_constr var_type; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_exists_gt_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable strictly larger than "; of_constr y; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_exists_ge_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable larger than or equal to "; of_constr y; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_exists_lt_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable strictly less than "; of_constr y; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_exists_le_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable less than or equal to "; of_constr y; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_exists_ne_msg (y: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable not equal to "; of_constr y; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_exists_pred_msg (q: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable that is (a/an) "; of_constr q; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_and_msg () :=
info_notice (of_string "The goal is to show a conjunction (∧). Show both statements.");
replace_msg "We show both statements." "We show both statements.${0}".
Local Ltac2 goal_or_msg () :=
info_notice (of_string "The goal is to show a disjunction (∨). It suffices to show one of the statements.");
replace_msg "It suffices to show that ...." "It suffices to show that ${0:0 = 0}.${1}".
Local Ltac2 goal_neg_msg (negated_type : constr) :=
info_notice (concat_list [of_string "The goal is to show a negation (¬). Assume that the negated expression "; of_constr negated_type; of_string "."]);
replace_msg "Assume that ...." "Assume that ${0:0 = 0}.${1}".
Local Ltac2 goal_directly () :=
info_notice (of_string "The goal can be shown immediately.");
replace_msg "We conclude that ...." "We conclude that ${0:0 = 0}.${1}".
Local Ltac2 goal_no_hint () :=
info_notice (of_string "No direct hint available. Does the goal contain a definition that can be expanded?").
Local Ltac2 goal_exists_msg (var_type: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'there exists'-statement (∃). Choose a specific variable of type "; of_constr var_type; of_string "."]);
replace_msg "Choose ... := ...." "Choose ${0:x} := ${1:0}.${2}".
Local Ltac2 goal_forall_el_msg (var_type: constr) :=
info_notice (concat_list [of_string "The goal is to show a 'for all'-statement (∀). Introduce an arbitrary variable in "; of_constr var_type; of_string "."]);
replace_msg "Take ... ∈ ...." "Take ${0:x} ∈ ${1:X}.${2}".
Auxilliary tactic that checks if goal can be shown with automation
Local Ltac2 solvable_by_core_auto () :=
let temp_id := Fresh.in_goal @temp in
let goal := Control.goal () in
assert $goal as $temp_id;
Control.focus 1 1 (fun () => waterprove 5 true Main);
clear $temp_id.
Local Ltac2 need_to_follow_advice () : bool :=
let gl := Control.goal () in
lazy_match! gl with
| Case.Wrapper _ _ => true
| NaturalInduction.Base.Wrapper _ => true
| NaturalInduction.Step.Wrapper _ => true
| StateGoal.Wrapper _ => true
| StateHyp.Wrapper _ _ _ => true
| ByContradiction.Wrapper _ _ => true
| False => true
| _ => false
end.
Local Ltac2 goal_hint () : bool :=
let gl := Control.goal () in
lazy_match! gl with
| ?a -> ?b =>
let sort_a := get_value_of_hyp a in
match check_constr_equal sort_a constr:(Prop) with
| true => goal_impl_msg a; true
| false => goal_func_msg a; true
end
| ∀ _ ∈ conv ?v_type, _ => goal_forall_el_msg v_type; true
| ∀ _ ∈ ?v_type, _ => goal_forall_el_msg v_type; true
| ∀ _ > ?y, _ => goal_forall_gt_msg y; true
| ∀ _ ≥ ?y, _ => goal_forall_ge_msg y; true
| ∀ _ < ?y, _ => goal_forall_lt_msg y; true
| ∀ _ ≤ ?y, _ => goal_forall_le_msg y; true
| ∀ _ ?q, _ => goal_forall_pred_msg q; true
| ∃ _ ∈ conv ?v_type, _ => goal_exists_el_msg v_type; true
| ∃ _ ∈ ?v_type, _ => goal_exists_el_msg v_type; true
| ∃ _ > ?y, _ => goal_exists_gt_msg y; true
| ∃ _ ≥ ?y, _ => goal_exists_ge_msg y; true
| ∃ _ < ?y, _ => goal_exists_lt_msg y; true
| ∃ _ ≤ ?y, _ => goal_exists_le_msg y; true
| ∃ _ ≠ ?y, _ => goal_exists_ne_msg y; true
| ∃ _ ?q, _ => goal_exists_pred_msg q; true
| forall v:?v_type, _ => goal_forall_msg v_type; true
| exists v:?v_type, _ => goal_exists_msg v_type; true
| _ /\ _ => goal_and_msg (); true
| _ \/ _ => goal_or_msg (); true
| not ?g => goal_neg_msg g; true
| _ => false
end.
Local Ltac2 forall_filter (x : constr) : bool :=
lazy_match! x with
| ?a -> ?b => false
| ∀ _ _ _, _ => true
| ∀ _ _, _ => true
| forall _, _ => true
| _ => false
end.
Local Ltac2 exists_filter (x : constr) : bool :=
lazy_match! x with
| exists _, _ => true
| ∃ _ _ _, _ => true
| ∃ _ _, _ => true
| _ => false
end.
Local Ltac2 is_empty (ls : 'a list) :=
match ls with
| _::_ => false
| [] => true
end.
Ltac2 print_hints () :=
if (goal_wrapped_template_msg ())
then (info_notice (of_string "Follow the advice in the goal window."))
else
match Control.case (solvable_by_core_auto) with
| Val _ => goal_directly ()
| Err exn =>
let hint_given := goal_hint () in
let hyps := List.map (fun (i, x, t) => t) (Control.hyps ()) in
let forall_hyps := List.filter (forall_filter) hyps in
let exists_hyps := List.filter (exists_filter) hyps in
if (is_empty forall_hyps)
then ()
else (
info_notice(of_string "You can use one of the ‘for all’-statements (∀):");
List.fold_left (fun _ h => info_notice (concat (of_string " ") (of_constr h))) forall_hyps ();
replace_msg "Use ... := ... in ...." "Use ${0:x} := ${1:0} in ({2:i}).${3}"
);
if (is_empty exists_hyps)
then ()
else (
info_notice(of_string "You can use one of the ‘there exists’-statements (∃):");
List.fold_left (fun _ h => info_notice (concat (of_string " ") (of_constr h))) exists_hyps ();
replace_msg "Obtain ... according to ...." "Obtain ${0:x} according to (${1:i}).${2}"
);
if (Bool.and (is_empty forall_hyps)
(Bool.and (is_empty exists_hyps) (Bool.neg hint_given)))
then (goal_no_hint ())
else ()
end.
let temp_id := Fresh.in_goal @temp in
let goal := Control.goal () in
assert $goal as $temp_id;
Control.focus 1 1 (fun () => waterprove 5 true Main);
clear $temp_id.
Local Ltac2 need_to_follow_advice () : bool :=
let gl := Control.goal () in
lazy_match! gl with
| Case.Wrapper _ _ => true
| NaturalInduction.Base.Wrapper _ => true
| NaturalInduction.Step.Wrapper _ => true
| StateGoal.Wrapper _ => true
| StateHyp.Wrapper _ _ _ => true
| ByContradiction.Wrapper _ _ => true
| False => true
| _ => false
end.
Local Ltac2 goal_hint () : bool :=
let gl := Control.goal () in
lazy_match! gl with
| ?a -> ?b =>
let sort_a := get_value_of_hyp a in
match check_constr_equal sort_a constr:(Prop) with
| true => goal_impl_msg a; true
| false => goal_func_msg a; true
end
| ∀ _ ∈ conv ?v_type, _ => goal_forall_el_msg v_type; true
| ∀ _ ∈ ?v_type, _ => goal_forall_el_msg v_type; true
| ∀ _ > ?y, _ => goal_forall_gt_msg y; true
| ∀ _ ≥ ?y, _ => goal_forall_ge_msg y; true
| ∀ _ < ?y, _ => goal_forall_lt_msg y; true
| ∀ _ ≤ ?y, _ => goal_forall_le_msg y; true
| ∀ _ ?q, _ => goal_forall_pred_msg q; true
| ∃ _ ∈ conv ?v_type, _ => goal_exists_el_msg v_type; true
| ∃ _ ∈ ?v_type, _ => goal_exists_el_msg v_type; true
| ∃ _ > ?y, _ => goal_exists_gt_msg y; true
| ∃ _ ≥ ?y, _ => goal_exists_ge_msg y; true
| ∃ _ < ?y, _ => goal_exists_lt_msg y; true
| ∃ _ ≤ ?y, _ => goal_exists_le_msg y; true
| ∃ _ ≠ ?y, _ => goal_exists_ne_msg y; true
| ∃ _ ?q, _ => goal_exists_pred_msg q; true
| forall v:?v_type, _ => goal_forall_msg v_type; true
| exists v:?v_type, _ => goal_exists_msg v_type; true
| _ /\ _ => goal_and_msg (); true
| _ \/ _ => goal_or_msg (); true
| not ?g => goal_neg_msg g; true
| _ => false
end.
Local Ltac2 forall_filter (x : constr) : bool :=
lazy_match! x with
| ?a -> ?b => false
| ∀ _ _ _, _ => true
| ∀ _ _, _ => true
| forall _, _ => true
| _ => false
end.
Local Ltac2 exists_filter (x : constr) : bool :=
lazy_match! x with
| exists _, _ => true
| ∃ _ _ _, _ => true
| ∃ _ _, _ => true
| _ => false
end.
Local Ltac2 is_empty (ls : 'a list) :=
match ls with
| _::_ => false
| [] => true
end.
Ltac2 print_hints () :=
if (goal_wrapped_template_msg ())
then (info_notice (of_string "Follow the advice in the goal window."))
else
match Control.case (solvable_by_core_auto) with
| Val _ => goal_directly ()
| Err exn =>
let hint_given := goal_hint () in
let hyps := List.map (fun (i, x, t) => t) (Control.hyps ()) in
let forall_hyps := List.filter (forall_filter) hyps in
let exists_hyps := List.filter (exists_filter) hyps in
if (is_empty forall_hyps)
then ()
else (
info_notice(of_string "You can use one of the ‘for all’-statements (∀):");
List.fold_left (fun _ h => info_notice (concat (of_string " ") (of_constr h))) forall_hyps ();
replace_msg "Use ... := ... in ...." "Use ${0:x} := ${1:0} in ({2:i}).${3}"
);
if (is_empty exists_hyps)
then ()
else (
info_notice(of_string "You can use one of the ‘there exists’-statements (∃):");
List.fold_left (fun _ h => info_notice (concat (of_string " ") (of_constr h))) exists_hyps ();
replace_msg "Obtain ... according to ...." "Obtain ${0:x} according to (${1:i}).${2}"
);
if (Bool.and (is_empty forall_hyps)
(Bool.and (is_empty exists_hyps) (Bool.neg hint_given)))
then (goal_no_hint ())
else ()
end.
Given a forall- or exists-statement, prints suggestion how to use it.
Ltac2 suggest_how_to_use (x : constr) (label : ident option) :=
if Bool.neg (get_print_hypothesis_flag ()) then ()
else
let msg_label :=
match label with
| None => of_string "..."
| Some i => of_ident i
end
in
let print_forall_msg () :=
info_notice (concat_list [
of_string "To use "; of_constr x; of_string ", consider:"]);
let template := match label with
| None => "Use ${0:x} := ${1:0} in (${2:0 = 0}).${3}"
| Some i => String.concat "" ["Use ${0:x} := ${1:0} in ("; Ident.to_string i; ").${2}"]
end in
insert_msg "Use ... := ... in ...." template in
let print_exists_msg () :=
info_notice (concat_list [
of_string "To use "; of_constr x; of_string ", consider:"]);
insert_msg "Obtain ... according to ...." "Obtain ${0:x} according to (${1:i}).${2}" in
lazy_match! x with
| ?a -> ?b => ()
| forall _, _ => print_forall_msg ()
| ∀ _ _ , _ => print_forall_msg ()
| ∀ _ > _ , _ => print_forall_msg ()
| ∀ _ ≥ _, _ => print_forall_msg ()
| ∀ _ < _ , _ => print_forall_msg ()
| ∀ _ ≤ _, _ => print_forall_msg ()
| exists _, _ => print_exists_msg ()
| ∃ _ _, _ => print_exists_msg ()
| ∃ _ > _, _ => print_exists_msg ()
| ∃ _ ≥ _, _ => print_exists_msg ()
| ∀ _ < _ , _ => print_forall_msg ()
| ∀ _ ≤ _, _ => print_forall_msg ()
| _ => ()
end.
Given a forall- or exists-statement, prints suggestion how to use it,
after statement is proven.
(for use in 'We claim that ...'-tactic.)
Ltac2 suggest_how_to_use_after_proof (x : constr) (label : ident option) :=
if Bool.neg (get_print_hypothesis_flag ()) then ()
else
let msg_label :=
match label with
| None => of_string "..."
| Some i => of_ident i
end
in
let print_forall_msg () :=
info_notice (concat_list [
of_string "After proving "; of_constr x; of_string ", consider:"]);
let template := match label with
| None => "Use ${0:x} := ${1:0} in (${2:i}).${3}"
| Some i => String.concat "" ["Use ${0:x} := ${1:0} in ("; Ident.to_string i; ").${2}"]
end in
insert_msg "Use ... := ... in ...." template in
let print_exists_msg () :=
info_notice (concat_list [
of_string "After proving "; of_constr x; of_string ", consider:"]);
insert_msg "Obtain such a ...." "Obtain such a ${0:x}.${1}" in
lazy_match! x with
| ?a -> ?b => ()
| forall _, _ => print_forall_msg ()
| ∀ _ _, _ => print_forall_msg ()
| ∀ _ > _, _ => print_forall_msg ()
| ∀ _ ≥ _, _ => print_forall_msg ()
| exists _, _ => print_exists_msg ()
| ∃ _ _, _ => print_exists_msg ()
| ∃ _ > _, _ => print_exists_msg ()
| ∃ _ ≥ _, _ => print_exists_msg ()
| _ => ()
end.
End HelpNewHyp.
Close Scope subset_scope.
if Bool.neg (get_print_hypothesis_flag ()) then ()
else
let msg_label :=
match label with
| None => of_string "..."
| Some i => of_ident i
end
in
let print_forall_msg () :=
info_notice (concat_list [
of_string "After proving "; of_constr x; of_string ", consider:"]);
let template := match label with
| None => "Use ${0:x} := ${1:0} in (${2:i}).${3}"
| Some i => String.concat "" ["Use ${0:x} := ${1:0} in ("; Ident.to_string i; ").${2}"]
end in
insert_msg "Use ... := ... in ...." template in
let print_exists_msg () :=
info_notice (concat_list [
of_string "After proving "; of_constr x; of_string ", consider:"]);
insert_msg "Obtain such a ...." "Obtain such a ${0:x}.${1}" in
lazy_match! x with
| ?a -> ?b => ()
| forall _, _ => print_forall_msg ()
| ∀ _ _, _ => print_forall_msg ()
| ∀ _ > _, _ => print_forall_msg ()
| ∀ _ ≥ _, _ => print_forall_msg ()
| exists _, _ => print_exists_msg ()
| ∃ _ _, _ => print_exists_msg ()
| ∃ _ > _, _ => print_exists_msg ()
| ∃ _ ≥ _, _ => print_exists_msg ()
| _ => ()
end.
End HelpNewHyp.
Close Scope subset_scope.