Stream: Coq users

Topic: Lots of unfold, simpl


view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Dec 04 2021 at 21:22):

example of what i'm talking about

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 04 2021 at 21:29):

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

view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 04 2021 at 21:39):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Dec 04 2021 at 23:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC