[POPLmark] Experience report with Twelf

[Dan Licata]

Sorry, I was unclear.

All I was suggesting was that the implies-false-premised rule was a
quick solution under the assumptions that (a) you want decidability of
subtyping as an extra premise or as an unproven metatheorem and (b) all
you ever want to do with a not-subtyping derivation is contradict a
subtyping one.  I didn't mean to suggest that it was a better solution
than coding up the negation and proving exclusivity.  Whenever I've run
into these sorts of things, I've defined the not-X judgement directly.

So, we agree.

-Dan

On Aug18, Stephanie Weirich wrote:
> Dan Licata wrote:
> 
> >>A side note: I don't think that this is exactly the law of the
> >>excluded middle. I think it says something like "at least one of the
> >>'subtyping' and 'notsubtyping' judgments are derivable." 
> >>   
> >>
> >
> >The law of the excluded middle is usually phrased as (A or not(A)),
> >which corresponds in this instance to the phrase in quotes above.
> >
> > 
> >
> <rest snipped>
> 
> I think we dis agree on what the definition of not-subtype should be, 
> and that makes all of the difference.
> You propose the following definition:
> 
> >not-subtyping-contra : not-subtyping A B
> >		       <- (subtyping A B -> false).
> 
> where I define non-subtyping without relation to the subtyping 
> judgement. (Technically, a judgments that
> holds when two types aren't subtypes of one another.)   That's why  the 
> subtyping-exclusive lemma
> 
> >>subtyping-exclusive: subtyping A B -> not-subtyping A B -> false ->  
> >>type.
> >>   
> >>
> is necessary to make it clear that both of these judgments can't hold.  
> (It is true by definition for your version.).
> 
> However, I prefer my definition of not-subtyping because with your 
> definition, the excluded middle lemma
> is not provable in Twelf---there is no LF canonical form of type 
> (subtyping A B -> false). Even though I
> originally wanted to assert the decidablity of subtyping, since 
> subtyping *is* in fact decidable, it makes sense for me to
> assert it in a way that could eventually be proven in Twelf.
> 
> >>
> >>lookupClass_strengthen :
> >>  ({x:exp} lookupClass CT C (class C D FS (MT x)))
> >>    -> lookupClass CT C (class C D FS (MT unit)) -> type.
> >>
> >>However, I think this is a case where strengthening is unavoidable.
> >>The type exp is subordinate to the type methodTable, but since the
> >>methodTable MT comes from the classTable CT (which does not depend on
> >>x) in this case, it can't depend on x.
> >>   
> >>
> >
> >This could be a property of the system you're formalizing, not just
> >the LF encoding.  That is, on paper, how do you *know* that the class
> >you get back doesn't mention some variable in the context?  Sometimes
> >I've glossed over things like this on paper only to have Twelf point
> >them out to me.
> > 
> >
> This issue didn't come up in either the Coq version of the proof (that I 
> did) or the Isabelle/HOL version
> (that two grad students here at Penn did).
> 
> --Stephanie
>