search

radeusgd / QuotedPatternMatchingProof

A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
3 stars 0 forks source link

Hints for tactics #4

Open radeusgd opened 4 years ago

radeusgd commented 4 years ago

It seems useful to add constructors as 'hints' to the prover, so that the auto and other tactics can use them.

For example:

Inductive is_free_in : label -> Term -> Prop :=
| fv_var : forall x, is_free_in x (Var x)
| fv_app1 : forall x t1 t2, is_free_in x t1 -> is_free_in x (App t1 t2)
| fv_app2 : forall x t1 t2, is_free_in x t2 -> is_free_in x (App t1 t2)
| fv_lam : forall x y t T, is_free_in x t -> x <> y -> is_free_in x (Lam y T t)
.
Hint Constructors is_free_in.

When I have a goal is_free_in x (Var x), normally I'd have to write apply fv_var, but after invoking the Hint command, I can just call auto. This is useful as I can call for example: induction something; auto and have all the trivial branches dealt with in one line instead of looking for each rule separately.

radeusgd commented 4 years ago

Another possible extension is adding some Lemmas as hints, so that when the goal looks like the result of some lemma it could be applied. For now I haven't figured out how to do that reliably (Hint Immediate doesn't seem to work, but maybe I used it wrong).

On another hand sometimes writing the used Lemma explicitly makes the proof clearer, so maybe overusing this is not the best idea either.

radeusgd commented 4 years ago

I have learnt I can also do auto using LemmaName which adds temporarily a lemma to the hints database. Looks like a good intermediate solution - I explicitly state what lemma I use, but if possible, auto can do the manipulation automatically.