In Coq, I have an inductive property on elements which may appear many times in the same proof. I would like to know if it is possible for Coq to memorize elements for which the property has already been proven. Also I would like to know how it is possible to automatize simple proofs such as the one in my minimal working example:
Require Import List.
Require Import List Notations.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Inductive Figure : Type :=
| P : Figure
| L : Figure -> Figure -> Figure
| C : list Figure -> Figure.
Inductive good : Figure -> Prop :=
|gP : good P
|gL : good (L P P)
|gC (ff: list Figure) (H1: goodL ff): good (C ff)
with goodL : list Figure -> Prop :=
|g0 : goodL nil
|g' (f: Figure) (ff: list Figure) (H1: good f) (H2: goodL ff) : goodL (f::ff).
Example ex0: goodL [P ; (L P P); C [P ; L P P]].
Proof. apply g'. apply gP. apply g'. apply gL.
apply g'. apply gC. apply g'. apply gP. apply g'. apply gL. apply g0. apply g0.
As you can see in the example, the proof for good P and good (L P P) appear twice. In the real case, this could happen dozens of times in the same proof. Asserting intermediate lemmas would be of little help as the rules to apply are quite direct. It is just that I may have many sub-levels of lists with the same elements and I would like Coq to recall that we already proved them. Another option is to have Coq to most of work, as this looks like pretty straightforward to automatize, but I am only a beginner. Thank you.
If you just have a bunch of apply, you can usually refactor it using auto, to which you can pass the relevant lemmas explicitly with using (or implicitly via Hint databases):
auto 10 using g', g0, gP, gL, gC.
or, since those are all constructors,
repeat constructor.
Duplicate work only becomes a problem when it makes the tactic noticeably slow, at which point you can extract the work as intermediate lemmas and add them to auto using ... or whatever automation script you end up with.