$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/11/02

### Chain Reasoning

lemma : {n₁ n₂ n₃ : Nat} ->
suc (parity p + (n₁ + n₂) + n₃) ≡ parity p + n₁ + suc (n₂ + n₃)
lemma {n₁} {n₂} {n₃} =
chain> suc (parity p + (n₁ + n₂) + n₃)
=== suc (parity p + (n₁ + n₂ + n₃))
by cong suc (sym (+assoc (parity p) (n₁ + n₂) n₃))
=== parity p + suc (n₁ + n₂ + n₃)
by sym (+suc (parity p) (n₁ + n₂ + n₃))
=== parity p + (n₁ + suc (n₂ + n₃)) by cong (\x -> parity p + x)
( chain> suc (n₁ + n₂ + n₃)
=== suc (n₁ + (n₂ + n₃)) by cong suc (sym (+assoc n₁ n₂ n₃))
=== n₁ + suc (n₂ + n₃) by sym (+suc n₁ (n₂ + n₃)) )
=== parity p + n₁ + suc (n₂ + n₃)
by +assoc (parity p) n₁ (suc (n₂ + n₃))


chain> suc (parity p + (n₁ + n₂) + n₃)
=== [ cong suc (sym (+assoc (parity p) (n₁ + n₂) n₃)) ]
suc (parity p + (n₁ + n₂ + n₃))
=== ...


data Indeed {A : Set} : A -> Set where
indeed : (x : A) -> Indeed x

[_ : {A : Set}{x y : A} -> x == y -> Indeed y -> x == y
[ eq = \_ -> eq

]_ : {A : Set} -> (y : A) -> Indeed y
] y = indeed y


--

half : (n : Nat) -> (Nat ⋮ \m -> n ≡ m + m) \/
(Nat ⋮ \m -> n ≡ 1 + (m + m))
...
half (suc n) | \/-IR (sub m p) = \/-IL (sub (1 + m) (proof n m p))
where
proof : (n : Nat) -> (m : Nat) ->
(n ≡ 1 + (m + m)) -> (1 + n ≡ (1 + m) + (1 + m))
proof n m p =
chain> 1 + n
=== 1 + (1 + m + m) by cong suc p
=== (1 + m) + (1 + m) by sym (+suc (1 + m) m)


--

Labels: ,