lean2/tests/lean/interactive/t13.lean

(**
-- 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.
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`
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-26 23:54:53 +00:00			`auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))`
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)`

			`Show Environment 1.`