I have 56 goals that can be solved using combination of few rewrite lemmas + Induction hypothesis.

How can I automate that.

Perhaps some `//=`

placed at their apparition point might help?

But `//=`

does not use external rewrite lemmas, at least not by default. How to fix that ?

actually `//=`

is the reasaon I have 56 instead of 63.

If the lemmas are morally about the same thing, I suggest you craft a multi rule https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#multi-rule-rewriting

I mean `by rewrite //= !myrule`

. But note that you can use `auto`

or any other Coq tactic in the middle of an ssr script.

yes they are all about the exact same thing, thanks for the idea of multi rules.

Another thing we often do is to load the context with more facts (via `have`

& co), and this automatically powers `//`

up.

~one~ Two question, so `//`

basically solve the goal by applying only one hypothesis right? it is possible to make it use two ?

Also it is possible to use 'have'(or similar functionality) to specify a lemma by name instead of by lemma's body:

I have a lemma that says:

```
Lemma trie_lookup_builder_a: forall (l r: Trie A) a, trie_lookup (xH) (trie_builder l a r) = a.
Proof.
by case => [|l] [|r] [a|];
rewrite /trie_builder /trie_lookup /=.
Qed.
```

I want to do

```
have: trie_lookup_builder_a
```

instead of rewrting the whole lemma body, I tried having this lemma in general and `//`

solved lots of the goals, I just want the have statement to look short if possible.

I'm a bit confused by the formatting of your message. Do you want `have ? := trie_lookup_builder_a`

?

yup that was exactly what I wanted! thanks

Last updated: Jul 25 2024 at 15:02 UTC