If my code has lots of "unfold", "simpl" in it, how can I clean this up? it doesn't seem right that like half a proof should be "unfold" and "simpl"
Local Proposition tensor_card_is_strict_right_iso_id : ∏ eq_ρ : I_posttensor (monoidal_cat_tensor FinCard) (monoidal_cat_unit FinCard) = functor_identity (pr1 FinCard), is_nat_z_iso_id eq_ρ (monoidal_cat_right_unitor FinCard). Proof. unfold is_nat_z_iso_id. intros eq_ρ c. unfold nat_comp_to_endo. set (Δ_sdg := (pr1 FinCard)). set (Rtensor0 := (I_posttensor _ _)). set (idfunctor := (functor_identity _)). rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _). cbv beta in j. assert (j = right_unitor_id c) as RW by apply (setproperty natset); rewrite RW. unfold right_unitor_id, transportb. apply fincard_hom_extensionality. intro x. unfold Rtensor0 in x. simpl in x. unfold functor_fix_snd_arg_ob in x. unfold monoidal_cat_tensor in x. simpl in x. unfold ordinal_addition in x. unfold monoidal_cat_unit in x. simpl in x. unfold tensor_unit in x. unfold monoidal_cat_right_unitor. simpl. unfold functor_fix_snd_arg_ob. unfold monoidal_cat_tensor. simpl. unfold ordinal_addition, monoidal_cat_unit. simpl. unfold AugmentedSimplexCategory.tensor_unit, tensor_right_unitor_card_nt_data. simpl. induction (natplusr0 c). simpl. reflexivity. Qed.
example of what i'm talking about
It would be nice if I could tell coq to always unfold these terms every time they come up in the goal or in a hypothesis. Lots of the time, a term is just a name for an attribute and I always want the computational thing itself. Like, if it's an accessor, then I always want to just unfold it to the thing it's talking about.
Here, ordinal_addition is just like, a wrapper for natural number addition. I always want to replace ordinal_addition n m with n + m.
Arguments name /. ensures that
simpl always unfolds
Second, for many tactics you can skip both
unfold. For instance, any occurrence of
simpl. reflexivity. can be replaced by
unfold x. apply lemma is _often_ reducible to just
apply lemma (or sometimes you need ssreflect’s
apply: lemma). This isn’t alone on its own, but…
instead of the unfold tactic, it can be useful to state high-level rewrite rules as lemmas; some of those can be proven by just
reflexivity or with few operations, but hide a complicated sequence of
the art is stating lemmas which are meaningful on their own.
For instance, I can’t be sure here, but is your code proving something like
1 * x = x on some high-level product by unfolding the unit and the product, and simplifying?
for instance, I see you unfold
monoidal_cat_unit in both
x and the goal — is there a common lemma to be abstracted?
Last: sometimes, a
Definition foo := bar. should just be a
Notation foo := bar., or
Notation foo := bar (only parsing). — that’s basically expanded at parse-time, so that it will never get in the way of any tactic.
Ok, thanks for these tips, I'll try and integrate them into my code.
FYI the main tactic i've been having trouble with which requires lots of unfold/simpl is equality induction / rewrite. I get errors of the form "illegal abstraction/ generalization" unless i simplify and unfold everything first.
Ooh I see. Then the rewrite lemmas might be harder to deploy, but transparency could work... A problem is that it doesn't scale much: unfolding many layers of abstraction blows up terms, and it's harder to write proofs where something must not be unfolded.
The general problem with rewrite is that it matches your rewrite against the goal syntactically (so it doesn't unfold to search matchez); ssreflect rewriting does more unfolding but only in certain cases.
In your case it's worse, since you're rewriting n + 0 by n in indexes... I wonder how other formalizations of category theory tackle this problem
Is this because the category is strict? Lax ones are more friendly to dependent types.
Last updated: Jan 29 2023 at 05:03 UTC