33 lines
638 B
Text
33 lines
638 B
Text
|
import data.nat
|
||
|
|
open nat
|
||
|
|
|
||
|
|
inductive Parity : nat → Type :=
|
||
|
|
| even : ∀ n : nat, Parity (2 * n)
|
||
|
|
| odd : ∀ n : nat, Parity (2 * n + 1)
|
||
|
|
|
||
|
|
open Parity
|
||
|
|
|
||
|
|
definition parity : Π (n : nat), Parity n
|
||
|
|
| parity 0 := even 0
|
||
|
|
| parity (n+1) :=
|
||
|
|
begin
|
||
|
|
have aux : Parity n, from parity n,
|
||
|
|
cases aux with (k, k),
|
||
|
|
begin
|
||
|
|
apply (odd k)
|
||
|
|
end,
|
||
|
|
begin
|
||
|
|
change (Parity (2*k + 2*1)),
|
||
|
|
rewrite -mul.left_distrib,
|
||
|
|
apply (even (k+1))
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
print definition parity
|
||
|
|
|
||
|
|
definition half (n : nat) : nat :=
|
||
|
|
match ⟨n, parity n⟩ with
|
||
|
|
| ⟨⌞2 * k⌟, even k⟩ := k
|
||
|
|
| ⟨⌞2 * k + 1⌟, odd k⟩ := k
|
||
|
|
end
|