Polymorphism and subordination

[Todd Wilson]

What exactly is the relationship between polymorphism and subordination? For example,

Kind t type.
% Close t.

Theorem member_prune[A] : forall E (L:list A), nabla (x:A),
  member (E x) L -> exists E', E = y\E'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

succeeds, but if I uncomment the `Close t.` command, then it fails with

Error: Pre-condition of subordination check is violated: target type cannot be a variable

Todd Wilson

[Todd Wilson]

I should have added that it's clear that there could be a problem if `A` were instantiated with `t`, but I haven't instantiated it yet. Couldn't the error message be invoked only when I try to instantiate `A` to `t`, which I would generally avoid, instead of being invoked if I use any subordination in my development at all? Going even further, what's actually wrong with `member_prune[t]`? Under the subordination declaration, this theorem should be vacuously true, since the only `E` that it could be applied to would already be a constant function. (Yes, I know that polymorphic theorems need parametric proofs, but ...)

[Kaustuv Chaudhuri]

Dear Todd,

If this isn't a bug, it's certainly a weird interaction that should be documented. I've made a new issue for it on Github:

https://github.com/abella-prover/abella/issues/144

Anything having to do with schematic polymorphism comes from Yuting and Gopalan originally, so maybe they can explain if this behavior makes sense. From my perspective, I'm happy to treat this as a bug, since obviously the type t can be introduced after the theorem is proved!

Kaustuv

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/abella-theorem-prover/4f296dbf-b35a-4a29-ad71-5e713363e277n%40googlegroups.com.