how do proofs with \< ... \> work?

Stream: new members

[François Sunatori]

Hi, I'm new to Lean.

I saw some examples where
lemma self_mem_coset (a : G) (H : subgroup G) : a ∈ a ⋆ H := ⟨1, H.one_mem, (group.mul_one a).symm⟩.
I'm unsure how to read this proof.

I know that ⟨..., ...⟩ represents a dependent pair (sigma type) and means that "the type of the second element of the pair, b : β a, depends on the first element of the pair, a : α"
from https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html

What does it translate to in tactics?

Thanks :)

[Adam Topaz]

Can you say where you found that lemma?

[Adam Topaz]

Even better, provide a #mwe

[Adam Topaz]

In any case, the point is that to prove that some element $g$ of a group is a member of a coset associated to $a$, you have to prove that there exists an element $h$ in the subgroup $H$ such that $g = a \cdot h$. In the case $g = a$, you take $h = 1$, so that's the first $1$ appearing there. The H.one_mem is the proof that $1$ is an element of $H$ (which is a subgroup of $G$), while group.mul_one a is the proof that $a = a \cdot 1$, while symm means reverse the equality.

[Thomas Browning]

A mwe would be helpful, but here's a guess of a tactic proof:

begin
  use 1,
  exact H.one_mem,
  exact (group.mul_one a).symm,
end

[François Sunatori]

@Adam Topaz I found it here: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/subgroup/basic.lean#L191

[François Sunatori]

but how should I interpret the ⟨..., ...⟩ more generally? Is it just used to sequence terms one after the other? since each spot in the tuple is dependent on the spot before it? (sorry, I don't know if "spot" is the right word to use here)

[Alex J. Best]

Its called an anonymous constructor, see https://leanprover.github.io/reference/declarations.html#structures-and-records

[François Sunatori]

Thanks @Alex J. Best ! That's exactly the info I needed. So does this mean that it doesn't correspond to a term of a sigma type?

[Alex J. Best]

Right, its much more general, you can make terms of sigma types with it like

def t : Σ n, vector ℤ n := ⟨0, vector.nil⟩

but we can also make a term of type vector ℤ 1 with this notation, a vector is a list of a fixed length, so it has one constructor, the list and the proof that it has that length, so this is ⟨[1], by simp⟩ : vector ℤ 1. The fun begins when we can combine these:

def t' : Σ n, vector ℤ n := ⟨1, ⟨[1], by simp⟩⟩
-- we can remove the nesting which is what makes this notation so powerful:
def t'' : Σ n, vector ℤ n := ⟨1, [1], by simp⟩

[Damiano Testa]

Another place where they can occur is in the proof of iff statements. In this case you would have

⟨proof of →, proof of ←⟩

[Kevin Buzzard]

Damiano, you were talking about structures recently -- you can make a term of any structure using this pointy bracket notation. The things in the bracket are the inputs for the constructor.

[Johan Commelin]

@Damiano Testa Note that iff is just a special case of what Alex said! It's also just a structure (-;

[Damiano Testa]

Ah, thanks for the information: I did not know that these were all special cases of the same construction!

[François Sunatori]

In the example shown here https://leanprover.github.io/reference/declarations.html#structures-and-records,
I'm still a little confused as to why ⟨ b₁, b₂, f₁, ..., fₙ ⟩ is equivalent to foo.constructor b₁ b₂ f₁ f₁ ... fₙ.
My understanding is that a structure is a pi-type with type former : foo : Π (a : α), Sort u
Wouldn't a term of the type formed by the structure need to be of a pi-type?
I thought ⟨ ...⟩ meant it's a term of a sigma-type.

Thanks again!
(I managed to translate a few of the proofs done with ⟨ ...⟩ into tactic proofs and am getting a better intuition toward it but I think I haven't yet wrapped my head completely around it)

[Alex J. Best]

The bracket notation is really for any inductive type with only one constructor, check out these examples for instance:

inductive foo
| a : foo
#check (⟨⟩ : foo)

inductive bar
| a : bar → bar
variable (l : bar)
#check (⟨⟨⟨l⟩⟩⟩ : bar)

[Eric Wieser]

I think the confusion comes from families of types, but the notation works in the same way:

inductive foo (n : nat)
| a : foo
#check (⟨⟩ : foo 3)

[François Sunatori]

ok I'm not sure why I was assuming that ⟨ ...⟩ was only for sigma types.
I just looked at the sigma type definition (https://github.com/leanprover/lean/blob/72a965986fa5aeae54062e98efb3140b2c4e79fd/library/init/core.lean#L247):

structure sigma {α : Type u} (β : α → Type v) :=
mk :: (fst : α) (snd : β fst)

and it has only one constructor and if I'm not mistaken a structure is an inductive.
This means we can use the "anonymous constructor" ⟨ ...⟩ to create a term of type sigma.

So if I understood correctly, ⟨ ...⟩ is not specific to sigma types but instead is specific to inductive types.

[Eric Wieser]

*with one constructor

[Eric Wieser]

You can't use it on or, which has two

[François Sunatori]

thanks @Eric Wieser @Alex J. Best you're explanations really helped me understand this :) and thanks everyone else as well for all your clues to help me untangle this!