test(tests/lean/extra): more tests for equations compiler

tests/lean/extra/denote_rec.lean

@@ -0,0 +1,27 @@
+inductive formula :=
+eqf : nat → nat → formula,
+andf : formula → formula → formula,
+impf : formula → formula → formula,
+allf : (nat → formula) → formula
+
+check @formula.rec_on
+
+namespace formula
+
+  definition denote : formula → Prop,
+  denote (eqf n1 n2)  := n1 = n2,
+  denote (andf f1 f2) := denote f1 ∧ denote f2,
+  denote (impf f1 f2) := denote f1 → denote f2,
+  denote (allf f)     := ∀ n : nat, denote (f n)
+
+end formula
+
+definition denote (f : formula) : Prop :=
+formula.rec_on f
+  (λ n₁ n₂, n₁ = n₂)
+  (λ f₁ f₂ r₁ r₂, r₁ ∧ r₂)
+  (λ f₁ f₂ r₁ r₂, r₁ → r₂)
+  (λ f r, ∀ n : nat, r n)
+
+open formula
+eval denote (allf (λ n₁, allf (λ n₂, impf (eqf n₁ n₂) (eqf n₂ n₁))))

tests/lean/extra/lt_rec.lean

@@ -0,0 +1,16 @@
+open nat
+
+set_option pp.implicit true
+set_option pp.notation false
+
+definition lt_trans : ∀ {a b c : nat}, a < b → b < c → a < c,
+lt_trans h  (lt.base _)   := lt.step h,
+lt_trans h₁ (lt.step h₂)  := lt.step (lt_trans h₁ h₂)
+
+definition lt_succ : ∀ {a b : nat}, a < b → succ a < succ b,
+lt_succ (lt.base a)  := lt.base (succ a),
+lt_succ (lt.step h)  := lt.step (lt_succ h)
+
+definition lt_of_succ : ∀ {a b : nat}, succ a < b → a < b,
+lt_of_succ (lt.base (succ a)) := lt.trans (lt.base a) (lt.base (succ a)),
+lt_of_succ (lt.step h₂)       := lt.step (lt_of_succ h₂)

tests/lean/extra/tree_list_rec.lean

@@ -0,0 +1,29 @@
+open nat
+
+inductive tree (A : Type) :=
+leaf : A → tree A,
+node : tree_list A → tree A
+with tree_list :=
+nil  : tree_list A,
+cons : tree A → tree_list A → tree_list A
+
+namespace tree
+open tree_list
+
+definition size {A : Type} : tree A → nat
+with size_l                : tree_list A → nat,
+size (leaf a)     := 1,
+size (node l)     := size_l l,
+size_l !nil       := 0,
+size_l (cons t l) := size t + size_l l
+
+definition eq_tree {A : Type} : tree A → tree A → Prop
+with eq_tree_list             : tree_list A → tree_list A → Prop,
+eq_tree (leaf a₁) (leaf a₂)            := a₁ = a₂,
+eq_tree (node l₁) (node l₂)            := eq_tree_list l₁ l₂,
+eq_tree _ _                            := false,
+eq_tree_list !nil !nil                 := true,
+eq_tree_list (cons t₁ l₁) (cons t₂ l₂) := eq_tree t₁ t₂ ∧ eq_tree_list l₁ l₂,
+eq_tree_list _ _                       := false
+
+end tree