From 1b95b692516b1cdd9adae8f4f3301a806c0fd3b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Nov 2014 16:17:51 -0800 Subject: [PATCH] test(tests/lean/run): define subterm relation for vectors --- tests/lean/run/vector_subterm_pred.lean | 47 +++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 tests/lean/run/vector_subterm_pred.lean diff --git a/tests/lean/run/vector_subterm_pred.lean b/tests/lean/run/vector_subterm_pred.lean new file mode 100644 index 000000000..0d75d09e9 --- /dev/null +++ b/tests/lean/run/vector_subterm_pred.lean @@ -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