2014-01-05 18:32:47 +00:00
|
|
|
(*
|
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
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>
2013-12-07 00:14:15 +00:00
|
|
|
-- Define a simple tactic using Lua
|
2013-12-26 23:54:53 +00:00
|
|
|
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
|
2014-01-05 18:32:47 +00:00
|
|
|
*)
|
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
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>
2013-12-07 00:14:15 +00:00
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
|
2014-01-05 19:03:35 +00:00
|
|
|
print Environment 1.
|