## Stream: general

### Topic: nearly no_confusion

#### Kevin Buzzard (Mar 23 2018 at 23:22):

I spent some time with Chris at Xena last night trying to get to the bottom of no_confusion. I seem to have a slightly simpler approach which gives what looks to me like everything we need for a proof of the idea that two nats are equal iff they were constructed using the same constructors in the same order.

#### Kevin Buzzard (Mar 23 2018 at 23:23):

inductive  xnat
| zero : xnat
| succ : xnat → xnat

open xnat

def  xnat_no_confusion_prop (s : xnat) (t : xnat) : Prop  :=
xnat.rec (xnat.rec true (λ _ _,false) t) (λ m _,(xnat.rec false (λ n _,(m=n)) t)) s

variables m n : xnat
#reduce xnat_no_confusion_prop zero zero -- true
#reduce xnat_no_confusion_prop (succ m) zero -- false
#reduce xnat_no_confusion_prop zero (succ n) -- false
#reduce xnat_no_confusion_prop (succ m) (succ n) -- (m = n)

def  xnat_no_confusion' (s t : xnat) (H : s = t) : xnat_no_confusion_prop s t :=
begin
rw H,
cases t with n,
exact trivial, -- t = 0
show (n=n), -- t = succ n
refl,
end

example : succ m = succ n → m = n :=  λ H, xnat_no_confusion' _ _ H
example : ¬ succ m = zero :=  λ H, xnat_no_confusion' _ _ H



#### Kevin Buzzard (Mar 23 2018 at 23:24):

Here I prove injectivity of xnat.succ and also that zero is not a succ using an easier variant of the no_confusion / no_confusion_type strategy, where instead of carrying round a general sort P I just use the relevant props.

#### Kevin Buzzard (Mar 23 2018 at 23:25):

Are there other applications of no_confusion_type lemmas which go beyond this sort of "instance of inductive type is uniquely determined by how it was constructed" sort of thing? Or am I missing something else? Why is this sort P used?

#### Kevin Buzzard (Mar 23 2018 at 23:27):

I'm writing a blog post about all this no_confusion stuff and I was somehow expecting for this to come out in the wash but it didn't, so I need to think of something coherent to say about why the general sort P is involved before I post.

#### Andrew Ashworth (Mar 23 2018 at 23:56):

was mcbride's paper on no confusion not helpful?

#### Kevin Buzzard (Mar 23 2018 at 23:58):

I either don't know this paper, or I looked at it before and at the time it was too much for me. Having actually spent some time thinking about no_confusion_type now perhaps I can ask you for a link to this paper in the hope that I can get something from it?

#### Andrew Ashworth (Mar 24 2018 at 00:04):

mcbride's phd thesis is definitely hard going

#### Andrew Ashworth (Mar 24 2018 at 00:06):

i had to sit and stare at it for awhile, and i still don't fully understand it :sweat_smile:

#### Kevin Buzzard (Mar 24 2018 at 00:08):

Well I am not an expert but it seems to me that what McBride is defining on p136ff is what is implemented in Lean.

#### Kevin Buzzard (Mar 24 2018 at 00:08):

Maybe I should just post my blog post. Hang on.

#### Mario Carneiro (Mar 24 2018 at 00:18):

