Stack Exchange
log in sign up chat discuss faq users badges

Area 51 » Science

definition commitment beta
238
followers

This proposal is now in the Beta phase — example questions are locked!

64 Example Questions

active newest votes
up vote 7 down vote
I need to compare two records with a semantic property for equality in Coq. What do I do with the proof-component?
added by Volker Stolz Nov 20 '21 at 9:08
link
up vote 5 down vote
Are there any tutorials to write a proof assistant from scratch?
added by Pedro Abreu Nov 20 '21 at 14:13
link
Probably a duplicate of area51.stackexchange.com/proposals/126242/… – k4rtik Nov 20 '21 at 20:13
up vote 5 down vote
Does propositional truncation in HoTT erase information?
added by Martín Hötzel Escardó Nov 20 '21 at 16:33
link
up vote 4 down vote
Could proof assistants be used to prove that some piece of code is free of bugs?
added by Glorfindel Nov 20 '21 at 18:37
link
up vote 3 down vote
What proof assistants are completely based on lambda-encodings?
added by Rígille Nov 20 '21 at 2:06
link
up vote 3 down vote
As a new user of coq, my proofs often look clunky with low readability unlike my programs. Is there a good reference to setup clean tactics for this
added by mycroft92 Nov 20 '21 at 17:51
link
up vote 2 down vote
Results about the lattice of topologies on a type aren't syntactically right to do rewrites with my topology typeclass. Is there a way around this?
added by Kyle Miller Nov 19 '21 at 23:09
link
up vote 2 down vote
Can Agda proofs be trusted and do they conform to a specific, well-defined type theory?
added by Martín Hötzel Escardó Nov 20 '21 at 16:19
link
up vote 2 down vote
Which proof assistants support HoTT/UF and how to they compare?
added by Martín Hötzel Escardó Nov 20 '21 at 16:38
link
up vote 2 down vote
How does Coq's Prop compare to Agda's Prop?
added by Nicolai Kraus Nov 20 '21 at 17:05
link
up vote 2 down vote
What proof assistants would be a good choice for teaching programming language theory in an undergraduate class?
added by Jonathan Aldrich Nov 20 '21 at 20:11
link
up vote 1 down vote
Similar to the massive library of formalised mathematics in LEAN, is there a library of formalised & proved algorithms in any of the proof assistants?
added by Art Nov 20 '21 at 8:33
link
up vote 1 down vote
When using the `induction ... using FOO` tactic in Coq, what is restrictions are placed on the `FOO` Prop?
added by illabout Nov 20 '21 at 13:58
link
up vote 1 down vote
What advantages do some proof assistants have over others? Are some better suited for some topics (like analysis) than others?
added by Wojowu Nov 20 '21 at 14:36
link
1  
I think a more specific question, e.g, just about analysis, would be better. – James Wood Nov 20 '21 at 18:31
up vote 1 down vote
Is propositional resizing well supported by existing proof assistants? Without it makes subsets somewhat awkward from a mathematician's view.
added by Kang Rongji Nov 20 '21 at 16:24
link
up vote 1 down vote
What are the advantages of HoTT's hProp over Coq's Prop?
added by Martín Hötzel Escardó Nov 20 '21 at 16:26
link
up vote 1 down vote
Is the `simp` system of Lean's mathlib a confluent rewriting system?
added by user216861 Nov 20 '21 at 20:17
link
up vote 0 down vote
Is there a way to use Haskell-style infix combinators like ($) and (.) in Coq? Why aren't these part of the Coq Prelude?
added by Agnishom Chattopadhyay Nov 20 '21 at 18:58
link
up vote 0 down vote
Do any proof-assistants make use of Gabbay and Pitts' nominal approach to variable binding and abstract syntax based on FM sets?
added by buraq Nov 20 '21 at 20:32
link
up vote 0 down vote
What are the differences when it comes to including classical reasoning in the most common proof-assistants?
added by Lereau Nov 20 '21 at 20:45
link
up vote 0 down vote
How do I debug "!= w of Type" errors when using `with` or `rewrite` in Agda?
added by jmite Nov 20 '21 at 21:07
link
up vote 0 down vote
What common mistakes have people made in implementations of universe polymorphism and how are they addressed?
added by ice1000 Nov 20 '21 at 21:30
link
up vote 0 down vote
What is the best way to engineer a proof that makes pervasive use of heterogeneous equality, without having to focus too much on transports? [Agda]
added by P.B. Nov 20 '21 at 21:33
link
up vote 0 down vote
What is the best way to prove results about the runtime complexity of a function in proof assistants such as Coq/Agda/Lean?
added by P.B. Nov 20 '21 at 21:37
link
1 2