[Agda] Why unification fail?

[Serge Leblanc]

Hi every, in the following example, how do informe Agda that 'i ⊔ o ≡
suc (k + i)' it's true and compatible?

Saluton ĉiun,en la sekva ekzemplo, kiel informi al Agda ke 'i ⊔ o ≡ suc
(k + i)' veras kaj kongruas?

Sinceran dankon,

-- 

Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190319/ff2f1738/attachment.html>
-------------- next part --------------
module Chomp2 where

  open import Data.Nat --as ℕ
  open import Data.Nat.Properties


  open import Function using (id ; _∘_)
  open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ) -- ; _≗_ ; refl ; sym ; trans ; cong ; cong₂ ; cong-app)
  open PropEq.≡-Reasoning


  infixr 15 _∷_

  data 𝕃 : ℕ → Set where
    [_] : (o : ℕ) → 𝕃 o
    _∷_ : ∀ {n} → (x : ℕ) → (xs : 𝕃 n) → 𝕃 (x + n)

  ŋ : ∀ {n} → 𝕃 n → ℕ
  ŋ [ o ] = o
  ŋ (h ∷ t) = h + ŋ t

  --infix 25  _⪾_   -- U+2ABE ⪾

  +-distribˡ-⊔′ : (m k : ℕ) → (m + k) ⊔ m ≡ k + m
  +-distribˡ-⊔′ m k = begin
    (m + k) ⊔ m ≡⟨ cong (λ s → s ⊔ m) (+-comm  m k) ⟩
    (k + m) ⊔ m ≡⟨ sym (+-distribʳ-⊔ m k 0) ⟩
    k ⊔ 0 + m ≡⟨ cong (_+ m) (⊔-identityʳ k) ⟩
    k + m
    ∎

  +-distribˡ-⊔″ : (m k : ℕ) → (m + k) ⊔ m ≡ m + k
  +-distribˡ-⊔″ m k = begin
    (m + k) ⊔ m ≡⟨ +-distribˡ-⊔′ m k ⟩
    k + m ≡⟨ +-comm k m ⟩
    m + k
    ∎

  +-distribʳ-⊔′ : (m k : ℕ) → m ⊔ (m + k) ≡ k + m
  +-distribʳ-⊔′ m k = begin
    m ⊔ (m + k) ≡⟨ cong (λ s → m ⊔ s) (+-comm m k) ⟩
    m ⊔ (k + m) ≡⟨ sym (+-distribʳ-⊔ m 0 k) ⟩
    k + m
    ∎

  +-distribʳ-⊔″ : (m k : ℕ) → m ⊔ (m + k) ≡ m + k
  +-distribʳ-⊔″ m k = begin
    m ⊔ (m + k) ≡⟨ +-distribʳ-⊔′ m k ⟩
    k + m ≡⟨ +-comm k m ⟩
    m + k
    ∎

  +-distribʳ-⊔‴ : (m k : ℕ) → m ⊔ suc (m + k) ≡ suc (k + m)
  +-distribʳ-⊔‴ m k = begin
    m ⊔ suc (m + k) ≡⟨ sym (cong (λ s → m ⊔ s) (+-suc m k)) ⟩
    m ⊔ (m + suc k) ≡⟨ +-distribʳ-⊔′ m (suc k) ⟩
    suc (k + m)
    ∎

  ⊔-cancelˡ-≡ : ∀ {i o₁ o₂} → i ⊔ (i + o₁) ≡ i ⊔ (i + o₂) → o₁ ≡ o₂
  ⊔-cancelˡ-≡ {i} {o₁} {o₂} eq rewrite +-distribʳ-⊔″ i o₁ | +-distribʳ-⊔″ i o₂ = +-cancelˡ-≡ i eq

  {-
  ⊔⇒≡ : (i o k : ℕ) → compare i (suc (i + k)) ≡ less i k → i ⊔ o ≡ suc (k + i)
  ⊔⇒≡ i o k lt = {!   !}
  -}

  l₁ = 3 ∷ 2 ∷ [ 4 ]
  l₂ = 3 ∷ 3 ∷ 5 ∷ [ 3 ]


  ⪾ : ∀ {n} → (x : ℕ) → 𝕃 n → 𝕃 (x ⊔ n)
  ⪾ i l with ŋ l | compare i (ŋ l) | inspect (compare i) (ŋ l)
  ⪾ i [ o ] | ŋl | less m k | [ eq ] {-rewrite ⊔⇒≡ i o k eq-} = {! suc k ∷ [ m ] !}
  ⪾ i (h ∷ t) | ŋl | less m k | [ eq ] = {! (suc (m + k) ∸ (ŋ (⪾ i t))) ∷ ⪾ i t !}
  ... | ŋl | equal m | [ eq ] {-rewrite ⊔-idem i-} = {! l !}
  ... | ŋl | greater m k | [ eq ] = {! suc k ∷ l !}

  ⫐ : ∀ {n₁ n₂} → 𝕃 n₁ → 𝕃 n₂ → 𝕃 (n₁ ⊔ n₂)
  ⫐ [ o ] l = {! ⪾ o l !}
  ⫐ l₁@(_ ∷ t) l₂ = {! ⪾ (ŋ l₁) (⫐ t l₂) !}

  {-
    ⪾ : ∀ {n₁ n₂} → 𝕃 n₁ → 𝕃 n₂ → 𝕃 (n₁ ⊔ n₂)
    ⪾ l₁@([ o₁ ]) l₂@([ o₂ ]) with compare o₁ o₂
    ... | less m k rewrite +-distribʳ-⊔′ m k = suc k ∷ [ m ]
    ... | equal m rewrite ⊔-idem m = [ m ]
    ... | greater m k rewrite +-distribˡ-⊔′ m k = suc k ∷ [ m ]
    ⪾ {q₁} {q₂} l₁@([ o₁ ]) l₂@(h₂ ∷ t₂) with q₂ | compare q₁ q₂
    ... | ŋl | less m k rewrite +-distribʳ-⊔″ m k = {! (ŋl ∸ (ŋ (⪾ l₁ t₂))) ∷ ⪾ l₁ t₂ !}
    ... | ŋl | equal m rewrite ⊔-idem m = {! l₂  !}
    ... | ŋl | greater m k rewrite +-distribˡ-⊔′ m k = {! suc k ∷ l₂ !}
    ⪾ {q₁} {q₂} l₁@(h₁ ∷ t₁) l₂@([ o₂ ]) with q₁ | compare q₁ q₂
    ... | ŋl | less m k rewrite +-distribʳ-⊔′ m k = {! suc k ∷ l₁ !}
    ... | ŋl | equal m rewrite ⊔-idem m = {! l₁  !}
    ... | ŋl | greater m k rewrite +-distribˡ-⊔″ m k = {! (ŋl ∸ (ŋ (⪾ t₁ l₂))) ∷ ⪾ t₁ l₂ !}
    ⪾ {q₁} {q₂} l₁@(h₁ ∷ t₁) l₂@(h₂ ∷ t₂) with q₁ | q₂ | compare q₁ q₂
    ... | ŋl₁ | ŋl₂ | less m k rewrite +-distribʳ-⊔″ m k = {! (ŋl₂ ∸ ŋ (⪾ l₁ t₂)) ∷ ⪾ l₁ t₂ !}
    ... | ŋl₁ | ŋl₂ | equal m rewrite ⊔-idem m = {! (m ∸ ŋ (⪾ t₁ t₂)) ∷ ⪾ t₁ t₂ !}
    ... | ŋl₁ | ŋl₂ | greater m k rewrite +-distribˡ-⊔″ m k = {! (ŋl₁ ∸ ŋ (⪾ t₁ l₂)) ∷ ⪾ t₁ l₂ !}
    -}
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190319/ff2f1738/attachment.sig>