Equality for the ⟨⟩

Stream: general

[Kind Bubble]

I'm trying to figure this one out:

variable {X : Type}
variable {x : X}
variable {y : X}
variable {p : x = y}
def q : ⟨x, x, x⟩ = ⟨y,y,y⟩ := sorry

I think it should be pretty simple.

[David Renshaw]

You need to specify what type you mean for the equality. For example:

variable {X : Type}
variable {x : X}
variable {y : X}
variable {p : x = y}
def q : (⟨x, x, x⟩ : X × X × X) = ⟨y,y,y⟩ := sorry

[David Renshaw]

⟨⟩ is "anonymous constructor syntax", and it can construct values of any product-like type.

[Kind Bubble]

David Renshaw said:

Ok hmm... here:

variable {X : Type}
variable {x : X}
variable {y : X}
variable {p : x = y}
def q : (⟨x, x, x, Unit.unit⟩ : Σ'(_:X), Σ'(_:X),Σ'(_:X),Unit) = ⟨y,y,y, Unit.unit⟩ := sorry

Now I'm trying to figure out the name of the axiom

[David Renshaw]

oh, is this Lean 4?

[Kind Bubble]

David Renshaw said:

oh, is this Lean 4?

yeah sorry about that

[David Renshaw]

variable {X : Type}
variable {x : X}
variable {y : X}
variable {p : x = y}
def q : (⟨x, x, x, Unit.unit⟩ : Σ'(_:X), Σ'(_:X), Σ'(_:X),Unit) = ⟨y,y,y, Unit.unit⟩ := by congr

[Kind Bubble]

What does by do?

[David Renshaw]

starts tactic mode. congr is a tactic

[Kind Bubble]

David Renshaw said:

starts tactic mode. congr is a tactic

Now suppose I've got some more complex constituent equalities (p:x = y here).

[Kind Bubble]

how would I assemble them? would congr automatically know about these demonstrated constituent equalities?

[David Renshaw]

I expect congr to break it into simpler subgoals for you

[Kind Bubble]

Ok thanks. This is good.

Nonetheless if someone knows a closed form for this involving constituent equalities that would be much appreciated.

[Kind Bubble]

Like ??? here:

variable {X : Type}
variable {x : X}
variable {y : X}
variable {p : x = y}
def q : (⟨x, Unit.unit⟩ : Σ'(_:X),Unit) = ⟨y,Unit.unit⟩ := ??? p Eq.refl

[Mario Carneiro]

congr applies congruence theorems, which have the form e.g. a = b -> c = d -> (a, c) = (b, d). They are generated on the fly, but you can prove them by using Eq.rec

[Mario Carneiro]

congr_arg is a theorem which covers most cases of this

[Kind Bubble]

Mario Carneiro said:

congr applies congruence theorems, which have the form e.g. a = b -> c = d -> (a, c) = (b, d). They are generated on the fly, but you can prove them by using Eq.rec

like this?

variable {X : Type}
variable {x : X}
variable {y : X}
variable {p : x = y}
def q : (⟨x, Unit.unit⟩ : Σ'(_:X),Unit) = ⟨y,Unit.unit⟩ := Eq.rec p Eq.refl

[Mario Carneiro]

probably p ▸ Eq.refl _ works

[Mario Carneiro]

▸ is a wrapper for Eq.rec which is better able to infer the higher order function argument (the "motive") in Eq.rec

[Mario Carneiro]

theorem q : (⟨x, Unit.unit⟩ : Σ'(_:X),Unit) = ⟨y,Unit.unit⟩ := p ▸ Eq.refl _
#print q

if you mouse over the ▸ in the proof it shows

@Eq.rec X x (fun x_1 h => { fst := x, snd := () } = { fst := x_1, snd := () }) (Eq.refl { fst := x, snd := () }) y p

where fun x_1 h => { fst := x, snd := () } = { fst := x_1, snd := () } is the "motive"

[Kind Bubble]

Mario Carneiro said:

theorem q : (⟨x, Unit.unit⟩ : Σ'(_:X),Unit) = ⟨y,Unit.unit⟩ := p ▸ Eq.refl _
#print q

if you mouse over the ▸ in the proof it shows

@Eq.rec X x (fun x_1 h => { fst := x, snd := () } = { fst := x_1, snd := () }) (Eq.refl { fst := x, snd := () }) y p

where fun x_1 h => { fst := x, snd := () } = { fst := x_1, snd := () } is the "motive"

hmm wow. ok this is great.