From 463e70332de6f38db8688c7df6f0682ee0e7a718 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Nov 2014 10:46:22 -0800
Subject: [PATCH] test(tests/lean/run): define brec_on and binduction_on for a
 reflexive type

We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.

For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.

We workaround this issue by defining two versions of brec_on:
  - One (brec_on) that eliminates to Type.{>=1}, and
  - binduction_on that eliminates to Prop.

For non-reflexive types, we can combine both of them.
---
 tests/lean/run/ftree_brec.lean | 109 +++++++++++++++++++++++++++++++++
 1 file changed, 109 insertions(+)
 create mode 100644 tests/lean/run/ftree_brec.lean

diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean
new file mode 100644
index 000000000..2be3c8aa8
--- /dev/null
+++ b/tests/lean/run/ftree_brec.lean
@@ -0,0 +1,109 @@
+import data.unit data.prod
+
+inductive ftree (A : Type) (B : Type) : Type :=
+leafa : ftree A B,
+node  : (A → B → ftree A B) → (B → ftree A B) → ftree A B
+
+namespace ftree
+
+definition below.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B → Type.{l+1}) (t : ftree A B)
+           : Type.{max l₁ l₂ (l+1)} :=
+@rec.{(max l₁ l₂ (l+1))+1 l₁ l₂}
+  A
+  B
+  (λ t : ftree A B,  Type.{max l₁ l₂ (l+1)})
+  unit.{max l₁ l₂ (l+1)}
+  (λ (f₁ : A → B → ftree A B)
+     (f₂ : B → ftree A B)
+     (r₁ : Π (a : A) (b : B), Type.{max l₁ l₂ (l+1)})
+     (r₂ : Π (b : B),         Type.{max l₁ l₂ (l+1)}),
+     let fc₁ : Type.{max l₁ l₂ (l+1)} := Π (a : A) (b : B), C (f₁ a b) in
+     let fc₂ : Type.{max l₂ l+1}      := Π (b : B), C (f₂ b) in
+     let fr₁ : Type.{max l₁ l₂ (l+1)} := Π (a : A) (b : B), r₁ a b in
+     let fr₂ : Type.{max l₁ l₂ (l+1)} := Π (b : B), r₂ b in
+     let p₁  : Type.{max l₁ l₂ (l+1)} := prod.{(max l₁ l₂ (l+1)) (max l₁ l₂ (l+1))} fc₁ fr₁ in
+     let p₂  : Type.{max l₁ l₂ (l+1)} := prod.{(max l₂ (l+1)) (max l₁ l₂ (l+1))} fc₂ fr₂ in
+     prod.{(max l₁ l₂ (l+1)) (max l₁ l₂ (l+1))} p₁ p₂)
+  t
+
+definition pbelow.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A B → Prop) (t : ftree A B)
+           : Prop :=
+@rec.{1 l₁ l₂}
+  A
+  B
+  (λ t : ftree A B,  Prop)
+  true
+  (λ (f₁ : A → B → ftree A B)
+     (f₂ : B → ftree A B)
+     (r₁ : Π (a : A) (b : B), Prop)
+     (r₂ : Π (b : B),         Prop),
+     let fc₁ : Prop := ∀ (a : A) (b : B), C (f₁ a b) in
+     let fc₂ : Prop := ∀ (b : B), C (f₂ b) in
+     let fr₁ : Prop := ∀ (a : A) (b : B), r₁ a b in
+     let fr₂ : Prop := ∀ (b : B), r₂ b in
+     let p₁  : Prop := fc₁ ∧ fr₁ in
+     let p₂  : Prop := fc₂ ∧ fr₂ in
+     p₁ ∧ p₂)
+  t
+
+definition brec_on.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree A B → Type.{l+1}}
+                  (t : ftree A B)
+                  (F : Π (t : ftree A B), below C t → C t)
+              : C t :=
+have gen : prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (below C t), from
+  @rec.{(max l₁ l₂ (l+1)) l₁ l₂}
+    A
+    B
+    (λ t : ftree A B, prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (below C t))
+    (have b : below C (leafa A B), from
+       unit.star.{max l₁ l₂ (l+1)},
+     have c : C (leafa A B), from
+       F (leafa A B) b,
+     prod.mk.{(l+1) (max l₁ l₂ (l+1))} c b)
+    (λ (f₁ : A → B → ftree A B)
+       (f₂ : B → ftree A B)
+       (r₁ : Π (a : A) (b : B), prod.{(l+1) (max l₁ l₂ (l+1))} (C (f₁ a b)) (below C (f₁ a b)))
+       (r₂ : Π (b : B), prod.{(l+1) (max l₁ l₂ (l+1))} (C (f₂ b)) (below C (f₂ b))),
+       let fc₁ : Π (a : A) (b : B), C (f₁ a b)       := λ (a : A) (b : B), prod.pr1 (r₁ a b) in
+       let fr₁ : Π (a : A) (b : B), below C (f₁ a b) := λ (a : A) (b : B), prod.pr2 (r₁ a b) in
+       let fc₂ : Π (b : B), C (f₂ b)                 := λ (b : B), prod.pr1 (r₂ b) in
+       let fr₂ : Π (b : B), below C (f₂ b)           := λ (b : B), prod.pr2 (r₂ b) in
+       have b : below C (node f₁ f₂), from
+         prod.mk (prod.mk fc₁ fr₁) (prod.mk fc₂ fr₂),
+       have c : C (node f₁ f₂), from
+         F (node f₁ f₂) b,
+       prod.mk c b)
+    t,
+prod.pr1 gen
+
+definition binduction_on.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} {C : ftree A B → Prop}
+               (t : ftree A B)
+               (F : Π (t : ftree A B), pbelow C t → C t)
+            : C t :=
+have gen : C t ∧ pbelow C t, from
+  @rec.{0 l₁ l₂}
+    A
+    B
+    (λ t : ftree A B, C t ∧ pbelow C t)
+    (have b : pbelow C (leafa A B), from
+       true.intro,
+     have c : C (leafa A B), from
+       F (leafa A B) b,
+     and.intro c b)
+    (λ (f₁ : A → B → ftree A B)
+       (f₂ : B → ftree A B)
+       (r₁ : ∀ (a : A) (b : B), C (f₁ a b) ∧ pbelow C (f₁ a b))
+       (r₂ : ∀ (b : B), C (f₂ b) ∧ pbelow C (f₂ b)),
+       let fc₁ : ∀ (a : A) (b : B), C (f₁ a b)        := λ (a : A) (b : B), and.elim_left  (r₁ a b) in
+       let fr₁ : ∀ (a : A) (b : B), pbelow C (f₁ a b) := λ (a : A) (b : B), and.elim_right (r₁ a b) in
+       let fc₂ : ∀ (b : B), C (f₂ b)                  := λ (b : B), and.elim_left  (r₂ b) in
+       let fr₂ : ∀ (b : B), pbelow C (f₂ b)           := λ (b : B), and.elim_right (r₂ b) in
+       have b : pbelow C (node f₁ f₂), from
+         and.intro (and.intro fc₁ fr₁) (and.intro fc₂ fr₂),
+       have c : C (node f₁ f₂), from
+         F (node f₁ f₂) b,
+       and.intro c b)
+    t,
+and.elim_left gen
+
+end ftree