Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Apr 16 18:25
    Tuplanolla commented #364
  • Apr 16 15:12
    mattam82 commented #364
  • Apr 16 15:10
    Tuplanolla commented #364
  • Apr 16 14:52
    mattam82 commented #364
  • Apr 16 14:45
    mattam82 commented #364
  • Apr 16 14:37
    mattam82 commented #335
  • Apr 16 14:37
    mattam82 commented #335
  • Apr 16 14:18
    Lysxia commented #335
  • Apr 16 13:05
    Tuplanolla opened #364
  • Apr 16 12:40
    gares commented #321
  • Apr 16 12:40
    gares commented #321
  • Apr 16 12:40
    gares commented #321
  • Apr 16 11:13
    kyoDralliam commented #321
  • Apr 16 08:59
    mattam82 commented #329
  • Apr 16 08:55

    mattam82 on fix-335

    (compare)

  • Apr 16 08:55

    mattam82 on master

    Fix issue #335: add an alias "E… Merge pull request #363 from ma… (compare)

  • Apr 16 08:55
    mattam82 closed #363
  • Apr 16 08:54
    mattam82 commented #335
  • Apr 16 08:50
    mattam82 synchronize #363
  • Apr 16 08:50

    mattam82 on fix-335

    Fix issue #335: add an alias "E… (compare)

