Stream: Coq users

Topic: Merge variables with same types in hypothesis list

view this post on Zulip Clément Blaudeau (Jan 17 2022 at 15:53):

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 !

view this post on Zulip Théo Winterhalter (Jan 17 2022 at 15:56):

You have 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.

view this post on Zulip Clément Blaudeau (Jan 17 2022 at 16:03):

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: Oct 13 2024 at 01:02 UTC