I think the reason no_confusion uses a general sort instead of using the consequent m = n directly is because the number of conclusions varies with the constructors, so that for list it would be something like cons a l = cons a' l' -> a = a' /\ l = l', which is a bit less natural to define inductively since the 0-ary case gets special consideration, and it also relies on the definition and which may not be available yet. As it is defined normally no_confusion for an arbitrary type needs nothing except the basics of DTT, plus eq and heq (which comes up when there are dependencies, for example sigma.mk a b = sigma.mk a' b' -> a = a' /\ b == b' where the latter equality involves b : B a and b' : B a' which are different types.

#### Kevin Buzzard (Mar 24 2018 at 00:25):

https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

#### Mario Carneiro (Mar 24 2018 at 00:37):

Here's another interesting story to do with no_confusion:

inductive {u} mystery : Sort u
| A : mystery
| B : mystery

def confused : Type := mystery
def confused.A : confused := mystery.A
def confused.B : confused := mystery.B
open confused

theorem A_ne_B_attempt_1 : A ≠ B :=
λ h, mystery.no_confusion h --fails: no_confusion not defined

theorem A_ne_B_attempt_2 : A ≠ B :=
λ h, by cases h -- now I have to prove ⊢ false?

theorem A_ne_B_attempt_3.no_confusion_type : mystery → mystery → Type
| mystery.A mystery.A := _ -- already fails, can't case on mystery
| mystery.B mystery.A := _
| mystery.A mystery.B := _
| mystery.A mystery.B := _

#print mystery.rec
-- protected eliminator tc.mystery.rec : ∀ {C : mystery → Prop},
-- C mystery.A → C mystery.B → ∀ (n : mystery), C n
--
-- Hm, the recursor only eliminates to Prop, so we can't
-- define functions like no_confusion_type

-- Maybe we can prove they are equal instead? If it was a Prop
-- they would be equal by proof irrelevance...
theorem A_eq_B_attempt_1 : A = B := rfl --nope


#### Mario Carneiro (Mar 24 2018 at 00:39):

The punch line is that confused is a type with two elements A and B, for which it is impossible to prove whether they are equal or not

#### Mario Carneiro (Mar 24 2018 at 00:45):

By the way in the blog post you could have defined mytype_equal like so:

def  mytype_equal : mytype → mytype →  Prop
| mytype.AA mytype.AA := true
| mytype.AA mytype.ZZ := false
| mytype.ZZ mytype.AA := false
| mytype.ZZ mytype.ZZ := true


Not sure if you were deliberately showing off other ways to construct it

#### Mario Carneiro (Mar 24 2018 at 00:51):

Re: the one-sided inverse, that approach actually does work in general, as a "partial projection". So for example you could define head l : option A when l : list A, to return none on the empty list and a on a::l. In general, you have an inductive type with several constructors, each of which has several arguments, and you can project each element of each constructor in an option, returning none if the wrong constructor is passed in and some a where a is the appropriate argument to the constructor otherwise. You can reconstruct the cases_on theorem using all these projections.

#### Kevin Buzzard (Mar 24 2018 at 01:05):

Aah excellent, I will beef up the post tomorrow

Thanks!

#### Kevin Buzzard (Mar 24 2018 at 16:30):

PS Do you think I'm wasting my time trying to get to the bottom of things like this? I am currently thinking about getting to the bottom of something else I've always been confused by -- "using-well-founded" (the error you get when you try and define something by recursion but things are slightly too convoluted for the elaborator(?) to figure out that what you're doing will definitely terminate after a finite time). Currently the only way I know how to figure stuff out is to look at the source code and then work stuff out by experimenting. My plan, like the no-confusion post, would be to work out some simple examples, and basically write some docs and either PR them to mathlib docs or blog about them. But when Lean 4 comes is there every chance that everything I write about these sorts of "obscure" parts of Lean will be no longer relevant?

#### Kevin Buzzard (Mar 24 2018 at 16:34):

I think I'm right in saying that using_well_founded is not mentioned in either the reference manual or TPIL (like no_confusion).

#### Kevin Buzzard (Mar 24 2018 at 16:49):

Re : mystery -- why is it any different to bool? It clearly is:

#### Kevin Buzzard (Mar 24 2018 at 16:49):

inductive {u} mystery : Sort u
| A : mystery
| B : mystery

#print  prefix mystery

inductive  bool'
| TT : bool'
| FF : bool'

#print  prefix bool'


#### Kevin Buzzard (Mar 24 2018 at 16:51):

we get bool'.no_confusion but no mystery.no_confusion; and bool.rec eliminates to any Sort whereas mystery.rec only eliminates to Prop. Why is this?

#### Simon Hudon (Mar 24 2018 at 16:53):

Because mystery can inhabit multiple types including Prop and when it does, it's a bit like or. If you could eliminate to anything other than Prop, you could affect the behavior of a program with just a proof

#### Simon Hudon (Mar 24 2018 at 16:55):

for example:

def prog : mystery.{0} -> nat
| A := 0
| B := 1


wouldn't make sense because of proof irrelevance

#### Kevin Buzzard (Mar 24 2018 at 17:08):

I see. The whole point is that mystery is allowed to be a Prop so everything is paranoid. You guys should get classical.

#### Andrew Ashworth (Mar 24 2018 at 17:09):

it's not a waste of time. some version of well-founded recursion will be in lean 4

#### Andrew Ashworth (Mar 24 2018 at 17:09):

what might change is the exact syntax / using_well_founded, so perhaps you could discuss doing it manually using well_founded.fix

#### Kevin Buzzard (Mar 24 2018 at 17:10):

I know even less about well_founded.fix.

#### Andrew Ashworth (Mar 24 2018 at 17:11):

i don't know much either about the fixed points of functions, so i would avidly read your blog post :)

#### Andrew Ashworth (Mar 24 2018 at 17:11):

it's a way of expressing well-founded induction

#### Kevin Buzzard (Mar 24 2018 at 17:11):

You should use Coq, everything seems to be defined using Fixpoint there.

#### Kevin Buzzard (Mar 24 2018 at 17:12):

Hey, I now realise I don't even understand Lean's definition of nat.div and I am supposed to be a professor of number theory :-/

#### Kevin Buzzard (Mar 24 2018 at 17:13):

Maybe this was mentioned in TPIL...

#### Kevin Buzzard (Mar 24 2018 at 17:15):

Maybe it's time I read TPIL Chapter 8 again in fact.

#### Moses Schönfinkel (Mar 24 2018 at 17:21):

Coq just uses the keyword Fixpoint to express Definition that can recurse, there's not much difference from Lean's def

#### Simon Hudon (Mar 24 2018 at 17:25):

The big difference is that Lean takes care of well founded recursion for you

#### Andrew Ashworth (Mar 24 2018 at 17:29):

regarding the div example in TPIL, I wish jeremy had pattern matched on y, it would have been clearer then IMO

#### Moses Schönfinkel (Mar 24 2018 at 17:29):

Except for when it doesn't and then you're stuck with quoted tactics and such :(.

#### Moses Schönfinkel (Mar 24 2018 at 17:29):

Coq has a better solution to provin gtermination.

#### Moses Schönfinkel (Mar 24 2018 at 17:31):

Not to mention that Coq can in some cases help you show your relation is well founded. Then you're left with proof of termination only.

#### Kevin Buzzard (Mar 24 2018 at 17:31):

Right -- this is what I see with using_well_founded -- I am having to actually write a tactic (or know about the "[" trick)

#### Kevin Buzzard (Mar 24 2018 at 17:32):

The reason I currently care is that I have been reading software foundations

#### Kevin Buzzard (Mar 24 2018 at 17:32):

and I defined a positive integer as an inductive type using binary notation: three constructors one, double x and double_and_then_add_one x

#### Kevin Buzzard (Mar 24 2018 at 17:33):

and when I tried to define addition on these things, I have trouble doing (2x+1)+(2y+1)

#### Simon Hudon (Mar 24 2018 at 17:34):

regarding the div example in TPIL, I wish jeremy had pattern matched on y, it would have been clearer then IMO

A clearer way to present that definition of division can be found:

https://github.com/leanprover/lean/blob/bb9e3ddae2396b574b8ab62976bd4db9520d525d/tests/lean/run/conv_tac1.lean#L8-L13

I believe nat has access to very little tactic machinery so they have to be frugal there.

#### Andrew Ashworth (Mar 24 2018 at 17:39):

i think it's worth caring about using well_founded.fix by hand, just like no_confusion

#### Andrew Ashworth (Mar 24 2018 at 17:39):

it's applicable whenever you're doing complicated induction

#### Moses Schönfinkel (Mar 24 2018 at 17:42):

Coq just asks for proofs of well foundedness and termination (according some decreasing measure).

#### Kevin Buzzard (Mar 24 2018 at 17:42):

Yes, as an end user I forget all about this "what is the actual state of Lean when this object is being made" stuff. For example with no_confusion I was thinking "why not just return a=a' and L=L'" for list.no_confusion_type (a::L) (a'::L')

#### Moses Schönfinkel (Mar 24 2018 at 17:42):

Lean has this weird way of requiring tactics.

#### Kevin Buzzard (Mar 24 2018 at 17:42):

and then Mario points out that and might not be defined at this point. Oops.

#### Kevin Buzzard (Mar 24 2018 at 17:43):

@Moses Schönfinkel Is it only weird because you are used to the Coq way? i.e. are you saying "I don't like it because I know Coq and Lean is different", or "I don't like it because I know Coq and Lean is worse for this sort of thing"

#### Moses Schönfinkel (Mar 24 2018 at 17:51):

It's worse because you can barely see the state of what you're proving, given it's in a tactic monad. All your feedback is nested exceptions from within the quoted tactics block.

#### Moses Schönfinkel (Mar 24 2018 at 17:52):

In Coq those are first-class proofs.

#### Moses Schönfinkel (Mar 24 2018 at 17:54):

So instead of a type you need to find a term for, in Lean you're asked to provide tactics.

#### Andrew Ashworth (Mar 24 2018 at 18:00):

yes, i agree, i always end up writing out everything using well_founded.fix just so it's easier to read

#### Andrew Ashworth (Mar 24 2018 at 18:01):

i'm glad it's not just my poor Lean programming skills, haha

#### Kevin Buzzard (Mar 24 2018 at 18:11):

Would defining addition on that binary type I mentioned above be easier in Coq? How hard is it in Lean?

#### Kevin Buzzard (Mar 24 2018 at 18:12):

(the inductive type with constructors one, double and double_then_add_one)

#### Andrew Ashworth (Mar 24 2018 at 18:17):

i remember doing that exercise and trying to solve it by defining a coercion to nat. the trouble is you can have an infinite sequence of doub doub doub doub doub zero and you need to normalize the expression before you can do so

#### Kevin Buzzard (Mar 24 2018 at 18:18):

I decided that zero was a bad thing to have, I started at one

#### Kevin Buzzard (Mar 24 2018 at 18:18):

then every positive integer is uniquely represented

#### Kevin Buzzard (Mar 24 2018 at 18:18):

and there is no confusion

#### Andrew Ashworth (Mar 24 2018 at 18:19):

that's cheating! haha

#### Andrew Ashworth (Mar 24 2018 at 18:21):

the same problem arises in the construction of the integers, where the pair (1,0) is the same as (2,1), but you need some way to say they are equivalent

#### Moses Schönfinkel (Mar 24 2018 at 18:23):

I remember doing it in Coq, I am not sure if it would be at all more difficult to do in Lean.

#### Chris Hughes (Mar 24 2018 at 18:58):

I solved the problem Kevin and Andrew were talking about.

lemma  sizeof_pos : ∀ n : pint, 0  < pint.sizeof n
| one := dec_trivial
| (d m) :=  by unfold pint.sizeof; rw add_comm; exact succ_pos _
| (da m) :=  by unfold pint.sizeof; rw add_comm; exact succ_pos _

def  padd2 : pint → pint → pint
| one one := d one
| one (d m) := da m
| one (da m) := d (padd2 one m)
| (d n) one := da n
| (d n) (d m) := d (padd2 n m)
| (d n) (da m) := da (padd2 n m)
| (da n) one := d (padd2 n one)
| (da n) (d m) := da (padd2 n m)
| (da n) (da m):=  have h : 0  < pint.sizeof n, from sizeof_pos _,


The order of arguments in the final case matters, I think because in the default well-founded relation on Σ' p : pint, pint⟨one, padd2 n m⟩ ≺ ⟨da n, da m⟩ , but not necessarily ⟨padd2 n m, one⟩ ≺ ⟨da n, da m⟩ I'm not sure why it wanted me to prove sizeof n was pos however, but that was the goal that came up in the error message.

#### Mario Carneiro (Mar 24 2018 at 20:56):

@Kevin Buzzard You should look at mathlib num type, which is binary naturals just as you are describing. You don't need wf recursion for any of the definitions

#### Andrew Ashworth (Mar 24 2018 at 21:33):

yeah, iirc that exercise asks you to define nat_to_bin and bin_to_nat. Once you've proven there is a bijection between the binary naturals and the"traditional" naturals, you can use nat addition on the binary numbers

#### Andrew Ashworth (Mar 24 2018 at 21:33):

this is hard to do if you don't have zero

#### Kevin Buzzard (Mar 24 2018 at 21:38):

it's harder to do if you do have zero

#### Kevin Buzzard (Mar 24 2018 at 21:38):

because double double double zero is zero

#### Kevin Buzzard (Mar 24 2018 at 21:38):

so bijectivity fails much worse

#### Kenny Lau (Mar 24 2018 at 21:39):

bijective binary to the rescue

#### Kenny Lau (Mar 24 2018 at 21:39):

ok it's literally inside the name

#### Andrew Ashworth (Mar 24 2018 at 21:40):

yeah, handling the doub doub doub zero case is the real trick to the problem

#### Kenny Lau (Mar 24 2018 at 21:41):

or you can just surject to the naturals and quotient

#### Andrew Ashworth (Mar 24 2018 at 21:41):

i solved it a long time ago, let me see if i can find my solution, maybe...

#### Kenny Lau (Mar 24 2018 at 21:41):

literally a~b iff f(a)=f(b)

(deleted)

#### Kevin Buzzard (Mar 24 2018 at 21:43):

I only defined the map one way. Did it ask you for the other way later on?

#### Andrew Ashworth (Mar 24 2018 at 21:44):

so, it seems they've made many of the exercises different / a little easier in the new edition

#### Andrew Ashworth (Mar 24 2018 at 21:45):

the original problem was a 4 star advanced take you all day to complete if you're a learner hair-raiser

#### Andrew Ashworth (Mar 24 2018 at 21:45):

at least it was for me

#### Andrew Ashworth (Mar 24 2018 at 21:47):

which is why i remember some of the details about it

#### Kevin Buzzard (Mar 24 2018 at 21:48):

They dumbed down for the kids?

#### Andrew Ashworth (Mar 24 2018 at 21:49):

not too badly! and i agree with dumbing it down, it's an introductory text

#### Andrew Ashworth (Mar 24 2018 at 21:50):

i can't imagine teaching yourself from the original software foundations without guidance or help

#### Andrew Ashworth (Mar 24 2018 at 21:50):

i eventually found somebody's homework solutions online and figured out how to solve it

ahh, yes

#### Andrew Ashworth (Mar 24 2018 at 21:57):

http://staff.ustc.edu.cn/~bjhua/courses/theory/2012/slides/lec1notes.html

#### Andrew Ashworth (Mar 24 2018 at 21:58):

once you've normalized your binary number, then you can create a bijection, and life is good again

#### Andrew Ashworth (Mar 25 2018 at 00:36):

literally a~b iff f(a)=f(b)

if only i had known at the time. they didn't talk much about equivalence relations in engineering school

#### Andrew Ashworth (Mar 25 2018 at 00:39):

and if SF had started talking about how bin_to_nat was onto but not one-to-one, I doubt many undergraduates would know what that really meant

#### Kevin Buzzard (Mar 25 2018 at 00:40):

That's funny. I teach that to maths undergraduates in year 1 term 1. And equivalence relations.

#### Simon Hudon (Mar 25 2018 at 00:41):

I remember learning that in first year of university too, in discrete math

#### Andrew Ashworth (Mar 25 2018 at 00:42):

i never had to take discrete math, I was an electrical engineer

#### Simon Hudon (Mar 25 2018 at 00:42):

(I did CS and not engineering though, if that makes a difference)

#### Andrew Ashworth (Mar 25 2018 at 00:42):

instead there was a 2 semester sequence on fourier transforms

#### Andrew Ashworth (Mar 25 2018 at 00:43):

where we basically learned very little theory and a lot of how to compute various integrals

#### Andrew Ashworth (Mar 25 2018 at 00:43):

i may have mentioned this before but i have issues with how they teach math in engineering school :)

#### Simon Hudon (Mar 25 2018 at 00:47):

It seems common that people who like math don't get enough of it in engineering school.

#### Andrew Ashworth (Mar 25 2018 at 00:48):

yes, we get a lot of boring computation instead

#### Andrew Ashworth (Mar 25 2018 at 00:48):

my linear algebra class was basically doing a lot of gauss-jordan elimination and calculating eigenvectors by hand

#### Andrew Ashworth (Mar 25 2018 at 00:49):

which ends up being completely a waste of time since no working engineer would ever do these things without a computer

#### Simon Hudon (Mar 25 2018 at 00:50):

Mine was like that too. I've never missed my calculator more than in that class

#### Simon Hudon (Mar 25 2018 at 00:52):

The follow up class was about numerical methods for linear algebra so I guess I should have been happy to do some implementation. I was not easy to satisfy I guess

Last updated: May 14 2021 at 02:15 UTC