cast vs subst in Data.Fin

[conal]

I’m working on a collection of proofs for submission to Data.Fin.Properties. I can phrase & prove via cast or via subst Fin. For my own use, I need the subst versions, to fit into a setting more general than Fin. If cast is a better fit for Fin, I’m happy to adapt via an equivalence property cast≗subst : ∀ {m n} (m≡n : m ≡ n) → cast m≡n ≗ subst Fin m≡n (which could also go into Data.Fin.Properties).

Going with cast, I also need some properties of cast corresponding to ones about subst in Relation.Binary.PropositionalEquality.Properties, such as subst-sym-subst (which I’m calling cast-sym-cast for now). I don’t imagine we’d want to replicate all subst properties for cast, though.

Thoughts?

[JacquesCarette]

To me, the biggest advantage of cast over subst is that cast computes regardless of the actual proof of equality, while subst only reduces for refl. Working --without-K and with subst is amazingly tedious.

Side commentary: Using either of them is also misleading; we know that Fin n has an automorphism group of size n!. By singling out the id one as being the only one worth talking about when doing type isomorphism on Fin n hides a lot of the beauty of Id types.

[conal]

To me, the biggest advantage of cast over subst is that cast computes regardless of the actual proof of equality, while subst only reduces for refl.

Ah, interesting. Thanks for mentioning this difference.

From the definitions of cast and subst, I gather that reducing cast requires evaluating only the Fin argument (as you mentioned), while reducing subst requires evaluating only the equality argument. Do you have any insight to share about how cast’s requirement tends to be less burdensome than subst’s?

[conal]

For concreteness, here are two of the properties (in their cast form) I intend to submit in a PR (where ⊎ is Data.Sum). I’ll probably need the analogous properties for products as well.

join-assocˡ : ∀ {m n p} →
  join (m + n) p ∘ ⊎.map₁ (join m n) ∘ ⊎.assocˡ
    ≗ cast (sym (+-assoc m n p)) ∘ join m (n + p) ∘ ⊎.map₂ (join n p)

join-assocʳ : ∀ {m n p} →
  join m (n + p) ∘ ⊎.map₂ (join n p) ∘ ⊎.assocʳ
    ≗ cast (+-assoc m n p) ∘ join (m + n) p ∘ ⊎.map₁ (join m n)

[conal]

By singling out the id one as being the only one worth talking about when doing type isomorphism on Fin n hides a lot of the beauty of Id types.

Thanks! I’ll meditate on this perspective.

[gallais]

Do you have any insight to share about how cast’s requirement tends to be less burdensome than subst’s?

Mostly because cast (suc k) = suc (cast k) holds definitionally.
When you're proving something about a function's behaviour and need to use a
coercion to have the types match up on both sides of the propositional equality,
you do want to expose constructors as soon as possible so that you can appeal to cong.

Edit: appeal to cong or have a function applied to this coerced value reduce!

[conal]

Thanks for the tips, @JacquesCarette & @gallais!

[conal]

By singling out the id one as being the only one worth talking about when doing type isomorphism on Fin n hides a lot of the beauty of Id types.

Thanks! I’ll meditate on this perspective.

I did, and now I am enlightened. I had indeed gotten focused on the identity automorphism. Seeing equality as such (thanks to your remark) puts the problem I was working on into a wider context that I need anyway. Thanks again, @JacquesCarette!

[JacquesCarette]

Seems to me that all of @conal 's questions have been answered, so that this could be closed?

[conal]

Thanks again for the answers.