Zulip Chat Archive

Stream: new members

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


view this post on Zulip François Sunatori (Jan 22 2021 at 04:37):

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 :)

view this post on Zulip Adam Topaz (Jan 22 2021 at 04:39):

Can you say where you found that lemma?

view this post on Zulip Adam Topaz (Jan 22 2021 at 04:40):

Even better, provide a #mwe

view this post on Zulip Adam Topaz (Jan 22 2021 at 04:42):

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

view this post on Zulip Thomas Browning (Jan 22 2021 at 04:42):

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

view this post on Zulip François Sunatori (Jan 22 2021 at 04:46):

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

view this post on Zulip François Sunatori (Jan 22 2021 at 04:48):

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)

view this post on Zulip Alex J. Best (Jan 22 2021 at 05:00):

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

view this post on Zulip François Sunatori (Jan 22 2021 at 05:03):

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?

view this post on Zulip Alex J. Best (Jan 22 2021 at 05:11):

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

view this post on Zulip Damiano Testa (Jan 22 2021 at 06:52):

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

proof of , proof of 

view this post on Zulip Kevin Buzzard (Jan 22 2021 at 07:13):

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.

view this post on Zulip Johan Commelin (Jan 22 2021 at 07:19):

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

view this post on Zulip Damiano Testa (Jan 22 2021 at 07:29):

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

view this post on Zulip François Sunatori (Jan 22 2021 at 15:43):

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)

view this post on Zulip Alex J. Best (Jan 22 2021 at 17:22):

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)

view this post on Zulip Eric Wieser (Jan 22 2021 at 17:42):

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)

view this post on Zulip François Sunatori (Jan 22 2021 at 17:59):

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.

view this post on Zulip Eric Wieser (Jan 22 2021 at 18:04):

*with one constructor

view this post on Zulip Eric Wieser (Jan 22 2021 at 18:04):

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

view this post on Zulip François Sunatori (Jan 22 2021 at 19:16):

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!


Last updated: May 08 2021 at 09:11 UTC