Jad Hamza
@jad-hamza
Yes you're right that might cause the difference, but simp_red is often used within repeat
Jad Hamza
@jad-hamza
(I tried with this change https://github.com/epfl-lara/SystemFR/pull/11/files, still faster than the autorewrite version)
Paolo G. Giarrusso
@Blaisorblade
(any chance you need repeat also on the other variants of those tactics?) But Robbert Krebbers has complained about autorewrite performance a lot, but it being slower than repeat rewrite is surprising.
(surprising to me)
(maybe performance of autorewrite is best discussed in coq/coq? For instance, Jason Gross has been working on rewriting tactics and comparing with rewrite_strat)
Paolo G. Giarrusso
@Blaisorblade
maybe unrelated: IIRC, Equations uses Opaque which is ignored by some tactics, and by conversion checking. I wonder if something like stdpp’s sealing https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/base.v#L42 would be better (see https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/namespaces.v#L11 for the use pattern).
that relies on Qed, which is actually Opaque, and it allows you to give a definition which is actually equal to its body only propositionally and not definitionally.
Jad Hamza
@jad-hamza
Thanks! Moving there
Matthieu Sozeau
@mattam82
You might indeed want a more refined rewrite strategy (using rewrite_strat)
I think autorewrite does not bypass opacity though
But I might be wrong :)
Jad Hamza
@jad-hamza
rewrite_strat indeed worked well! (and faster than repeat rewrite) after a few adjustments (importing RelationClasses and defining a few missing instances)
Paolo G. Giarrusso
@Blaisorblade
@jad-hamza oh, is rewrite_strat just faster or do you need to do optimizations yourself? I use Autosubst which uses autorewrite, and its performance is annoying
Jad Hamza
@jad-hamza
I think it was faster out of the box (using this: https://github.com/epfl-lara/SystemFR/blob/7eff4ae12a8441001f49c58f3dea93758e78090f/ReducibilityDefinition.v#L213-L225), but I cannot tell for sure because some proofs didn't go through automatically and I had to do adjustments. There seems to be a difference with rewrite in *, which doesn't rewrite under binders while rewrite_strat maybe does? So I ended up using variants in these places such as simp_red_top_level_hyp, which will only rewrite top level occurrences. After all these changes (in commit epfl-lara/SystemFR@7eff4ae), the build using make -j10 went from around ~12min45 to ~11min20 (I didn't run these many times so these times may be off). Also, I didn't try other strategies (topdown or bottomup or innermost). Tell me your results if you try something :)
Paolo G. Giarrusso
@Blaisorblade
ah, there's coq/coq#6105 on this
Matthieu Sozeau
@mattam82
rewrite_strat uses congruence lemmas and produces smaller proof terms a priori, but indeed it's not 100% the same as autorewrite's strategy which is just repeat rewrite
Bas Spitters
@spitters
Idris2 has some cool technology to generate programs from a type. Apparently, it originated here:
https://hackage.haskell.org/package/djinn
has anyone looked at porting it to Coq?
Paolo G. Giarrusso
@Blaisorblade
isn’t that based on a foundation similar to tauto? if so, is there any significant difference in engineering?
in particular, they're both based on decision procedures for LJT by Roy Dyckhoff (as Augustsson describes e.g. in http://lambda-the-ultimate.org/node/1178; https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.tauto); but I could easily miss some subtlety...
Bas Spitters
@spitters
Yes, I think the basic algorithms are there, and one could hope that it can be put together cheaply, but I haven't looked into it deeply, as I would expect someone has done so already.
Karl Palmskog
@palmskog
applications seem to be quite limited, basically a special case of synthesis
something like Isabelle's Nitpick would be more valuable, and solves a similar problem
Bas Spitters
@spitters
Edwin referred to it as a "magic trick". Jasmin has been promising nitpick for DTT for some time, but I could find much progress. Do you happen to know more?
Karl Palmskog
@palmskog
@spitters Nunchaku is still being worked on by Jasmin's collaborator: https://github.com/nunchaku-inria/nunchaku
but no Coq integration available to my knowledge
it wouldn't surprise me if they do Lean integration first, since that's what Jasmin's current project targets
Bas Spitters
@spitters
That project doesn't seem very active
Karl Palmskog
@palmskog
the main author is in industry these days
to be honest, I don't think any focused efforts will happen (w.r.t. counter-example generation and synthesis etc.) for Coq unless someone gets specific funds for it, I would say postdoc level for 1+ year or something like that
Jasmin has one postdoc working on tools part-time (Gabriel Ebner), but my understanding is he mostly works on the hammer for Lean
Bas Spitters
@spitters
Would a hammer for lean be fundamentally different from a hammer for Coq?
Karl Palmskog
@palmskog
it looks like they chose to implement it quite differently
I think the most design choices are in how to map the type theory to TPTP format and how to do reconstruction
for CoqHammer, they (Kalizcyk and Csajka) chose to implicitly use an intermediate calculus "CIC0" and write custom reconstruction tactics
I think Jasmin and Gabriel are following Sledgehammer more closely
they also implement it in C++ to hook into Lean's implementation: https://leanprover-community.github.io/archive/113488general/28743Hammertalk.html
ah right, they target HOL instead of CIC0 it seems
Théo Winterhalter
@TheoWinterhalter

I’m trying to port an old project from coq 8.8 and I seem to have problems with Equations.
For instance

Derive NoConfusion for nat.

gives off the warning

Solve Obligations tactic returned error: Tactic failure: Equations.Init.solve_noconf has not been bound yet.
This will become an error in the future [solve_obligation_error,tactics]

twice.
And it leaves me to prove no confusion myself.

I import Equations with

From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.

and use 1.2.1+8.11

I guess I’m missing something but I can’t figure it out. If someone knows, thanks. :)
Matthieu Sozeau
@mattam82
Swap the imports
It messes with tactic redéfinitions
Théo Winterhalter
@TheoWinterhalter
Oh… It’s that simple, thanks!
Cyril Cohen
@CohenCyril
Hi, I am in the process of exporting gitter channels (public) data to zulip, (it can be done only once, during the creation of the zulip chatroom), do you wish that I export the data of this channel too?
Matthieu Sozeau
@mattam82
Yes
@CohenCyril
PLBegay
@PLBegay
Hi everyone, when trying to install coq-equations 1.2+8.9 or 1.2.1+8.9 via opam on two different computers, I get an error (the sources couldn't be obtained, curl error code 500). I did add the https://coq.inria.fr/opam/released repo and I'm pretty sure it was working yesterday. Thanks in advance !
Paolo G. Giarrusso
@Blaisorblade
@PLBegay releases are hosted on GitHub and GitHub was down. Please try again now that GitHub is up.
PLBegay
@PLBegay
@Blaisorblade It indeeds works like a charm now, thanks!
Cyril Cohen
@CohenCyril
Dear @/all the gitter data from May 6 at 4:24 has been imported in a new zulip chat.
I need a mapping from your user github name to your email for you to recover your account. Please click on my picture, then "Chat Privately", then type: /me your-email-adress@yourprovider.org. This mail should be associated with your gitter account
I will notify you when you have access, it takes a guy on PDT timezone to answer my mail, I send him batches of username->mail as I receive the data from you guys.