From 015bff82835f9ed3982859c450abee2667d49bf0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Dec 2013 16:14:15 -0800
Subject: [PATCH] fix(library/tactic/goal): to_goal way of handling
 context_entries of the form (name, domain, body) where domain is null, and
 body is a proof term
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This commit fixes a problem exposed by t13.lean.
It has a theorem of the form:

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form

 [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A

The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type).
Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions.
Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created
     A : Bool, B : Bool, assumption : A /\ B |- B /\ A
That is, the lemmas are not available when solving B /\ A.
Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used.

    Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
            let lemma1 := Conjunct1 assumption,
                lemma2 := Conjunct2 assumption
            in Conj (Conjunct2 assumption) (Conjunct1 assumption)

This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal
     A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A

After this commit, the proof for theorem T1 is

Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
    let lemma1 := Conjunct1 assumption,
        lemma2 := Conjunct2 assumption
    in Conj lemma2 lemma1

as expected.

Finally, this example suggests that the encoding

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 : A := (by auto),
              lemma2 : B := (by auto)
          in (show B /\ A by auto)

is more efficient than

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/goal.cpp                  |  5 ++++-
 tests/lean/interactive/t13.lean              | 12 ++++++++++++
 tests/lean/interactive/t13.lean.expected.out |  7 +++++++
 3 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/interactive/t13.lean
 create mode 100644 tests/lean/interactive/t13.lean.expected.out

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index 78154fd56..dafa5a665 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -136,8 +136,11 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
         name n = mk_unique_name(used_names, e.get_name());
         expr d = replacer(e.get_domain());
         expr b = replacer(e.get_body());
+        if (b && !d) {
+            d = inferer(b);
+        }
         replacer.clear();
-        if (b && (!d || !inferer.is_proposition(d))) {
+        if (b && !inferer.is_proposition(d)) {
             bodies.push_back(b);
             consts.push_back(expr());
         } else {
diff --git a/tests/lean/interactive/t13.lean b/tests/lean/interactive/t13.lean
new file mode 100644
index 000000000..d1af3886e
--- /dev/null
+++ b/tests/lean/interactive/t13.lean
@@ -0,0 +1,12 @@
+(**
+-- Define a simple tactic using Lua
+auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
+**)
+
+Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
+     fun assumption : A /\ B,
+          let lemma1 := (show A by auto),
+              lemma2 := (show B by auto)
+          in (show B /\ A by auto)
+
+Show Environment 1.
diff --git a/tests/lean/interactive/t13.lean.expected.out b/tests/lean/interactive/t13.lean.expected.out
new file mode 100644
index 000000000..e7a96745f
--- /dev/null
+++ b/tests/lean/interactive/t13.lean.expected.out
@@ -0,0 +1,7 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+  Proved: T1
+Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
+    let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1
+# 
\ No newline at end of file