## Stream: general

### Topic: qpf/no_confusion

#### matt rice (Apr 17 2019 at 19:27):

sorry for the millions of qpf questions, a bit stuck on this one
This was originally about another data type, but I figured it would be easiest to just reformulate under option

I have this little proof here, (on the normal lean inductive option), which I didn't see in mathlib or core btw

import data.option.basic

def option.neq_of_none_some {α : Type} {x : α}
: (option.none) ≠ (option.some x)
:= λ h, option.no_confusion h


I had managed to get it working relatively unscathed with the qpf parser

import data.fix.parser.equations
universe u

namespace opt'
qpf opt' (α : Type)
| none : opt'
| some : α → opt'

def opt'.neq_of_none_some {α : Type} {x : α}
: (opt'.none α) ≠ (opt'.some x)
:= λ h, opt'.no_confusion h
end opt'


When i tried to change qpf opt' (α : Type) into data opt (α : Type)
The no_confusion function is then derived under opt.shape.no_confusion,
but the signature has changed to accepting an equality between opt.shapes rather.

I haven't figured out how to go from the original equality into the shape one (see the sorry below).

namespace opt
data opt (α : Type)
| none : opt
| some : α → opt

#check @opt.shape.no_confusion
def opt.neq_of_none_some {α : Type} {x : α}
: (opt.none α) ≠ (opt.some α x)
:= (λ h,
have h' : opt.shape.none α α = opt.shape.some α x,
by sorry,
opt.shape.no_confusion h')
end opt


#### Simon Hudon (Apr 17 2019 at 19:46):

I don't think we generate no_confusion for the data types yet but it should be fairly easy to add it because I already have code that does that. I can create a branch with code if you like. I'm trying to not touch the master branch at the moment so that it can serve as a stable state for the reviewer of my paper.

#### matt rice (Apr 17 2019 at 19:52):

I can just leave it as a sorry for now, but a branch would be fine too, either way

#### Simon Hudon (Apr 17 2019 at 20:23):

Ok, I'll get on it and let you know when it's usable

Last updated: May 15 2021 at 23:13 UTC