Library Waterproof.Util.Since
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.MessagesToUser.
Require Import Waterprove.
Require Import Util.Init.
Require Import Util.TypeCorrector.
Local Ltac2 get_type (x: constr) : constr := eval unfold type_of in (type_of $x).
Local Ltac2 check_if_not_reference (x : constr) :=
let type_x := get_type x in
match! type_x with
| Prop => ()
| Set => ()
| Type => ()
| _ => throw (concat_list
[of_string "Cannot use reference "; of_constr x; of_string " with `Since`. Try `By "; of_constr x; of_string " ...` instead."])
end.
Local Ltac2 check_if_not_statement (x : constr) :=
let err_msg := concat_list
[of_string "Cannot use statement "; of_constr x; of_string " with `By`. Try `Since "; of_constr x; of_string " ...` instead."]
in
let type_x := get_type x in
match! type_x with
| Prop => throw err_msg
| Set => throw err_msg
| Type => throw err_msg
| _ => ()
end.
Attempts to prove claimed_cause with minimal automation,
and then executes by_tactic with the proof of claimed_cause
as an argument.
Expects that by_tactic can throw a (Waterprove.)FailedToUse error,
those errors are caught; the extra lemma that the automation failed to use
is used in a new error that is thrown.
Ltac2 since_framework (by_tactic : constr -> unit) (claimed_cause : constr) :=
let claimed_cause := correct_type_by_wrapping claimed_cause in
check_if_not_reference claimed_cause;
let id_cause := Fresh.in_goal @_temp in
match Control.case (fun () =>
assert $claimed_cause as $id_cause by
(waterprove 1 true Shorten))
with
| Err (FailedToProve _) =>
throw (concat_list
[of_string "State that "; of_constr claimed_cause; of_string " holds";
of_string " before using it in `Since ...`."])
| Err exn => Control.zero exn
| Val _ =>
let cause := Control.hyp id_cause in
match Control.case (fun () =>
by_tactic cause)
with
| Val _ => clear $id_cause
| Err (FailedToUse h) =>
let type_h := (get_type h) in
clear $id_cause;
throw (concat_list
[of_string "Could not verify this follows from "; of_constr type_h; of_string "."])
| Err exn => clear $id_cause; Control.zero exn
end
end.
Wrapper for the main functionality of 'By ...'-tactics,
such that the main fucntionality can be reused in 'Since ...'-tactics.
Checks whether xtr_lemma is not a statement (i.e. not a Prop/Set/Type) and
catches (Waterprove.)FailedToUse errors to turn them into user-readable errors.
Ltac2 wrapper_core_by_tactic (by_tactic : constr -> unit) (xtr_lemma : constr) :=
check_if_not_statement xtr_lemma;
match Control.case (fun () => by_tactic xtr_lemma) with
| Val _ => ()
| Err (FailedToUse h) => throw (concat_list
[of_string "Could not verify this follows from "; of_constr h; of_string "."])
| Err exn => Control.zero exn
end.
check_if_not_statement xtr_lemma;
match Control.case (fun () => by_tactic xtr_lemma) with
| Val _ => ()
| Err (FailedToUse h) => throw (concat_list
[of_string "Could not verify this follows from "; of_constr h; of_string "."])
| Err exn => Control.zero exn
end.