Make an automated compare functions' tactic
The goal of the issue is to make an automated tactic for the verification of the compare function. This automated tactic should handle the part where we apply the list of lemmas for the validity of known combinators/compare functions. For example, with the following proof:
Lemma compare_values_is_valid {a : Set} (c_value : a -> a -> int) :
Compare.Valid.t (fun _ => True) id c_value ->
Compare.Valid.t Value.Valid.t id (Indexable.compare_values c_value).
Proof.
intros H.
apply (Compare.equality (
let proj x :=
match x with
| Indexable.Value x => Some x
| _ => None
end in
Compare.projection proj (Compare.Option.compare c_value)
)); [sauto lq: on rew: off|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
eapply Compare.option_is_valid.
apply H.
}
all: intros [] []; unfold id; sfirstorder.
Qed.
were should automate the following part:
{ eapply Compare.projection_is_valid.
eapply Compare.option_is_valid.
apply H.
}
to a single tactic call (maybe not the apply H
as it is specific to this context).
The tactic should be made in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/environment/proofs/compare/ and be named valid_auto
. Inspiration for such tactic can be found in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/environment/proofs/rpc_arg/ or https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/environment/proofs/data_encoding There should be a database of hints as data-encodings with Data_encoding_db
. It is possible to call such hints database with eauto 1 with Data_encoding_db
.
In the second part of the task, you should propagate the use of this tactic to existing proofs (grep for eapply Compare.implies
).
-
make a compare tactic -
propagate the use of this tactic