Застрял на доказательстве с неоднородным равенством

Импорт:

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

Я немного изменил ваш inc, чтобы упростить:

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))

Лемма:

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

Тип отверстия

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)))))

Так что нам понадобится что-то вроде subst-removeable из стандартной библиотеки:

≡-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

Тип

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)

Практически то, что нам нужно. Теперь мы хотим добавить hcong inc, но компилятор отклоняет это. Вот реализация 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

Итак, x и y должны быть одного типа A, в то время как наш subst меняет тип. Вот реализация hcong, которая нам нужна:

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

И последнее доказательство:

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)

Также мы можем объединить subst-removable и 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

Кстати, Пирс имел в виду этот тип данных, я полагаю:

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

Кстати, ваш надуманный пример можно доказать без дополнительных определений:

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)

Кстати, hsubst-ix1 можно значительно сократить, поскольку вы используете гетерогенное равенство и вам не нужно доказывать равенство типов:

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

Оказывается, эта проблема чем-то похожа на эту, за исключением того, что здесь конструкторы инъективных типов не не помогло.

Обычно вы можете использовать subst для разнородного равенства, когда очевидно, что два типа на сторонах равенства равны:

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

Это hsubst почти то же самое, что subst для пропозиционального равенства, за исключением типа равенства. Поскольку от нас требуется знать, что типы x и x' равны, мы могли бы просто преобразовать наше неоднородное доказательство равенства в нормальное, а затем использовать обычное subst.

Однако OP (т.е. я) попытался заменить, используя равенство, у которого были индексированные типы с обеих сторон, и не было очевидно, что индексы были равны. Решение состоит в том, чтобы параметризовать hsubst индексом и потребовать дополнительного доказательства равенства для индексов:

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

Я немного поэкспериментировал, чтобы выяснить, какие аргументы можно вывести, и результат приведен выше. Вот надуманный пример:

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