6 ms·

https://github.com/Odomontois/Tincat https://github.com/Odomontois/Tincat Not exactly you asked for but the only one I know.

tom_mellior 7y ago
Thanks. The only lemma in that repo is the following (in Cat.ard): \lemma op_is_revertible (C : PreCat) : op (op C) = C => path ( \lam i => \new PreCat { | Ob => C.Ob | Hom => C.Hom | id => C.id | o => C.o | l_unit => C.l_unit | r_unit => C.r_unit | assoc => \lam {a} {b} {c} {d} f g h => (inv_inv (C.assoc f g h) @ i) } ) I'm not 100% sure what's going on but it looks like this would be a one-liner in Coq, something like (hand-waving here): destruct C; auto using assoc, inv_inv. So... yeah. Not enough data to come to a final conclusion, but I do wonder why people keep building more systems of this kind.
- syrak 7y ago
  > I do wonder why people keep building more systems of this kind. Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're missing in Isabelle and Coq. That's also orthogonal to the matter of automation/metaprogramming, which, from the lack of mention, doesn't seem to be their focus right now. There doesn't seem to be anything fundamentally in the way of Coq-style tactics either if they really wanted to build that on top of what is presented here.
  - tom_mellior 7y ago
    True, there are probably no theoretical obstacles. But there is a huge implementation effort, and judging from other new proof assistants that started out without tactics, I wouldn't hold my breath. Unless you desperately need exactly this kind of fancy logic, if you actually want to get stuff done, you would choose a different system. That's not great if they are interested in wide adoption.
- naasking 7y ago
  Coq with tactics does not fair particularly well on anything more than toy examples: https://www.cister.isep.ipp.pt/docs/experimental_evaluation_of_formal_software_development_using_dependently_typed_languages/1534/view.pdf https://www.cister.isep.ipp.pt/docs/experimental_evaluation_... Better tools are still needed, so people really should be building more systems of this kind.
  - tom_mellior 7y ago
    > Coq with tactics does not fair particularly well on anything more than toy examples Actual citation from the paper or some other source needed. Relevant-ish citations from the paper: 1. "Coq uses interactive tactics to prove goals, which is veryconvenient, but may lead to large proof scripts in case onedoes ad-hoc proofs. But Coq also has the tools to make theproofs concise, provided one works in a fixed domain, andcreates the necessary abstractions." 2. "In [50] Wadler states“Proofs in Coq require an interactiveenvironment to be understood, while proofs in Agda canbe read on the page.”, while this is true for the languagesthemselves, but Proviola [49] can alleviate this problem ofCoq, by recording the proof state after each tactic execution,and producing an html document with the proof state addedfor each tactic. F* does not have this problem, as the proofterms do not appear either in the source, or during proving.Whether it is easier to read complete proof terms, or thereplay of a step by step creation of a proof term is dependentof the task at hand, but the author thinks, that it is morestraightforward to create scripts step by step in Coq, thoughit does require discipline on the programmer’s part, so as tonot create a write-only script" Are you basing your very wide claim on one of these that don't say what you're saying, or did I overlook one? Anyway, there's CompCert (http://compcert.inria.fr/ http://compcert.inria.fr/) and Iris (https://iris-project.org/ https://iris-project.org/) and Kami (http://plv.csail.mit.edu/kami/papers/icfp17.pdf http://plv.csail.mit.edu/kami/papers/icfp17.pdf) and many other projects of non-toy size implemented in Coq, so I don't quite know what else to say to convince you. Sure, tactic scripts can be hard to read and next to impossible to skim. The same goes for direct proof terms. > Better tools are still needed Agreed.
    - naasking 7y ago
      Take a look at how much trouble the author had finding a working ST, despite there being widely published and used libraries at some point but which no longer work in newer versions of Coq. The author ended up using a very specific git hash version of the Iris library, and he admits the documentation of Iris is pretty much non-existent. This doesn't inspire confidence, considering this author is also the most familiar with Coq of the three. He also somehow claims that Coq is stable, which I can only take to mean that it won't crash rather than that it largely preserves backwards compatibility given his difficulties. If we can't rely on some measure of backwards compatibility so we can build on stable libraries, theorem proving simple won't scale any more than programming of any kind won't scale in the same circumstances. The number of lines of code required for the second task also doesn't inspire confidence that theorem proving with Coq will scale. So I frankly can't see any reason to think that Coq even with tactics is a viable approach to real world verification beyond exploratory toy examples. No doubt we have different goals in mind when it comes to verification/theorem proving, which is why you think Coq is suitable and I do not.
- Odomontois 7y ago
  This repo was my first learning project. I barely knew Idris, and have no experience with HoTT. Please don't judge the language referring to this. You can refer nice code here https://github.com/JetBrains/arend-lib https://github.com/JetBrains/arend-lib
- Odomontois 7y ago
  The "only" lemma is because other lemmas are defined via \func I've learned about \lemma and \property and HoTT precategories and univalent categories not so long ago. Now I'm planning to rewrite all of this from scratch

