qpf/no_confusion

Stream: general

[matt rice]

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]

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]

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

[Simon Hudon]

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