michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean/run): define subterm relation for vectors

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-15 16:17:51 -08:00
parent ea640257bf
commit 1b95b69251
1 changed files with 47 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
tests/lean/run/vector_subterm_pred.lean Normal file
View file

@ -0,0 +1,47 @@
import logic data.nat.basic data.sigma
open nat eq.ops sigma
inductive vector (A : Type) : nat → Type :=
nil : vector A zero,
cons : A → (Π{n}, vector A n → vector A (succ n))
namespace vector
definition vec (A : Type) : Type := Σ n : nat, vector A n
definition to_vec {A : Type} {n : nat} (v : vector A n) : vec A := dpair n v
inductive direct_subterm (A : Type) : vec A → vec A → Prop :=
cons : Π (n : nat) (a : A) (v : vector A n), direct_subterm A (to_vec v) (to_vec (cons a v))
definition direct_subterm.wf (A : Type) : well_founded (direct_subterm A) :=
well_founded.intro (λ (bv : vec A),
sigma.rec_on bv (λ (n : nat) (v : vector A n),
vector.rec_on v
(show acc (direct_subterm A) (to_vec (nil A)), from
acc.intro (to_vec (nil A)) (λ (v₂ : vec A) (H : direct_subterm A v₂ (to_vec (nil A))),
have gen : ∀ (bv : vec A) (H : direct_subterm A v₂ bv) (Heq : bv = (to_vec (nil A))), acc (direct_subterm A) v₂, from
λ bv H, direct_subterm.induction_on H (λ n₁ a₁ v₁ e,
have e₁ : succ n₁ = zero, from sigma.no_confusion e (λ e₁ e₂, e₁),
nat.no_confusion e₁),
gen (to_vec (nil A)) H rfl))
(λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (ih : acc (direct_subterm A) (to_vec v₁)),
acc.intro (to_vec (cons a₁ v₁)) (λ (w₁ : vec A) (lt₁ : direct_subterm A w₁ (to_vec (cons a₁ v₁))),
have gen : ∀ (bv : vec A) (H : direct_subterm A w₁ bv) (Heq : bv = (to_vec (cons a₁ v₁))), acc (direct_subterm A) w₁, from
λ bv H, direct_subterm.induction_on H (λ n₂ a₂ v₂ e,
sigma.no_confusion e (λ (e₁ : succ n₂ = succ n₁) (e₂ : @cons A a₂ n₂ v₂ == @cons A a₁ n₁ v₁),
nat.no_confusion e₁ (λ (e₃ : n₂ = n₁),
have gen₂ : ∀ (m : nat) (Heq₁ : n₂ = m) (v : vector A m) (ih : acc (direct_subterm A) (to_vec v))
(Heq₂ : @cons A a₂ n₂ v₂ == @cons A a₁ m v), acc (direct_subterm A) (to_vec v₂), from
λ m Heq₁, eq.rec_on Heq₁ (λ (v : vector A n₂) (ih : acc (direct_subterm A) (to_vec v)) (Heq₂ : @cons A a₂ n₂ v₂ == @cons A a₁ n₂ v),
vector.no_confusion (heq.to_eq Heq₂) (λ (e₄ : a₂ = a₁) (e₅ : n₂ = n₂) (e₆ : v₂ == v),
eq.rec_on (heq.to_eq (heq.symm e₆)) ih)),
gen₂ n₁ e₃ v₁ ih e₂))),
gen (to_vec (cons a₁ v₁)) lt₁ rfl))))
definition subterm (A : Type) := tc (direct_subterm A)
definition subterm.wf (A : Type) : well_founded (subterm A) :=
tc.wf (direct_subterm.wf A)
end vector