Top new questions this week:
|
|
I am looking for axioms/inference rules that satisfy the following 3 conditions: can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, …
|
|
Suppose I have cong : {A B : Type} (f : A -> B) (p : a = b) : f a = f b coe : (A : I -> Type) -> A 0 -> A 1 It is …
|
|
I’m interested in figures on computer proof assistant usage. To put this in perspective, I have a server which I am making at the moment, and I only feel like committing time to setting up four or …
|
|
I’m trying to prove the following lemma : …
|
|
Given this code, inductive Test : Type | T1 | T2 example : Test.T1 ∈ { t: Test | t = Test.T1 } := begin sorry end How do I prove that …
|
Greatest hits from previous weeks:
|
|
I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my …
|
|
What is a good starting point to learn about proof assistants? The answer will invariably depend on the area of interest: mathematics (and its areas, e.g. algebra,combinatorics, analysis, logic), CS – …
|
|
Off and on I have heard of the jargon “commuting conversion” but I don’t really know what it means. I’ve heard commuting conversions are problematic but I don’t know why.
|
|
Fifty years ago, few would have imagined that the process of verifying the correctness of a known proof of a mathematical theorem might be so costly that the mathematical community would hesitate to …
|
|
Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too). What are the main differences between Coq and Lean? Ideally it …
|
|
I’m working in cubical agda. I am wondering how to access local definitions once outside of the local environment. For example, suppose I have the following code: …
|
|
Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type …
|
