lean2/tests/lean/run/blast_meta_bug.lean

constants {A : Type.{1}} (P : A → Prop) (Q : A → Prop)
definition H [forward] : ∀ a, (: P a :) → Exists Q := sorry

set_option blast.strategy "ematch"

example (a : A) : P a → Exists Q :=
by blast
fix(library/blast/strategies): constructor action was being applied too soon 2015-12-06 03:43:48 +00:00			`constants {A : Type.{1}} (P : A → Prop) (Q : A → Prop)`
feat(library/blast/forward): inst_simp should use the left-hand-side as a pattern (if none is provided by the user) The motivation is to reduce the number of instances generated by ematching. For example, given inv_inv: forall a, (a⁻¹)⁻¹ = a the new heuristic uses ((a⁻¹)⁻¹) as the pattern. This matches the intuition that inv_inv should be used a simplification rule. The default pattern inference procedure would use (a⁻¹). This is bad because it generates an infinite chain of instances whenever there is a term (a⁻¹) in the proof state. By using (a⁻¹), we get (a⁻¹)⁻¹ = a Now that we have (a⁻¹)⁻¹, we can match again and generate ((a⁻¹)⁻¹)⁻¹ = a⁻¹ and so on 2016-01-01 04:20:39 +00:00			`definition H [forward] : ∀ a, (: P a :) → Exists Q := sorry`
fix(library/blast/strategies): constructor action was being applied too soon 2015-12-06 03:43:48 +00:00
chore(tests/lean/run/blast_meta_bug): use "ematch" strategy in the test 2015-12-07 20:23:01 +00:00			`set_option blast.strategy "ematch"`
fix(library/blast/strategies): constructor action was being applied too soon 2015-12-06 03:43:48 +00:00
			`example (a : A) : P a → Exists Q :=`
			`by blast`