From e499f8e20acc01f503e04a1baad7d933da36973f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Nov 2014 09:36:54 -0800
Subject: [PATCH] feat(kernel/inductive): relax conditions for an inductive
 datatype in Prop to be able to eliminate into Type

The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.

See justification in the new comments at inductive.cpp
---
 src/kernel/inductive/inductive.cpp | 24 ++++++++++++++++++++----
 tests/lean/acc.lean                |  6 ++++++
 tests/lean/acc.lean.expected.out   |  4 ++++
 tests/lua/ac.lua                   |  2 +-
 4 files changed, 31 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/acc.lean
 create mode 100644 tests/lean/acc.lean.expected.out

diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 6854abb5a..21693824a 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -484,19 +484,35 @@ struct add_inductive_fn {
             return false;
         }
         // We have only one introduction rule, the final check is, the type of each argument
-        // that is not a parameter must live in Type.{0}.
+        // that is not a parameter:
+        //  1- It must live in Type.{0}, *OR*
+        //  2- It must occur in the return type. (this is essentially what is called a non-uniform parameter in Coq).
+        //     We can justify 2 by observing that this information is not a *secret* it is part of the type.
+        //     By eliminating to a non-proposition, we would not be revealing anything that is not already known.
         auto ir    = head(inductive_decl_intros(head(m_decls)));
         expr t     = intro_rule_type(ir);
         unsigned i = 0;
+        buffer<expr> to_check; // arguments that we must check if occur in the result type
         while (is_pi(t)) {
+            expr local = mk_local_for(t);
             if (i >= m_num_params) {
                 expr s = ensure_type(binding_domain(t));
-                if (!is_zero(sort_level(s)))
-                    return true;
+                if (!is_zero(sort_level(s))) {
+                    // Current argument is not in Type.{0} (i.e., condition 1 failed).
+                    // We save it in to_check to be able to try condition 2 above.
+                    to_check.push_back(local);
+                }
             }
-            t = instantiate(binding_body(t), mk_local_for(t));
+            t = instantiate(binding_body(t), local);
             i++;
         }
+        buffer<expr> result_args;
+        get_app_args(t, result_args);
+        // Check condition 2: every argument in to_check must occur in result_args
+        for (expr const & arg : to_check) {
+            if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())
+                return true; // condition 2 failed
+        }
         return false;
     }
 
diff --git a/tests/lean/acc.lean b/tests/lean/acc.lean
new file mode 100644
index 000000000..eb4fe2db0
--- /dev/null
+++ b/tests/lean/acc.lean
@@ -0,0 +1,6 @@
+import logic
+
+inductive acc (A : Type) (R : A → A → Prop) :  A → Prop :=
+intro : ∀ (x : A), (∀ (y : A), R y x → acc A R y) → acc A R x
+
+check @acc.rec
diff --git a/tests/lean/acc.lean.expected.out b/tests/lean/acc.lean.expected.out
new file mode 100644
index 000000000..6fabcafe2
--- /dev/null
+++ b/tests/lean/acc.lean.expected.out
@@ -0,0 +1,4 @@
+acc.rec :
+  Π {A : Type} {R : A → A → Prop} {C : A → Type},
+    (Π (x : A), (∀ (y : A), R y x → acc A R y) → (Π (y : A), R y x → C y) → C x) →
+    (Π {a : A}, acc A R a → C a)
diff --git a/tests/lua/ac.lua b/tests/lua/ac.lua
index e5b7852b2..adba24d30 100644
--- a/tests/lua/ac.lua
+++ b/tests/lua/ac.lua
@@ -14,4 +14,4 @@ function display_type(env, t)
    print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))
 end
 
-display_type(env, Const({"Acc", "rec"}, {1}))
+display_type(env, Const({"Acc", "rec"}, {0, 1}))