Skip to content
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

Set 'Help'-tactic to use default automation system. #36

Merged
merged 1 commit into from
Nov 6, 2023
Merged

Set 'Help'-tactic to use default automation system. #36

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
19 changes: 9 additions & 10 deletions theories/Tactics/Help.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ Require Import Util.Goals.
Require Import Util.Hypothesis.
Require Import Util.MessagesToUser.

Require Import Waterprove.

Ltac2 Type exn ::= [ Inner ].

Local Ltac2 create_forall_message (v_type: constr) :=
Expand Down Expand Up @@ -57,17 +59,14 @@ of_string " holds, then show a contradiction.
Use ‘Assume that (...).’ to do the first step."].

(**
Auxilliary tactic that checks if goal can be shown with minimal automation, i.e. only with core database.
Auxilliary tactic that checks if goal can be shown with automation
*)
Local Ltac2 solvable_by_core_auto () :=
let assertion_id := Fresh.in_goal @assert_goal in
let temp_id := Fresh.in_goal @temp in
let goal := Control.goal () in
assert $goal as $assertion_id;
Control.focus 1 1 (fun () =>
let hint_databases := Some ((@core)::[]) in
Std.auto Std.Off (Some 1) [] hint_databases
);
clear $assertion_id.
assert $goal as $temp_id;
Control.focus 1 1 (fun () => waterprove 5 true Main);
clear $temp_id.

(**
Give a hint indicating a potential step to proving a given proposition [g].
Expand Down Expand Up @@ -106,7 +105,7 @@ Show one of the statements, use ‘It suffices to show that (...).’ with the d
| not ?g => create_not_message g
| False => create_goal_wrapped_message ()
| _ =>
match Control.case solvable_by_core_auto with
match Control.case (solvable_by_core_auto) with
| Val _ => of_string "The goal can be shown immediately, use ‘We conclude that (...).’."
| Err exn => Control.zero Inner
end
Expand Down Expand Up @@ -137,4 +136,4 @@ Ltac2 print_goal_hint (g: constr option) :=
(** * Help tactic
Tries to give a hint how to proceed proving the current goal.
*)
Ltac2 Notation "Help" := print_goal_hint None.
Ltac2 Notation "Help" := print_goal_hint None.
Loading