Stuck on proof with heterogeneous equality

Question

I have a binary number representation, plus some conversion to and from Nat:

open import Data.Nat
open import Data.Nat.Properties
open import Function
open import Relation.Binary.PropositionalEquality hiding (trans; cong; subst; sym)
open import Relation.Binary.HeterogeneousEquality
open import Data.Unit
open import Algebra
module CS = CommutativeSemiring commutativeSemiring 

data Bin : ℕ → Set where
  zero  : Bin zero
  2*n   : ∀ {n} → Bin n → Bin (n + n)
  2*n+1 : ∀ {n} → Bin n → Bin (suc (n + n))

suc-lem : ∀ n → suc (suc (n + n)) ≡ suc n + suc n
suc-lem zero = refl
suc-lem (suc n) rewrite 
    CS.+-comm n (suc n)
  | suc-lem n | CS.+-comm n (suc (suc n)) 
  | CS.+-comm n (suc n) = refl

inc : ∀ {n} → Bin n → Bin (suc n)
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 {n} b) rewrite suc-lem n = 2*n (inc b)

nat2bin : (n : ℕ) → Bin n
nat2bin zero = zero
nat2bin (suc n) = inc (nat2bin n)

bin2nat : ∀ {n} → Bin n → ℕ
bin2nat {n} b = n

I think I need heterogeneous equality for proving things here, since it's usually not evident that the Nat indices of two Bin-s are equal. I'm rather inexperienced in Agda though, so please tell me if the approach is misguided.

I'm stuck with the following:

lem : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) = 
  subst
    (λ b → 2*n+1 (inc (inc (nat2bin n))) ≅ inc (inc b))
    (sym $ lem ?) ? 

The obvious thing would be to plug in n into sym $ lem ?, but that results in an error complaining that suc (n + n) != n + suc n.

I'd like to know why this happens or how it could be helped.

Answer 1

Imports:

open import Level hiding (zero; suc)
open import Function
open import Relation.Binary.HeterogeneousEquality
  renaming (sym to hsym; trans to htrans; cong to hcong; subst to hsubst)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin hiding (_+_)
open import Algebra
open import Data.Nat.Properties
module ℕplus = CommutativeSemiring commutativeSemiring

I've rearranged your inc a little to simplify things:

inc : ∀ {n} → Bin n → Bin (suc n)
inc zero = 2*n+1 zero
inc (2*n b) = 2*n+1 b
inc (2*n+1 {n} b) = subst (Bin ∘ suc) (ℕplus.+-comm n (suc n)) (2*n (inc b))

Lemma:

lem : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) = {!!}

The type of the hole is

2*n+1 (inc (inc (nat2bin n))) ≅
      inc
      (subst ((λ {.x} → Bin) ∘ suc) (ℕplus.+-comm (suc n) (suc (suc n)))
       (2*n (inc (inc (nat2bin n)))))

So we need something like subst-removable from the standart library:

≡-subst-removable : ∀ {a p} {A : Set a}
                    (P : A → Set p) {x y} (eq : x ≡ y) z →
                    P.subst P eq z ≅ z
≡-subst-removable P refl z = refl

The type of

hsym $
  ≡-subst-removable
    (Bin ∘ suc)
    (ℕplus.+-comm (suc n) (suc (suc n)))
    (2*n $ inc $ inc $ nat2bin n)

is

(2*n $ inc $ inc $ nat2bin n) ≅
      subst ((λ {.x} → Bin) ∘ suc) (ℕplus.+-comm (suc n) (suc (suc n)))
      (2*n $ inc $ inc $ nat2bin n)

Almost what we need. Now we want to add hcong inc, but compiler rejects it. Here is the implementation of cong:

cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}
       (f : (x : A) → B x) → x ≅ y → f x ≅ f y
cong f refl = refl

So x and y must be of the same type A, while our subst changes the type. Here is the implementation of hcong, that we need:

hcong' : {α β γ : Level} {I : Set α} {i j : I}
       -> (A : I -> Set β) {B : {k : I} -> A k -> Set γ} {x : A i} {y : A j}
       -> i ≡ j
       -> (f : {k : I} -> (x : A k) -> B x)
       -> x ≅ y
       -> f x ≅ f y
hcong' _ refl _ refl = refl

And the final proof:

