Vleeptron wishes Earth, Hoon, Mollyringwald, Yobbo & BjörkGuðmundsdóttir High Holy Days & Merry Christmas / J******* x E*** x H*** want to skolemize all the evars / parse this early draft of "Lucky's Speech" from "Waiting for Some Guy" / Greeks don't say "It's all Greek to me" that would make no sense / ipse dixit

Click to enlarge

Leave A Comment.  No Belize real estate or viagra ads pls. No Anonymous Driveby Comments. Show some credible kind of i.d. or link to an authentic living carbon-based sentient.

Gibberish and surrealism, Pataphysics/Pataphysique, Anagrams Puns & Ciphers (with or without fabulous treasure upon solution) welcome. Stop making sense. Wear a big suit.

But 4 slices mozzerella endives & shallots if your Comment

* treats this as a Real Meme in Our World and

* pretty accurately describes what J******* & E*** & H*** are  rapping about. There's no quiz on this stuff tomorrow morning, just pizza for the deserving.

HINT: Sentients what talk like this all the time like to convene in beachfront resorts in Cyprus (Larnaca and Limasol) during MY brutal New England winter. I see a seminar by around February. I see tall iced drinks with little parasols poolside.

*****************************

Thanks for your help, J*******.

Is there any way to search a term to find all the evars in it, so I can skolemize all of them? I would like to do something like this, where R is a typeclass that only has an instance for non-dependent function types:

Ltac prove_R :=
  lazymatch goal with
  | |- R (forall x:?A, ?B) => skolemize_all_evars B; apply R_nondep_fun_instance
  end.

Thanks again,
-E***

> On Dec 2, 2016, at 1:15 PM, J******* L****** wrote:
> On 12/02/2016 03:50 PM, E*** W******** wrote:

J*******
>>
>> Thanks for the reply, and for the suggested workaround. I’ll see if I can get something like that to work.
>>
>> The reason this looks like a bug to me, though, is that I think, if I’m not mistaken, that what I am actually trying [to] solve is the problem
>>
>> ?T2 x = ?B
>
> FYI - You can "skolemize" ?T2 with respect to x in the goal by doing this:
>
> Goal { T:Type | T=T }.
>  refine (exist _ (forall (x:?[T1]), ?[T2]) _).
>  instantiate (T2:=ltac:(revert x)). (*skolemize ?T2 wrt x*)
>
>>
>> (Technically, I think Coq writes the left-hand side as something like ?T2@{__:=x}, but it’s the same thing.) This problem has the solution ?T2 = (fun _ => ?B). It falls into the higher-order pattern fragment, since ?T2 is fully applied to distinct bound variables, and I thought Coq would solve this fragment.
>
> I don't think Coq can solve such fragments.
>
>>
>> Also, either way, the fact that the unify tactic is not commutative also seems like a bug...
>
> I think the problems with commutativity of unification with evars is a known issue that H*** has attempted to (and is continuing to attempt to) deal with.
>
> -- J*******
>