Angle brackets

Stream: new members

[Robert Spencer]

Are (| ... |) and ⟨ ... ⟩ meant to be treated identically by lean?

[Robert Spencer]

In particular, I have a case where or.inr ⟨a, b⟩ works as expected, but or.inr (|a, b|) does not (it does though if I write or.inr ( (|a, b|) ).

[Simon Hudon]

That is curious. @Sebastian Ullrich, is this normal?

[Sebastian Ullrich]

It looks like (| is missing the precedence from ⟨

[Sebastian Ullrich]

i.e. it's a bug

[Simon Hudon]

Is it worth fixing?

[Robert Spencer]

Well, I'll file an issue, and then people can decide.

[Mario Carneiro]

issues at lean repo are dead on arrival for the most part. Everything I have seen suggests that lean ascii support is half-hearted at best and has several issues, and seems like one of those things that is more likely to be dropped than fixed in lean 4

[Mario Carneiro]

I recommend getting used to the angle brackets

[Patrick Massot]

This (| ... |) is a nightmare for mathematicians who want to use | for absolute values. I really really hope Lean 4 drops it

[Robert Spencer]

Hmmkay. That's a little disappointing personally as I am loathe to install an IDE just for unicode support.

[Mario Carneiro]

I mean, if you can find another means to input the unicode, by all means go ahead, but it's certainly easiest to use an editor that supports unicode

[Mario Carneiro]

You don't really need an IDE - I hesitate to call the existing editors IDEs since they are mostly just error reporting and unicode input

[Mario Carneiro]

but presumably you use some text editor to write your files, and you can probably set it up to input the lean unicode characters

[Robert Spencer]

This is true. I should just not be lazy and write some vimscript to translate \forall etc into unicode.

[Robert Spencer]

Although if it is the opinion of the maintainers that ASCII should not be preferred, it might be worth mentioning this in the tutorial document, and possibly throwing warnings that ASCII is deprecated (a bit more extreme)

[Patrick Massot]

You don't need any fancy vimscript, imap is all you need

[Kevin Buzzard]

Saved by a fellow vimmer :-) There are all sorts of people around here :-)

[Jeremy Teitelbaum]

That makes sense. I'm working on proving that X in Z and Y in Z implies X union Y in Z. The statement

rintros \< hXZ, hYZ\> a (h1 | h2)

magically pulls this apart but I'm not sure why you use angle brackets in the first part and regular parens in the second.

[Kevin Buzzard]

and is an inductive type with one constructor which takes two inputs -- that's the pointy brackets. or is an inductive type with two constructors, that's the round brackets.

[Mario Carneiro]

They represent different operations. (h1 | h2) destructures an or-like type and produces two subgoals; \<h1, h2\> destructures an and-like type and produces one subgoal with two hypotheses

[Kevin Buzzard]

import tactic

example (A B C : Prop) : A ∨ B → C :=
begin
  rintro (hA | hB),
  /-
  2 goals

  A B C: Prop
  hA : A
  ⊢ C

  A B C : Prop
  hB: B
  ⊢ C
  -/
  sorry, sorry
end

[Jeremy Teitelbaum]

I will ponder this. I think I need to get a grip on what I'm doing from the point of view of the underlying language, since the words "constructor" have no meaning to me in this context (though I do know the term from general object oriented programming).

[Mario Carneiro]

That pattern is appropriate for destructuring a goal that looks like A /\ B -> C -> D \/ E -> F, and produces two subgoals like

hXY : A, hYZ : B, a : C, h1 : D |- F

hXY : A, hYZ : B, a : C, h1 : E |- F

[Mario Carneiro]

The word "constructor" is applied to the functions that construct an element of an inductive type. For example, if you look at src#or, you will see that it has two constructors, called or.inl and or.inr

[Kevin Buzzard]

If P and Q are propositions, then they're types, as are P ∧ Q and P ∨ Q. If P is a proposition then to give a term of type P is to give a proof of P. Statements like $P\implies Q$ now become functions from proofs of $P$ to proofs of $Q$.

[Kevin Buzzard]

P ∧ Q has one constructor. If you want to prove P ∧ Q then the only way to do it is to prove P and to prove Q! So P ∧ Q has one constructor which takes as inputs proofs of P and of Q and then gives you a proof of P ∧ Q. On the other hand there are two ways to prove P ∨ Q -- you can either prove P or you can prove Q. So P ∨ Q has two constructors! This whole story is very weird because "and" and "or" are just defined by truth tables as far as I'm concerned and they're basically dual to each other. The asymmetry comes from the fact that we're doing constructive logic here, and so you get a whole bunch of extra weirdness which as mathematicians we are not usually exposed to.

[Kevin Buzzard]

A very good place to read about this stuff is Theorem Proving In Lean #tpil -- chapter 3 does this stuff: https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html .

[Jeremy Teitelbaum]

OK, thanks a lot, I will see where this all takes me.

[Kevin Buzzard]

That book holds off from introducing tactics until chapter 5, which has the disadvantage that pre that point proofs can become quite long and unwieldy and difficult to debug (you miss a bracket somewhere, you get an incomprehensible error three lines later and you're totally bewildered), but it has a _really_ good explanation to the whole "a proposition is a type" thing.

[Kyle Miller]

Jeremy Teitelbaum said:

the words "constructor" have no meaning to me in this context (though I do know the term from general object oriented programming).

Maybe if you want to relate OO, the Lean constructors are like static factory methods on an abstract base class. Lean promises that every object can be constructed using one of these factory methods, so you get a reverse operation, destructuring.

One weird way to think about destructuring is that you're doing the visitor pattern, and each goal that pops up is a different "method" you have to implement.