Stream: Coq users

Topic: Lots of unfold, simpl

Patrick Nicodemus (Dec 04 2021 at 21:21):

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"

Patrick Nicodemus (Dec 04 2021 at 21:22):

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.

Patrick Nicodemus (Dec 04 2021 at 21:22):

example of what i'm talking about

Patrick Nicodemus (Dec 04 2021 at 21:23):

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.

Patrick Nicodemus (Dec 04 2021 at 21:24):

Here, ordinal_addition is just like, a wrapper for natural number addition. I always want to replace ordinal_addition n m with n + m.

Paolo Giarrusso (Dec 04 2021 at 21:29):

First, Arguments name /. ensures that simpl always unfolds name.

Paolo Giarrusso (Dec 04 2021 at 21:31):

Second, for many tactics you can skip both simpl and unfold. For instance, any occurrence of simpl. reflexivity. can be replaced by reflexivity; similarly, 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…

Paolo Giarrusso (Dec 04 2021 at 21:37):

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 rewrite steps.

Paolo Giarrusso (Dec 04 2021 at 21:39):

the art is stating lemmas which are meaningful on their own.

Paolo Giarrusso (Dec 04 2021 at 21:40):

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?

Paolo Giarrusso (Dec 04 2021 at 21:42):

for instance, I see you unfold monoidal_cat_tensor, ordinal_addition and monoidal_cat_unit in both x and the goal — is there a common lemma to be abstracted?

Paolo Giarrusso (Dec 04 2021 at 21:43):

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.

Patrick Nicodemus (Dec 04 2021 at 23:01):

Ok, thanks for these tips, I'll try and integrate them into my code.

Patrick Nicodemus (Dec 04 2021 at 23:34):

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.

Paolo Giarrusso (Dec 04 2021 at 23:47):

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.

Paolo Giarrusso (Dec 04 2021 at 23:50):

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.

Paolo Giarrusso (Dec 04 2021 at 23:54):

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

Li-yao (Dec 05 2021 at 15:30):

Is this because the category is strict? Lax ones are more friendly to dependent types.

Last updated: Oct 12 2024 at 12:01 UTC