lean2/tests/lean/run/forest.lean
Leonardo de Moura e65b5884e5 test(tests/lean/run/forest): define brec_on for forests
Almost everything explicit to get an idea of what needs to be generated automatically.
2014-11-11 13:16:23 -08:00

108 lines
4.4 KiB
Text

import data.prod data.unit
open prod
inductive tree (A : Type) : Type :=
node : A → forest A → tree A
with forest : Type :=
nil : forest A,
cons : tree A → forest A → forest A
definition tree.below.{l₁ l₂}
(A : Type.{l₁})
(C₁ : tree A → Type.{l₂})
(C₂ : forest A → Type.{l₂})
(t : tree A) : Type.{max 1 l₂} :=
@tree.rec_on A
(λ t : tree A, Type.{max 1 l₂})
(λ t : forest A, Type.{max 1 l₂})
t
(λ (a : A) (f : forest A) (r : Type.{max 1 l₂}), prod.{l₂ (max 1 l₂)} (C₂ f) r)
unit.{max 1 l₂}
(λ (t : tree A) (f : forest A) (rt : Type.{max 1 l₂}) (rf : Type.{max 1 l₂}),
prod.{(max 1 l₂) (max 1 l₂)} (prod.{l₂ (max 1 l₂)} (C₁ t) rt) (prod.{l₂ (max 1 l₂)} (C₂ f) rf))
definition forest.below.{l₁ l₂}
(A : Type.{l₁})
(C₁ : tree A → Type.{l₂})
(C₂ : forest A → Type.{l₂})
(f : forest A) : Type.{max 1 l₂} :=
@forest.rec_on A
(λ t : tree A, Type.{max 1 l₂})
(λ t : forest A, Type.{max 1 l₂})
f
(λ (a : A) (f : forest A) (r : Type.{max 1 l₂}), prod.{l₂ (max 1 l₂)} (C₂ f) r)
unit.{max 1 l₂}
(λ (t : tree A) (f : forest A) (rt : Type.{max 1 l₂}) (rf : Type.{max 1 l₂}),
prod.{(max 1 l₂) (max 1 l₂)} (prod.{l₂ (max 1 l₂)} (C₁ t) rt) (prod.{l₂ (max 1 l₂)} (C₂ f) rf))
definition tree.brec_on.{l₁ l₂}
(A : Type.{l₁})
(C₁ : tree A → Type.{l₂})
(C₂ : forest A → Type.{l₂})
(t : tree A)
(F₁ : Π (t : tree A), tree.below A C₁ C₂ t → C₁ t)
(F₂ : Π (f : forest A), forest.below A C₁ C₂ f → C₂ f)
: C₁ t :=
have general : prod.{l₂ (max 1 l₂)} (C₁ t) (tree.below A C₁ C₂ t), from
@tree.rec_on
A
(λ (t' : tree A), prod.{l₂ (max 1 l₂)} (C₁ t') (tree.below A C₁ C₂ t'))
(λ (f' : forest A), prod.{l₂ (max 1 l₂)} (C₂ f') (forest.below A C₁ C₂ f'))
t
(λ (a : A) (f : forest A) (r : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f)),
have b : tree.below A C₁ C₂ (tree.node a f), from
r,
have c : C₁ (tree.node a f), from
F₁ (tree.node a f) b,
prod.mk.{l₂ (max 1 l₂)} c b)
(have b : forest.below A C₁ C₂ (forest.nil A), from
unit.star.{max 1 l₂},
have c : C₂ (forest.nil A), from
F₂ (forest.nil A) b,
prod.mk.{l₂ (max 1 l₂)} c b)
(λ (t : tree A)
(f : forest A)
(rt : prod.{l₂ (max 1 l₂)} (C₁ t) (tree.below A C₁ C₂ t))
(rf : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f)),
have b : forest.below A C₁ C₂ (forest.cons t f), from
prod.mk.{(max 1 l₂) (max 1 l₂)} rt rf,
have c : C₂ (forest.cons t f), from
F₂ (forest.cons t f) b,
prod.mk.{l₂ (max 1 l₂)} c b),
pr₁ general
definition forest.brec_on.{l₁ l₂}
(A : Type.{l₁})
(C₁ : tree A → Type.{l₂})
(C₂ : forest A → Type.{l₂})
(f : forest A)
(F₁ : Π (t : tree A), tree.below A C₁ C₂ t → C₁ t)
(F₂ : Π (f : forest A), forest.below A C₁ C₂ f → C₂ f)
: C₂ f :=
have general : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f), from
@forest.rec_on
A
(λ (t' : tree A), prod.{l₂ (max 1 l₂)} (C₁ t') (tree.below A C₁ C₂ t'))
(λ (f' : forest A), prod.{l₂ (max 1 l₂)} (C₂ f') (forest.below A C₁ C₂ f'))
f
(λ (a : A) (f : forest A) (r : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f)),
have b : tree.below A C₁ C₂ (tree.node a f), from
r,
have c : C₁ (tree.node a f), from
F₁ (tree.node a f) b,
prod.mk.{l₂ (max 1 l₂)} c b)
(have b : forest.below A C₁ C₂ (forest.nil A), from
unit.star.{max 1 l₂},
have c : C₂ (forest.nil A), from
F₂ (forest.nil A) b,
prod.mk.{l₂ (max 1 l₂)} c b)
(λ (t : tree A)
(f : forest A)
(rt : prod.{l₂ (max 1 l₂)} (C₁ t) (tree.below A C₁ C₂ t))
(rf : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f)),
have b : forest.below A C₁ C₂ (forest.cons t f), from
prod.mk.{(max 1 l₂) (max 1 l₂)} rt rf,
have c : C₂ (forest.cons t f), from
F₂ (forest.cons t f) b,
prod.mk.{l₂ (max 1 l₂)} c b),
pr₁ general