You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
apply_instance fails to find an instance, although it finds one for another problem which is defeq to the first one, even with the flag tactic.transparency.instances. MWE, based on mathlib:
import analysis.normed_space.basic
section normed_module
set_option default_priority 100-- see Note [default priority]classnormed_module (α : Type*) (β : Type*) [normed_ring α] [normed_group β]
extends semimodule α β :=
(norm_smul_le : ∀ (a:α) (b:β), ∥a • b∥ ≤ ∥a∥ * ∥b∥)
end normed_module
variables {𝕜 : Type} {n : ℕ} {E : fin n → Type}
[A : normed_field 𝕜] [N : ∀i, normed_group (E i)] [∀i, normed_module 𝕜 (E i)]
-- Two different ways to say: Π (i : fin n), module 𝕜 (E i)set_option trace.class_instances true
lemmaall_right :
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance
lemmafails :
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@comm_ring.to_ring.{0} 𝕜
(@field.to_comm_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A)))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance -- fails-- all_right -- works
The two terms in the two lemmas are defeq with tactic.transparency.instances, and the subterms are also defeq with tactic.transparency.instances, but they are not defeq with tactic.transparency.reducible, as shown by the following:
lemmaouter_works_with_transparency.instances :
(Π (i : fin n),
@module.{0} 𝕜 (E i)
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
(@normed_group.to_add_comm_group.{0} (E i) (N i)))
=
Π (i : fin n),
@module.{0} 𝕜 (E i)
(@comm_ring.to_ring.{0} 𝕜
(@field.to_comm_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A)))
(@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by tactic.reflexivity tactic.transparency.instances -- workslemmainner_works_with_transparency.instances :
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
=
(@comm_ring.to_ring.{0} 𝕜
(@field.to_comm_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A))) :=
by tactic.reflexivity tactic.transparency.instances --workslemmainner_fails_with_transparency.reducible :
(@normed_ring.to_ring.{0} 𝕜
(@normed_field.to_normed_ring.{0} 𝕜 A))
=
(@comm_ring.to_ring.{0} 𝕜
(@field.to_comm_ring.{0} 𝕜
(@normed_field.to_field.{0} 𝕜 A))) :=
by tactic.reflexivity tactic.transparency.reducible -- fails
I'm pretty sure this is a unification problem and not a transparency issue. During type class search we need to unify the instance with the goal, this is much harder than checking definitional equality of terms without metavariables.
I just stumbled on the same issue (with pretty complicated pi types, again). Is there hope that #300 could change something here? (It involves pi types and instance search and reducibility flags, so from a distance it sounds similar, but the details look rather different).
apply_instance
fails to find an instance, although it finds one for another problem which is defeq to the first one, even with the flagtactic.transparency.instances
. MWE, based on mathlib:The two terms in the two lemmas are defeq with
tactic.transparency.instances
, and the subterms are also defeq withtactic.transparency.instances
, but they are not defeq withtactic.transparency.reducible
, as shown by the following:Mario's guess on Zulip is that
apply_instance
probably passes the wrong flag to subproblems (see discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Normed.20spaces/near/197786186)Tested on Lean 3.11 and 3.13.1
(Example edited for 3.16.0)
The text was updated successfully, but these errors were encountered: