easy questions

Stream: new members

[Adrian Chu]

theorem test (x : ℕ): ∃ a : ℕ, 2*a = 4 := sorry

theorem test2 (x : ℕ): ∃ b : ℕ, 3*b = 6 :=
begin
fapply exists.intro,
  exact 3, sorry
end

in this stupid theorem, i want to replace 3 with the a given by test, how should i write?

[Kenny Lau]

you can't take out what you put in the proof of an existential statement

[Adrian Chu]

huh? but then how should we define a number x+1, in which the existence of x is guaranteed by some previous theorem A?

[Kenny Lau]

example (choice : Π (C : ℕ → Prop), (∃ n, C n) → ℕ)
  (spec : ∀ (C : ℕ → Prop) (n : ℕ) (h : C n), choice C ⟨n, h⟩ = n) :
  false :=
nat.zero_ne_one $ show 0 = 1, from
calc  0
    = choice (λ n, n = n) ⟨0, rfl⟩ : (spec (λ n, n = n) 0 rfl).symm
... = choice (λ n, n = n) ⟨1, rfl⟩ : rfl
... = 1                           : spec (λ n, n = n) 1 rfl

[Kenny Lau]

this is because of proof irrelevance, where two proofs of the same theorem are definitionally equal

[Kenny Lau]

so in particular two witnesses result in the same proof of the existential.

[Kenny Lau]

but you can use a subtype to retain the witness:

def test : { a : ℕ // 2*a = 4} := ⟨2, rfl⟩

theorem test2 : ∃ b : ℕ, 3*b = 6 := ⟨test.1, rfl⟩

[Alistair Tucker]

But if you want only want to use the witness a in a proof of something else then you can say cases test with a ha,

[Kenny Lau]

oh right

[Kenny Lau]

theorem test : ∃ a : ℕ, 2*a = 4 := ⟨2, rfl⟩

theorem test2 : ∃ b : ℕ, 3*b = 6 :=
begin
  cases test with a ha,
  refine ⟨a, _⟩,
  have : a = 2,
  { rw two_mul at ha,
    exact nat.bit0_inj ha },
  subst this,
  refl
end

[Adrian Chu]

i see, thanks!!

[Kevin Buzzard]

you can't take out what you put in the proof of an existential statement

Don't listen to the constructivist!

import tactic.interactive

theorem test (x : ℕ): ∃ a : ℕ, 2*a = 4 := sorry

theorem test2 (x : ℕ): ∃ b : ℕ, 3*b = 6 :=
begin
  choose a ha using test 37,
  /-
  1 goal
  x a : ℕ,
  ha : 2 * a = 4
  ⊢ ∃ (b : ℕ), 3 * b = 6
  -/
  sorry
end

[why does test take an input which is never used?]

[Reid Barton]

You don't need choose here, just cases which was mentioned earlier

[Kevin Buzzard]

Sure, but this is a refutation of Kenny's claim "you can't take out what you put in the proof of an existential statement". The issue with choose is that it is noncomputable (Lean actually forgot a once it had checked your proof, so there is no algorithm for getting it back).

[Kenny Lau]

but my point was that you can't take out what you put in, i.e. the explicit witness you constructed

[Kenny Lau]

contrary to maths where you can always destruct an existential to get data

[Mario Carneiro]

I don't know that in maths the behavior is much different from choose

[Mario Carneiro]

Except possibly that you can prove additional properties to put in the existential after the fact

[Mario Carneiro]

but this is more of a proof structuring thing

[Keeley Hoek]

I think the situation in real maths is just that if you constructed an existential by directly producing a term, then if you ever need it later you're allowed to remember your proof and the element

[Kevin Buzzard]

It's even better than that, we're even allowed to say "By the proof of Theorem 3.2, ..."

[Adrian Chu]

how to prove that

def x: ℕ → ℕ := (λ i, i+1)
def y: ℕ → ℕ := (λ i, 1+i)
theorem test : x = y  := by sorry

? library search gives nothing

[Johan Commelin]

begin
  funext i,
  sorry
end

[Johan Commelin]

Or in term mode: funext $ _

[Adrian Chu]

i see

[Kevin Buzzard]

Why does rfl fail?

[Kevin Buzzard]

def x: ℕ → ℕ := (λ i, i+1)
def y: ℕ → ℕ := (λ i, 1+i)
theorem test : x = y  := rfl -- type mismatch

[Kenny Lau]

the first one is i+1 and the second one is 1+i

[Kevin Buzzard]

oh thanks. Duh.

[Kevin Buzzard]

The colours played a trick on my brain somehow

[Keeley Hoek]

Whoever made the courier new typeface has caused at least billions of dollars of damage with how close i and 1 look

[Adrian Chu]

wouldn't 1 and l be deadlier?

[Marc Huisinga]

1ucki1y l is 1ess common in programming

[Keeley Hoek]

is it illegal to delcare a long literal in Java with a lower case l?

[Keeley Hoek]

If no, that's a good one

[Mario Carneiro]

that's legal

[Johan Commelin]

There's an entire class of "off-by-l" errors

[Gun Pinyo]

Hi guys, I want to use the heterogeneous equality but cannot derive it to homogeneous equality. i.e. can we define the following?

    def foo (α β : Type) (p : α = β) (x : α) (y : β) :
              x == y → (eq.rec_on p x : β) = y := sorry

[Chris Hughes]

def foo (α β : Type) (p : α = β) (x : α) (y : β) :
              x == y → (eq.rec_on p x : β) = y := λ h, by cases h; refl

[Chris Hughes]

You don't need the assumption α = β, it's implied by x == y

[Gun Pinyo]

@Chris Hughes ah, thanks. but how about another way?

[Gun Pinyo]

wait, if we don't need p : α = β, then how can we express (eq.rec_on p x : β) = y?

[Chris Hughes]

You could write eq.rec_on (type_eq_of_heq (h : x == y)) x

[Gun Pinyo]

Hi, there. Can anyone tell me why the following example doesn't work?

example (α β : Type) (p : α = β) : unit → α = unit → β :=
  begin rw p, reflexivity end

after rw p the goal is unit → β = unit → β but reflexivity doesn't work.

[Chris Hughes]

Brackets

example (α β : Type) (p : α = β) : (unit → α) = (unit → β) :=
  begin rw p end

[Gun Pinyo]

@Chris Hughes wow, such a silly mistake. Thank you

[Kenny Lau]

example (α β : Type) (p : α = β) : unit → α = unit → β :=
  begin intros _ h, rw [← p, h], exact () end

[Gun Pinyo]

Does lean have something like the following in standard library or mathlib?

def uip (α : Prop) (x y : α) : x = y := sorry

if not, how can we prove this?

[Kenny Lau]

rfl

[Kenny Lau]

this is called proof irrelevance and is built into Lean

[Kenny Lau]

it says that two proofs of the same proposition are definitionally equal

[Gun Pinyo]

@Kenny Lau , thank you :)

[Gun Pinyo]

I have a problem with unfolding tactic. Considering the following code

structure graph :=
  (nodes  : Type)
  (edges  : Type)
  (srctrg : bool → edges → nodes)

def prism_graph (G : graph) : graph :=
  { nodes  := bool × G.nodes
  , edges  := (bool × G.edges) ⊕ G.nodes
  , srctrg := λ b e, match e with
                     | (sum.inl (b', e)) := (b, G.srctrg b' e)
                     | (sum.inr v)       := (b, v)
                     end
  }

def cube_graph : ℕ → graph
| 0      := ⟨unit, unit, (λ _ _, ())⟩
| (n +1) := prism_graph (cube_graph n)

example (n : ℕ) (b : bool) (v : (cube_graph n).nodes) :
      (graph.srctrg (cube_graph (n +1)) b (sum.inr v)) = (b, v) :=
  begin
    unfold cube_graph,
  end

I don't understand why unfold cube_graph fails. Clearly, it should succeed with the goal become (graph.srctrg (prism_graph (cube_graph n)) b (sum.inr v)) = (b, v).

Ps. You might argue that I can close this tactic by refl but my point is to use unfold. The reason is that this is the simplified version of the actual problem that I am working and I can't just use refl.
Ps2. This is another question. If refl works, why simp doesn't. Isn't simp use refl at the end anyway?

[Patrick Massot]

You're expecting too much from unfold. What you want here is dsimp [cube_graph].

[Patrick Massot]

About your second question, maybe simp is actually doing some thing which turns your goal into a non-refl goal.

[Chris Hughes]

You can use dunfold. The reason simp doesn't work, is because graph.srctrg is a dependent function, so the expression after rewriting only typechecks because cube_graph (n + 1) = prism_graph (cube_graph n) is s definitional equality.

[Gun Pinyo]

@Patrick Massot @Chris Hughes Thank you for introducing dsimp and dunfold to me.

Another question, if I have two occurrences of the same
definition in a goal. (d)unfold once will affect the first
occurrence an not the second, if I want another way (i.e. affect the second
one and not the first one) what should I do?

[Kevin Buzzard]

Definitional unfolding is all defeq, so if your goal does not look like what you want it to look like, you can just write change <what you want the goal to look like> and if what you write is definitionally equal to what the goal is, the goal will change to what you write. Note that show is synonymous with change, although you can use change on hypotheses as well.

[Kevin Buzzard]

The other approach for zooming in on terms in goals is conv mode: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

[Kevin Buzzard]

I don't know how much you know about definitional equality v all the other equalities, but here's something I wrote about definitional equality: https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/

[Chris Hughes]

Patrick Massot Chris Hughes Thank you for introducing dsimp and dunfold to me.

Another question, if I have two occurrences of the same
definition in a goal. (d)unfold once will affect the first
occurrence an not the second, if I want another way (i.e. affect the second
one and not the first one) what should I do?

Do you have an example of this. Usually I think it unfolds all occurrences, so it might be not unfolding the second one for some other reason.

[Kevin Buzzard]

Another thing you might want to know is that if you type #print prefix cube_graph then you can see all the stuff that Lean generated for you when you made cube_graph. Things called cube_graph._equation.1 or something (I forget what they're exactly called) are the things which Lean tries to use when you run unfold -- that's what the tactic actually does. Similarly dsimp [cube_graph] tries to simplify using those "hidden" equation lemmas.

[Gun Pinyo]

@Kevin Buzzard Thank you for introducing change and conv. These what tactics that I have been looking for many days. It is also interesting to know that we can even unfold anonymous functions as well.

@Chris Hughes I have but it is in a long file and it can be the case that the second occurrence is not unfoldable at the moment so I miss understood the behaviour of (d)unfold .

[Jesse Michael Han]

@Gun Pinyo you should definitely read through the general mathlib tactic documentation

[Gun Pinyo]

If I am in the tactic mode with 2 goals. Is there any tactic that lets me prove the second goal before the first one?
The motivation behind this is when the second goal is a lot easier than the first one.

Ps. I have read through https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md but didn't find any.

[Kevin Buzzard]

swap

[Kevin Buzzard]

Once you've got it working, hover over the tactic to see the docstring.

[Gun Pinyo]

@Kevin Buzzard Thank you.
So there are more tactics that are not in mathlib. Where can I find the documentation of these built-in tactics?
At first, I thought every built-in tactic should be in https://leanprover.github.io/reference/tactics.html# but it is not the case for swap.

[Kevin Buzzard]

Maybe swap is in core Lean? You can just right click on it to check.

[Kevin Buzzard]

A great place for learning about core tactics is the book Theorem Proving In Lean.

[Bryan Gin-ge Chen]

It would be good to add swap and any other missing core tactics to that doc page. Maybe for now we should just add a comment to this issue https://github.com/leanprover-community/mathlib/issues/450

[Gun Pinyo]

@Kevin Buzzard I agree, that was what I did before starting my current project.
But again, it doesn't mention swap.

[Gun Pinyo]

Oh, btw, swap is defined in mathlib and not the builtin one. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean

[Keeley Hoek]

If I recall, core defines tactic.swap but does not expose to interactive?

[Gun Pinyo]

This might be a very stupid question but why can't we add univalence axiom to lean3? i.e. why axiom K of lean3 doesn't play well with the univalence axiom?

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

This has been talked about before and I know it's inconsistent but I don't know why. It's something to do with impredicativity of Prop

[Chris Hughes]

Because equality is a subsingleton, and univalence says it is isomorphic to something which is not a subsingleton. Even if you define a equality to return a type, rather than a Prop, this is still provably a subsingleton (the proof uses the proof irrelevant version of eq).

[Chris Hughes]

I think α ≃ β → α = β is consistent though, but not very useful.

[Kevin Buzzard]

So is even my undeleted post incorrect?

[Kevin Buzzard]

Because α = β → α ≃ β is a theorem

[Chris Hughes]

Those two function aren't inverses of each other in Lean, but univalence says they are.

[Kevin Buzzard]

Surely α ≃ β → α = β would be useful in Lean, because it would enable me to show that if R and S are isomorphic rings and R is Noetherian local then S is Noetherian local?

[Chris Hughes]

You also need the ring structures to be heq for that. Which won't be provable.

[Kevin Buzzard]

So you can't get from the bare α ≃ β → α = β statement about types to statements about isomorphic groups being equal groups by using some kind of trickery?

[Kevin Buzzard]

I would imagine that in HoTT they can do this somehow

[Chris Hughes]

I don't think so. In Lean, you have no idea what eq.mp gives you. In HoTT, you know from the right_inv part of the univalence equivalence, that eq.mpr is to_fun of your bijection. Then you can prove that eq.rec one_ring_strcuture = the_other_ring_structure

[Chris Hughes]

In the univalence equivalence inv_fun := eq.mp. The axiom says that eq.mp has a two sided inverse.

[Floris van Doorn]

In answer to the original question: from univalence you can show that bool = bool has two unequal elements (one corresponding to the identity function, and one corresponding to the function that swaps the elements), which contradicts axiom K.

[Floris van Doorn]

And I'm quite sure that Chris is right that weak univalence (α ≃ β → α = β) doesn't give you that isomorphic groups are equal.

[Gun Pinyo]

Hi, there. Regarding defined class in stdlib, many of them have one field. I try to understand why don't you just use def with @[class]? For example,

class inhabited (α : Sort u) :=
(default : α)

@[class] def inhabited' (α : Sort u) := α

inhabited' should be as usable as inhabited but we also don't need to write the constructor.

There are some classes that way such as in library/init/relator.lean. I can see the advantage of using the letter way but haven't seen the advantage of the former way. Could you please explain to me please?

[Andrew Ashworth]

<deleted>

[Andrew Ashworth]

<deleted>

[Andrew Ashworth]

<deleted>

[Floris van Doorn]

One difference is that inhabited' α is definitionally equal to α, while inhabited α is not (it is equivalent to α, in the sense that equiv (inhabited α) α can be proven).
Sometimes extra definitional equalities are convenient, but sometimes they have downsides. It is possible that the elaborator of Lean will unfold inhabited' in places where you didn't want to, and then you are not talking about the type inhabited' α anymore, but about α. The latter is not a class, which might cause issues with type class inference not firing.
Since inhabited is not a definition, it can never be unfolded.

[Andrew Ashworth]

This is a much better explanation of why, haha.

[Gun Pinyo]

@Floris van Doorn , how about we add @[irreducible] to inhabited' α, would it solved the problem with unwanted unfolding?

[Reid Barton]

In that case there won't be much advantage of the def over the single-field class

[Floris van Doorn]

That would also be fine. But as Reid said: if you don't want to unfold it, you can just as well make it a structure.

[Gun Pinyo]

Well, my point is that I don't want to keep writing .intro or something like that.

[Andrew Ashworth]

Angle bracket notation doesn't work for you?

[Chris Hughes]

If you marked it irreducible you'd have to define anintro and use that.

[Gun Pinyo]

I just discover that we can write numerals as elements of fin
type. So I want to refactor the following code:

def fin.zero {n : ℕ} : fin (n +1) := ⟨0, nat.zero_lt_succ n⟩
def vector.insert_nth_zero : v.insert_nth a fin.zero = a :: v :=
  begin
    cases v with l p,
    simp [fin.zero, vector.insert_nth, vector.cons, list.insert_nth],
  end

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
  begin
    cases v with l p,
    simp [{!what should be here?!}, vector.insert_nth, vector.cons, list.insert_nth],
  end

vector.insert_nth_zero' is the same as vector.insert_nth_zero
except that fin.zero is changed to 0. Everything should be fine, however, I don't know there to replace fin.zero in simp tactic now. Does anyone know how to fix this?

[Joe]

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
  begin
    cases v with l p,
    simp only [vector.insert_nth], norm_cast
  end

[Joe]

or maybe this

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
  begin
    cases v with l p,
    simp only [vector.insert_nth, vector.cons, subtype.mk_eq_mk],
    show list.insert_nth 0 a l = a :: l,
    simp [list.insert_nth]
  end

[Gun Pinyo]

I still have another question regarding fin. Sometimes, I want to use pattern matching on i : fin n in the same way as one will do in ℕ but since the inductive part is in i.val so I need to do as follows:

def fin_is_even : Π n : ℕ, fin n → bool
| 0      i                        := i.elim0
| (n +1) ⟨0,    _⟩                := true
| (n +1) ⟨i_val +1, succ_i_is_lt⟩ :=
     let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩
      in bnot (fin_is_even n i)

Ok it works, but in practice, I find it quite annoying to write let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩ every time whereas i should be obtained directly from something like fin.succ i. Therefore, I try to use @[pattern] to help me with this as follows:

@[pattern]
def fin.zero {n : ℕ} : fin (n +1) := ⟨0, nat.zero_lt_succ n⟩

attribute [pattern] fin.succ

def fin_is_even' : Π n : ℕ, fin n → bool
| 0      i            := i.elim0
| (n +1) fin.zero     := true
| (n +1) (fin.succ i) := bnot (fin_is_even' n i)

However I get an error, what is wrong with my code? Did I misunderstand anything about @[pattern]?

err msg1:
invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
err msg2:
don't know how to synthesize placeholder context: fin_is_even' : Π (n : ℕ), fin n → bool ⊢ fin n

[Chris Hughes]

You're basically expecting the equation compiler to determine whether an element of fin n is in the image of fin.succ or not, and if it is what the element that maps to it is. This is very hard in general. I think the pattern attribute only works for things that are definitionally equal to a constructor. for example λ x, x + 2 = λ x, nat.succ (nat.succ x), by definition, so marking add with the pattern attribute works. Incidentall changing your definition of fin.zero also works - it also wanted to reduce the proof to a constructor, but it's probably not a desirable change.

@[pattern]
def fin.zero {n : ℕ} (h): fin (nat.succ n) := ⟨0, h⟩

attribute [pattern] fin.succ

def fin_is_even' : Π n : ℕ, fin n → bool
| 0      i            := i.elim0
| (n +1) (fin.zero h)     := true
--| (n +1) x := bnot (fin_is_even' n i)

[Gun Pinyo]

@Chris Hughes , thank you, now I can see why fin.succ doesn't work. Anyway, is there any other that allow us use something like fin.zero and fin.succ in pattern matching? I really miss the following alternative definition of fin

inductive fin' : ℕ → Type
| zero : fin' 0
| succ : Π {n : ℕ}, fin' n → fin' (n +1)

But I use this definition, it is incompatible with the standard library.

I think the pattern attribute only works for things that are definitionally equal to a constructor

How about this following code in data.vector? Is this definitionally equal to any constructor? I fact, I haven't seen any code using pattern matching on vector

@[pattern] def nil : vector α 0 := ⟨[],  rfl⟩

@[pattern] def cons : α → vector α n → vector α (nat.succ n)
| a ⟨ v, h ⟩ := ⟨ a::v, congr_arg nat.succ h ⟩

[Chris Hughes]

nil definitely is. cons definitely isn't.

Actually it depends on the vector you're trying to match with. If your vector is a variable then it won't work. If you do

match vector.mk l rfl with...

Then it has a better chance of working, but I think the prood of equality would have to be rfl.

[Kevin Buzzard]

I thought this variant of fin was in mathlib somewhere