Context
I have defined two structures corresponding to a group and a subgroup :
structure groupe : Type (u+1) :=
(ens : Type u)
(mul : ens → ens → ens)
-- other things
structure sous_groupe (G : groupe) :=
(sous_ensemble : set G.ens)
-- other things
I then defined coercions from a group G to the carrier type, and from a subgroup H of G to the underlying group with the carrier type being {a : G.ens // a ∈ H.sous_ens}:
instance groupe_to_ens : has_coe_to_sort groupe (Type u) :=
⟨λ G : groupe, G.ens⟩
instance sous_groupe_to_groupe {G: groupe} : has_coe (sous_groupe G) groupe :=
sorry -- definition of the subtype and the corresponding functions and axioms
Problem
Now what I tried to to is :
example (G: groupe) (H : sous_groupe G) (a : G) (b : H): G.ens := G.mul a b
What I expected for it to do is for b to be coerced by H --> x : group --> x.ens (which equals {a : G.ens // a ∈ H.sous_ens}) --> G.ens).
But I got this error:
type mismatch at application
G.mul a b
term
b
has type
@coe_sort.{u+1 u+2} (sous_groupe G) (Type u) (@coe_sort_trans.{u+2 u+1 u+2} (sous_groupe G) groupe (Type u) groupe_to_ens (@coe_base_aux.{u+1 u+2} (sous_groupe G) groupe (@sous_groupe_to_groupe G))) H
I tried to do #reduce [the big expression for the type of b in the error] and it reduced to {a : G.ens // H.sous_ens a} so it seems to have been coerced all the way up to the subtype, but it did not do the final coercion from the subtype to the corresponding type.
I also tried to do this:
variable (a : G)
variable (b : {t // H.sous_ens t})
variable (c : [the big expression that reduces to {t // H.sous_ens t})
example : G.ens := G.mul a b -- This works correctly and b is coerced to G.ens
example : G.ens := G.mul a c -- This fails even though c is definitionally equal to b
Full block of code to reproduce the error
section
universe u
structure groupe : Type (u+1) :=
(ens : Type u)
(mul : ens → ens → ens )
(neutre : ens)
(inv : ens → ens )
(mul_assoc : ∀ a b c : ens, mul (mul a b) c = mul a (mul b c))
(neutre_gauche : ∀ x : ens, mul neutre x = x)
(inv_gauche : ∀ x : ens, mul (inv x) x = neutre)
instance groupe_to_ens : has_coe_to_sort groupe (Type u) :=
⟨λ a : groupe, a.ens⟩
instance groupe_has_inv (G: groupe) :
has_inv (G.ens) := ⟨G.inv⟩
instance groupe_has_mul (G : groupe) :
has_mul (G.ens) := ⟨G.mul⟩
structure sous_groupe (G: groupe) :=
(sous_ens : set G.ens)
(mul_stab : ∀ a b ∈ sous_ens, G.mul a b ∈ sous_ens)
(inv_stab : ∀ a ∈ sous_ens, a⁻¹ ∈ sous_ens)
(contient_neutre : G.neutre ∈ sous_ens )
instance sous_groupe_to_groupe {G: groupe}:
has_coe (sous_groupe G) groupe :=
⟨λ SG : sous_groupe G,
{groupe .
ens := {a // a ∈ SG.sous_ens},
mul := λ x y, ⟨x.val*y.val, SG.mul_stab x.val x.property y.val y.property⟩,
inv := λ x, ⟨x.val⁻¹, SG.inv_stab x.val x.property⟩,
neutre := ⟨G.neutre, SG.contient_neutre⟩,
mul_assoc := λ x y z, by {rw subtype.mk.inj_eq, unfold subtype.val, exact G.mul_assoc x y z},
neutre_gauche := λ x, by {cases x, rw subtype.mk.inj_eq, unfold subtype.val, exact G.neutre_gauche _},
inv_gauche := λ x, by {rw subtype.mk.inj_eq, unfold subtype.val, exact G.inv_gauche x.val},
}⟩
section
variable (G: groupe)
variable (H: sous_groupe G)
variable (a : G)
variable (a' : H)
variable (b : {c // H.sous_ens c})
variable (b' : (@coe_sort.{u+1 u+2} (sous_groupe G) (Type u)
(@coe_sort_trans.{u+2 u+1 u+2} (sous_groupe G) groupe (Type u) groupe_to_ens
(@coe_base_aux.{u+1 u+2} (sous_groupe G) groupe (@sous_groupe_to_groupe G)))
H))
#reduce (@coe_sort.{u+1 u+2} (sous_groupe G) (Type u)
(@coe_sort_trans.{u+2 u+1 u+2} (sous_groupe G) groupe (Type u) groupe_to_ens
(@coe_base_aux.{u+1 u+2} (sous_groupe G) groupe (@sous_groupe_to_groupe G)))
H) -- infered type, reduces to {a // H.sous_ens a}
set_option pp.all true
#reduce G.mul a a' -- does not work, the infered type for a' is the type of b'
#reduce G.mul a b -- works
#reduce G.mul a b' -- does not work
end
end
Is there anything in the coercion mechanisms that would explain this behaviour ?