lem : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem zero = refl
lem (suc n) =
  hcong'
    (Bin ∘ suc)
    (ℕplus.+-comm (suc n) (suc (suc n)))
    inc
    $ hsym
      $ ≡-subst-removable
          (Bin ∘ suc)
          (ℕplus.+-comm (suc n) (suc (suc n)))
          (2*n $ inc $ inc $ nat2bin n)

Also, we can consolidate subst-removable and cong:

≡-cong-subst-removable : {α β γ : Level} {I : Set α} {i j : I}
                       -> (A : I -> Set β) {B : {k : I} -> A k -> Set γ}
                       -> (e : i ≡ j)
                       -> (x : A i)
                       -> (f : {k : I} -> (x : A k) -> B x)
                       -> f (subst A e x) ≅ f x
≡-cong-subst-removable _ refl _ _ = refl

lem' : ∀ n → 2*n+1 (inc (nat2bin n)) ≅ inc (inc (2*n+1 (nat2bin n)))
lem' zero = refl
lem' (suc n) = hsym $
  ≡-cong-subst-removable
    (Bin ∘ suc)
    (ℕplus.+-comm (suc n) (suc (suc n)))
    (2*n $ inc $ inc $ nat2bin n)
    inc

BTW, Pierce meant this datatype, I suppose:

data Bin : Set where
  zero  : Bin
  2*n   : Bin → Bin
  2*n+1 : Bin → Bin

BTW2, it's possible to prove your contrived-example without additional definitions:

contrived-example : {n : ℕ} {f : Fin (n + suc n)}
                  -> f ≅ fromℕ (n + suc n)
                  -> f ≅ fromℕ (suc n + n)
contrived-example {n} eq = htrans eq $ hcong fromℕ $ ≡-to-≅ $ ℕplus.+-comm n (suc n)

BTW3, hsubst-ix1 can be reduced a lot, since you use heterogeneous equality and do not need to prove equality of types:

hsubst' : {C1 C2 : Set} {x : C1} {y : C2}
        -> (P : {C : Set} -> C -> Set)
        -> x ≅ y
        -> P x
        -> P y
hsubst' _ refl x = x

contrived-example' : 
  ∀ n
  → (f : Fin (n + suc n)) 
  → (fromℕ (n + suc n) ≅ fromℕ (suc n + n))
  → (f ≅ fromℕ (n + suc n))
  → (f ≅ fromℕ (suc n + n)) 
contrived-example' n f eq p = hsubst' (λ f' → f ≅ f') eq p

Answer 2

It turns out that this problem is somewhat similar to this one, except that here injective type constructors don't help.

Normally you can use the subst for heterogeneous equality when it is evident that the two types on the sides of the equality are equal:

hsubst :
  {A    : Set}
  (P    : A → Set)
  {x x' : A}
  → x ≅ x'
  → P x
  → P x' 
hsubst P refl p = p 

This hsubst is pretty much the same as subst for propositional equality, except for the type of the equality. Since we are required to know that the types of x and x' are equal, we could have just converted our heterogeneous equality proof into a normal one, and then used the regular subst.

However, OP (i. e. me) tried to substitute using an equality that had indexed types on both sides, and it was not evident that the indices were equal. The solution is to parametrize hsubst by the index and demand an additional equality proof for the indices:

hsubst-ix1 : 
    {I    : Set}
    (C    : I → Set)  
    (P    : ∀ {i} → C i → Set)
    {i i' : I}
    {x    : C i}
    {x'   : C i'}
    → i ≡ i'
    → x ≅ x'
    → P x
    → P x'
hsubst-ix1 C P refl refl p = p

I experimented a bit to find out which arguments can be left to be inferred, and the result is above. Here's a contrived example:

open import Relation.Binary.HeterogeneousEquality hiding (cong)
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin hiding (_+_)
open import Algebra
open import Data.Nat.Properties
module ℕplus = CommutativeSemiring commutativeSemiring

contrived-example : 
  ∀ n
  → (f : Fin (n + suc n)) 
  → (fromℕ (n + suc n) ≅ fromℕ (suc n + n))
  → (f ≅ fromℕ (n + suc n))
  → (f ≅ fromℕ (suc n + n)) 
contrived-example n f eq p =
  hsubst-ix1
    -- the type constructor to be indexed
    Fin
    -- substitution
    (λ f' → f ≅ f')
    -- proof that the indices are equal
    (cong suc (ℕplus.+-comm n (suc n)))
    -- heterogeneous equality
    eq
    -- original expression
    p