nearly no_confusion

Stream: general

[Kevin Buzzard]

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]

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]

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]

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]

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]

was mcbride's paper on no confusion not helpful?

[Kevin Buzzard]

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]

https://pdfs.semanticscholar.org/d224/e96c59a81a471625faf87118b6299094e1e4.pdf section 7.3

[Andrew Ashworth]

http://strictlypositive.org/thesis.pdf page 136

[Andrew Ashworth]

mcbride's phd thesis is definitely hard going

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

I'll perhaps add some comments about what you said above, later.

[Mario Carneiro]

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]

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]

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]

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]

Aah excellent, I will beef up the post tomorrow

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

#print  prefix mystery

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

#print  prefix bool'

[Kevin Buzzard]

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]

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]

for example:

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

wouldn't make sense because of proof irrelevance

[Kevin Buzzard]

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]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

I know even less about well_founded.fix.

[Andrew Ashworth]

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

[Andrew Ashworth]

it's a way of expressing well-founded induction

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Maybe this was mentioned in TPIL...

[Kevin Buzzard]

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

[Moses Schönfinkel]

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

[Simon Hudon]

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

[Andrew Ashworth]

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

[Moses Schönfinkel]

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

[Moses Schönfinkel]

Coq has a better solution to provin gtermination.

[Moses Schönfinkel]

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]

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]

I don't know whether as a mathematician I should care about this

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Simon Hudon]

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]

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

[Andrew Ashworth]

it's applicable whenever you're doing complicated induction

[Moses Schönfinkel]

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

[Kevin Buzzard]

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]

Lean has this weird way of requiring tactics.

[Kevin Buzzard]

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

[Kevin Buzzard]

@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]

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]

In Coq those are first-class proofs.

[Moses Schönfinkel]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Andrew Ashworth]

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]

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

[Kevin Buzzard]

then every positive integer is uniquely represented

[Kevin Buzzard]

and there is no confusion

[Andrew Ashworth]

that's cheating! haha

[Andrew Ashworth]

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]

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

[Chris Hughes]

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 _,
d (padd2 one (padd2 n m))

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]

@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]

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]

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

[Kevin Buzzard]

it's harder to do if you do have zero

[Kevin Buzzard]

because double double double zero is zero

[Kevin Buzzard]

so bijectivity fails much worse

[Kenny Lau]

bijective binary to the rescue

[Kenny Lau]

ok it's literally inside the name

[Andrew Ashworth]

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

[Kenny Lau]

or you can just surject to the naturals and quotient

[Andrew Ashworth]

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

[Kenny Lau]

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

[Kenny Lau]

(deleted)

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

at least it was for me

[Andrew Ashworth]

which is why i remember some of the details about it

[Kevin Buzzard]

They dumbed down for the kids?

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

ahh, yes

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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]

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]

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

[Simon Hudon]

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

[Andrew Ashworth]

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

[Simon Hudon]

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

[Andrew Ashworth]

instead there was a 2 semester sequence on fourier transforms

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Simon Hudon]

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

[Andrew Ashworth]

yes, we get a lot of boring computation instead

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Simon Hudon]

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

[Simon Hudon]

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