Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC