Simplifying congruence proofs in Substitution

[L-TChen]

As commented by @jsiek

[JGS: I would have liked to prove all of these via cong and cong₂, but I have not yet found a way to make that work. It seems that various implicit parameters get in the way.]

congruence proofs are not really necessary if we annotate the equality with a type of terms explicitly. For example, instead of

cong-ext : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}
   → (∀{A} → ρ ≡ ρ′ {A})
     ---------------------------------
   → ∀{A} → ext ρ {B = B} ≡ ext ρ′ {A}

we should write

cong-ext : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}
   → (∀{A} → _≡_ {A = Ren Γ Δ} ρ ρ′)
     ---------------------------------
   → ∀{A} → _≡_ {A = Ren (Γ , B) (Δ , B)} (ext ρ) (ext ρ′)

so that cong can be applied to prove the statement without using the induction principle again.

Agda inserts metavariables for implicit variables which appears before the first explicit variable automatically. So, the ρ is not of type Rename Γ Δ but ∀ {A} → Γ ∋ A → Δ ∋ A but Γ ∋ _A_n → Δ ∋ _A_n for some metavariable n that is different from cong ext rr.

I can create a PR later if it helps.

[wenkokke]

Unfortunately, that’s tragically unreadable. Perhaps we could define an _≡[_]_ operator with explicit type information?

[L-TChen]

Or maybe a new syntax?

≡-syntax : {a : Level} (A : Set a) (x y : A) → Set a
≡-syntax A x y = x ≡ y

syntax ≡-syntax A x y = x ≡ y ⦂ A

But the use of the symbol ⦂ might be confusing.

[jsiek]

It would be helpful to see an example of how this would change the proofs that currently use the congruence rules, such as the proof of rename-subst-ren.

[L-TChen]

All proofs including rename-subst-ren until compose-rename remain the same after simplified congruence rules. (I haven't checked carefully what happens to compose-rename and remaining proofs.)

Some tweaks are needed though. For example, consider the following definitions using Rename:

• The type of ext needs to be changed from

ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
     -----------------------------------
  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)

to

ext : ∀ {Γ Δ B} →  (∀ {A} → Γ ∋ A → Δ ∋ A)
    -----------------------------------
  → ∀ {A} → Γ , B ∋ A → Δ , B ∋ A

where the variable B is moved before the first renaming (or after the first Rename).

• Then, cong-ext can actually be proved by cong directly:

cong-ext : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ} {B}
   → _≡_ {A = Rename Γ Δ} ρ ρ′
     ---------------------------------
   → _≡_ {A = Rename (Γ , B) (Δ , B)} (ext ρ) (ext ρ′)
cong-ext rr = cong ext rr 

• As for cong-rename, a variant of cong-app is needed since the type of rename ρ is not (x : A) → B x.

cong-app′ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (x : A) (y : B x) → Set c}
  → {f g : {x : A} (y : B x) → C x y}
  → _≡_ {A = {x : A} (y : B x) → C x y} f g → {x : A} (y : B x) → f {x} y ≡ g {x} y
cong-app′ refl _ = refl

• cong-rename is proved directly by the new variant cong-app′ without any induction:

cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ} {B} 
        → _≡_ {A = Rename Γ Δ} ρ  ρ′
          ------------------------
        → {M : Γ ⊢ B} → rename ρ M ≡ rename ρ′ M
cong-rename rr {M} = cong-app′ (cong rename rr) M

Similarly, some changes are also needed for Subst.

[jsiek]

Which Chapters of PLFA would these proposed changes impact?

[L-TChen]

Substitution and the chapter on Intrinsically-typed de Bruijn representation, I think.

It shouldn't be a bad idea to introduce Rename and Subst much earlier to clarify the types of operations on terms.

[jsiek]

Instead of DeBruijn, it looks like Untyped would need to change. But then there's the question of whether we'd want to let these chapters be slightly out of sync with the rest of the chapters which define there own ext. Let's see how many of those there are... More, Properties, and Subtyping. That's not so many. I suppose I'd be OK with all of them being changed.

I wonder how @wenkokke and @wadler feel about the proposed change to ext?

[L-TChen]

Fair enough. Perhaps I need to really make a PR for evaluation. That will take some time, though ...

[L-TChen]

Hum… I don’t think I have enough time to work on this in the foreseeable future. I am closing this issue as not planned. If anyone wants to pick up, please feel free to do so.