test(tests/lean/run): try different ways to pack mutually recursive datatypes

tests/lean/run/forest2.lean

@@ -0,0 +1,51 @@
+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
+
+namespace solution1
+
+inductive tree_forest (A : Type) :=
+of_tree   : tree A   → tree_forest A,
+of_forest : forest A → tree_forest A
+
+inductive same_kind {A : Type} : tree_forest A → tree_forest A → Type :=
+is_tree   : Π (t₁ t₂ : tree A),   same_kind (tree_forest.of_tree t₁)   (tree_forest.of_tree t₂),
+is_forest : Π (f₁ f₂ : forest A), same_kind (tree_forest.of_forest f₁) (tree_forest.of_forest f₂)
+
+definition to_tree {A : Type} (tf : tree_forest A) (t : tree A) : same_kind tf (tree_forest.of_tree t) → tree A :=
+tree_forest.cases_on tf
+  (λ t₁ H, t₁)
+  (λ f₁ H, by cases H)
+
+end solution1
+
+namespace solution2
+
+variables {A B : Type}
+
+inductive same_kind : sum A B → sum A B → Prop :=
+isl : Π (a₁ a₂ : A), same_kind (sum.inl B a₁) (sum.inl B a₂),
+isr : Π (b₁ b₂ : B), same_kind (sum.inr A b₁) (sum.inr A b₂)
+
+definition to_left (s : sum A B) (a : A) : same_kind s (sum.inl B a) → A :=
+sum.cases_on s
+  (λ a₁ H, a₁)
+  (λ b₁ H, false.rec _ (by cases H))
+
+definition to_right (s : sum A B) (b : B) : same_kind s (sum.inr A b) → B :=
+sum.cases_on s
+  (λ a₁ H, false.rec _ (by cases H))
+  (λ b₁ H, b₁)
+
+theorem to_left_inl (a₁ a₂ : A) (H : same_kind (sum.inl B a₁) (sum.inl B a₂)) : to_left (sum.inl B a₁) a₂ H = a₁ :=
+rfl
+
+theorem to_right_inr (b₁ b₂ : B) (H : same_kind (sum.inr A b₁) (sum.inr A b₂)) : to_right (sum.inr A b₁) b₂ H = b₁ :=
+rfl
+
+end solution2