SHARE
TWEET

Untitled

a guest Feb 21st, 2020 92 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. binom-identity : (a b :) -> (a + b) * (a + b)(a * a) + (b * b) + (2 * a * b)
  2. binom-identity zero b = sym (+-identityʳ (b * b))
  3. binom-identity (suc a) b = begin
  4.                               (1 + a + b) * (1 + a + b)     ≡⟨⟩
  5.     1 +        a + b        + (a + b) * (1 + a + b)         ≡⟨ cong (1 + a + b +_) (*-suc (a + b) (a + b))
  6.     1 +  (a + b) + ((a + b) + ((a + b) * (a + b)))          ≡⟨ cong suc (sym (+-assoc (a + b) (a + b) ((a + b) * (a + b))))
  7.     1 +  (a + b) + (a + b)  + (a + b) * (a + b)             ≡⟨ cong suc (cong (_+ ((a + b) * (a + b))) (+-double-comm a b))
  8.     1 +  (a + a) + (b + b)  + (a + b) * (a + b)             ≡⟨ cong (1 + (a + a) + (b + b) +_) (binom-identity a b)
  9.     1 +  (a + a) + (b + b)  + (a * a + b * b + 2 * a * b)   ≡⟨ cong (1 + (a + a) + (b + b) +_) (+-assoc (a * a) (b * b) (2 * a * b))
  10.     1 +  (a + a) + (b + b)  + (a * a + (b * b + 2 * a * b)) ≡⟨ cong suc (sym (+-assoc (a + a + (b + b)) (a * a) (b * b + 2 * a * b)))
  11.     1 + (((a + a) + (b + b)) + (a * a)) + (b * b + 2 * a * b) ≡⟨ cong suc (cong (_+ (b * b + 2 * a * b)) {!!})
  12.     1 + (((a + a) + a * a) + (b + b)) + (b * b + 2 * a * b)   ≡⟨⟩
  13.     {!!}
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Top