Skip to content

Instantly share code, notes, and snippets.

@cutsea110
Created July 12, 2015 02:31
Show Gist options
  • Save cutsea110/3510efa866fda3a1306a to your computer and use it in GitHub Desktop.
Save cutsea110/3510efa866fda3a1306a to your computer and use it in GitHub Desktop.
BCoPL theorem 2.5
-- theorem 2.5
associativity-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₁ plus n₂ is n₄ → n₄ plus n₃ is n₅ →
∃ λ n₆ → n₂ plus n₃ is n₆ → n₁ plus n₆ is n₅
associativity-plus {Z} {Z} {Z} {Z} {Z} P-Zero P-Zero = Z , id
associativity-plus {Z} {Z} {Z} {Z} {S n₅} P-Zero ()
associativity-plus {Z} {Z} {n₄ = S n₄} () l₂
associativity-plus {Z} {Z} {S n₃} {Z} {Z} P-Zero ()
associativity-plus {Z} {Z} {S n₃} {Z} {S .n₃} P-Zero P-Zero = S n₃ , id
associativity-plus {Z} {S n₂} {n₄ = Z} () l₂
associativity-plus {Z} {S n₂} {n₄ = S .n₂} {n₅ = Z} P-Zero ()
associativity-plus {Z} {S n₂} {n₄ = S .n₂} {n₅ = S n₅} P-Zero (P-Succ l₂) = S n₅ , const P-Zero
associativity-plus {S n₁} {n₄ = Z} () l₂
associativity-plus {S n₁} {n₄ = S n₄} {n₅ = Z} (P-Succ l₁) ()
associativity-plus {S n₁} {Z} {Z} {S n₄} {S n₅} (P-Succ l₁) (P-Succ l₂) = S n₅ , (λ ())
associativity-plus {S n₁} {Z} {S n₃} {S n₄} {S n₅} (P-Succ l₁) (P-Succ l₂) = Z , (λ ())
associativity-plus {S n₁} {S n₂} {n₄ = S n₄} {n₅ = S n₅} (P-Succ l₁) (P-Succ l₂) = Z , (λ ())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment