Practically every lemma and theorem is only defined for well-formed patterns, so it would make sense to represent these patterns specifically using sig well_formed. Then wrappers may be defined for pattern operators, like this example for patt_and:
Definition patt_and_wrapper : forall (a b : sig well_formed), sig well_formed.
Proof.
intros [a wfa] [b wfb].
exists (a and b).
now apply well_formed_and.
Defined.
Building the well-formedness proofs into the patterns themselves would significantly reduce, or in simpler cases possibly even eliminate, the need for providing these proofs manually (which are mostly trivial with auto and wf_auto2 anyway).
Another usecase of dependent pairs would be creating fresh variables, like this:
Definition get_fresh_evar (φ : Pattern) : sig (.∉ free_evars φ).
Proof.
exists (fresh_evar φ); auto.
Defined.
A version for a list of patterns may be defined similarly. Not only would pose proofing this as [y Hy] be cleaner than the current remember (fresh_evar φ) as y. assert (y ∉ free_evars φ) as Hy by auto. method, it could also be used directly in a slightly modified version of total_phi_impl_phi, for example.
Practically every lemma and theorem is only defined for well-formed patterns, so it would make sense to represent these patterns specifically using
sig well_formed. Then wrappers may be defined for pattern operators, like this example forpatt_and:Building the well-formedness proofs into the patterns themselves would significantly reduce, or in simpler cases possibly even eliminate, the need for providing these proofs manually (which are mostly trivial with
autoandwf_auto2anyway).Another usecase of dependent pairs would be creating fresh variables, like this:
A version for a list of patterns may be defined similarly. Not only would
pose proofing thisas [y Hy]be cleaner than the currentremember (fresh_evar φ) as y. assert (y ∉ free_evars φ) as Hy by auto.method, it could also be used directly in a slightly modified version oftotal_phi_impl_phi, for example.