tom_mellior 7y ago

Thanks. The only lemma in that repo is the following (in Cat.ard): \lemma op_is_revertible (C : PreCat) : op (op C) = C => path ( \lam i => \new PreCat { | Ob => C.Ob | Hom => C.Hom | id => C.id | o => C.o | l_unit => C.l_unit | r_unit => C.r_unit | assoc => \lam {a} {b} {c} {d} f g h => (inv_inv (C.assoc f g h) @ i) } ) I'm not 100% sure what's going on but it looks like this would be a one-liner in Coq, something like (hand-waving here): destruct C; auto using assoc, inv_inv. So... yeah. Not enough data to come to a final conclusion, but I do wonder why people keep building more systems of this kind.

syrak 7y ago
> I do wonder why people keep building more systems of this kind. Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're missing in Isabelle and Coq. That's also orthogonal to the matter of automation/metaprogramming, which, from the lack of mention, doesn't seem to be their focus right now. There doesn't seem to be anything fundamentally in the way of Coq-style tactics either if they really wanted to build that on top of what is presented here.
- tom_mellior 7y ago
  True, there are probably no theoretical obstacles. But there is a huge implementation effort, and judging from other new proof assistants that started out without tactics, I wouldn't hold my breath. Unless you desperately need exactly this kind of fancy logic, if you actually want to get stuff done, you would choose a different system. That's not great if they are interested in wide adoption.
naasking 7y ago
Coq with tactics does not fair particularly well on anything more than toy examples: https://www.cister.isep.ipp.pt/docs/experimental_evaluation_of_formal_software_development_using_dependently_typed_languages/1534/view.pdf https://www.cister.isep.ipp.pt/docs/experimental_evaluation_... Better tools are still needed, so people really should be building more systems of this kind.
- tom_mellior 7y ago
  > Coq with tactics does not fair particularly well on anything more than toy examples Actual citation from the paper or some other source needed. Relevant-ish citations from the paper: 1. "Coq uses interactive tactics to prove goals, which is veryconvenient, but may lead to large proof scripts in case onedoes ad-hoc proofs. But Coq also has the tools to make theproofs concise, provided one works in a fixed domain, andcreates the necessary abstractions." 2. "In [50] Wadler states“Proofs in Coq require an interactiveenvironment to be understood, while proofs in Agda canbe read on the page.”, while this is true for the languagesthemselves, but Proviola [49] can alleviate this problem ofCoq, by recording the proof state after each tactic execution,and producing an html document with the proof state addedfor each tactic. F* does not have this problem, as the proofterms do not appear either in the source, or during proving.Whether it is easier to read complete proof terms, or thereplay of a step by step creation of a proof term is dependentof the task at hand, but the author thinks, that it is morestraightforward to create scripts step by step in Coq, thoughit does require discipline on the programmer’s part, so as tonot create a write-only script" Are you basing your very wide claim on one of these that don't say what you're saying, or did I overlook one? Anyway, there's CompCert (http://compcert.inria.fr/ http://compcert.inria.fr/) and Iris (https://iris-project.org/ https://iris-project.org/) and Kami (http://plv.csail.mit.edu/kami/papers/icfp17.pdf http://plv.csail.mit.edu/kami/papers/icfp17.pdf) and many other projects of non-toy size implemented in Coq, so I don't quite know what else to say to convince you. Sure, tactic scripts can be hard to read and next to impossible to skim. The same goes for direct proof terms. > Better tools are still needed Agreed.
  - naasking 7y ago
    Take a look at how much trouble the author had finding a working ST, despite there being widely published and used libraries at some point but which no longer work in newer versions of Coq. The author ended up using a very specific git hash version of the Iris library, and he admits the documentation of Iris is pretty much non-existent. This doesn't inspire confidence, considering this author is also the most familiar with Coq of the three. He also somehow claims that Coq is stable, which I can only take to mean that it won't crash rather than that it largely preserves backwards compatibility given his difficulties. If we can't rely on some measure of backwards compatibility so we can build on stable libraries, theorem proving simple won't scale any more than programming of any kind won't scale in the same circumstances. The number of lines of code required for the second task also doesn't inspire confidence that theorem proving with Coq will scale. So I frankly can't see any reason to think that Coq even with tactics is a viable approach to real world verification beyond exploratory toy examples. No doubt we have different goals in mind when it comes to verification/theorem proving, which is why you think Coq is suitable and I do not.
Odomontois 7y ago
This repo was my first learning project. I barely knew Idris, and have no experience with HoTT. Please don't judge the language referring to this. You can refer nice code here https://github.com/JetBrains/arend-lib https://github.com/JetBrains/arend-lib
Odomontois 7y ago
The "only" lemma is because other lemmas are defined via \func I've learned about \lemma and \property and HoTT precategories and univalent categories not so long ago. Now I'm planning to rewrite all of this from scratch