Hi! In my proofs, I often get a large number of variables with some similar types. If they are quantified together, Coq will merge them into
a, c : T1. If not, they will get 2 different lines:
a:T1 ... b:T1. Is there a way to clean (factorize?) a proof state to improve readability? (especially, compactness)
Here is a minimal example:
Parameter T1 T2 :Type. Lemma my_lemma: forall (a:T1) (b:T2) (c:T1) (d:T2), False. Proof. intros. (* factorize proof state to get : a, c : T1 b, d : T2 *) Admitted.
I'm here interested in the case where of course b does not appear in c's type.
Thanks a lot !
move tactics to do this manually: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.move
I don't know if there is something automatic.
Thanks ! That's a starting point, I'm trying out some ltac to see if I can get it to move all variables of the same type to the top...
Last updated: Sep 26 2023 at 12:02 UTC