Do we really want special case casts? (was: [Agda] Proof involving associativity of ++ of vectors)

[Samuel Gélineau]

On Sun, Oct 18, 2009 at 11:50 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>> Couldn't we define dependent versions of subst and cong
>> once and for all? Of course we can...
>
> Thanks for the explanation. Although the whole picture still
> puzzles me, I feel I understand cong and subst for indexed
> types more. It's relieving knowing that there is a way to
> define general subst and cong, even if they require some
> extra proofs. And I'd be interested to see a version of
> subst and cong parameterized on injectivity proofs.

Sure, here you go. I'm just fleshing out the implementation of cong
found in the "Congruence and substitutivity rules in heterogeneous
equality" thread which Nils keeps referring us to.

-- rewriting Relation.Nullary's Injective
-- to use ≡₁ and ≅ instead of ≡
Injective : ∀ {A B} → (A → B) → Set
Injective f = ∀ {x y}
            → f x ≡₁ f y
            →   x ≅  y

≅⇒≡₁ : ∀ {A B}{a : A}{b : B}
     → a ≅ b
     → A ≡₁ B
≅⇒≡₁ refl = refl

dependent-subst : {A : Set}{B : A → Set}
                → Injective B
                → (P : ∀ x → B x → Set)
                → {x₁ : A}{y₁ : B x₁}
                → {x₂ : A}{y₂ : B x₂}
                → y₁ ≅ y₂
                → P x₁ y₁
                → P x₂ y₂
dependent-subst inj P prf p with inj (≅⇒≡₁ prf) | prf
... | refl | refl = p

dependent-cong : {A : Set}{B : A → Set}
               → Injective B
               → {C : ∀ x → B x → Set}
               → (f : ∀ x y → C x y)
               → {x₁ : A}{y₁ : B x₁}
               → {x₂ : A}{y₂ : B x₂}
               → y₁ ≅ y₂
               → f x₁ y₁
               ≅ f x₂ y₂
dependent-cong inj f prf with inj (≅⇒≡₁ prf) | prf
... | refl | refl = refl


By the way, I was confused at first by the need for adding "| prf" in
addition to "with inj (≅⇒≡₁ prf)". The reason seems to be that the
order of the arguments matters, and the proof of (x₁ ≅ x₂) must occur
before (y₁ ≅ y₂) or the refl pattern will be rejected. For example:

fail : {A : Set}{B : A → Set}
     → {x₁ : A}{y₁ : B x₁}
     → {x₂ : A}{y₂ : B x₂}
     → y₁ ≅ y₂
     → x₁ ≅ x₂
     → y₁ ≅ y₂
fail refl refl = refl -- error
-- x₁ != x₂ of type A
-- when checking that the pattern refl has type y₁ ≅ y₂

pass : {A : Set}{B : A → Set}
     → {x₁ : A}{y₁ : B x₁}
     → {x₂ : A}{y₂ : B x₂}
     → x₁ ≅ x₂
     → y₁ ≅ y₂
     → y₁ ≅ y₂
pass refl refl = refl


I don't know what is the cause of this ordering restriction, but I'll
make sure to remember it now.

– Samuel