48 lines
1.7 KiB
Text
48 lines
1.7 KiB
Text
import logic data.nat.basic data.prod data.unit
|
||
open nat prod
|
||
|
||
inductive vector (A : Type) : nat → Type :=
|
||
vnil : vector A zero,
|
||
vcons : Π {n : nat}, A → vector A n → vector A (succ n)
|
||
|
||
namespace vector
|
||
print definition no_confusion
|
||
|
||
theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
|
||
begin
|
||
intro h, apply (no_confusion h), intros, assumption
|
||
end
|
||
|
||
theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ :=
|
||
begin
|
||
intro h, apply heq.to_eq, apply (no_confusion h), intros, eassumption,
|
||
end
|
||
|
||
section
|
||
universe variables l₁ l₂
|
||
variable {A : Type.{l₁}}
|
||
variable C : Π (n : nat), vector A n → Type.{l₂}
|
||
definition below {n : nat} (v : vector A n) :=
|
||
rec_on v unit.{max 1 l₂} (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : Type.{max 1 l₂}), C n₁ v₁ × r₁)
|
||
end
|
||
|
||
section
|
||
universe variables l₁ l₂
|
||
variable {A : Type.{l₁}}
|
||
variable {C : Π (n : nat), vector A n → Type.{l₂}}
|
||
definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), below C v → C n v) : C n v :=
|
||
have general : C n v × below C v, from
|
||
rec_on v
|
||
(pair (H zero (vnil A) unit.star) unit.star)
|
||
(λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × below C v₁),
|
||
have b : below C (vcons a₁ v₁), from
|
||
r₁,
|
||
have c : C (succ n₁) (vcons a₁ v₁), from
|
||
H (succ n₁) (vcons a₁ v₁) b,
|
||
pair c b),
|
||
pr₁ general
|
||
end
|
||
|
||
check brec_on
|
||
|
||
end vector
|