Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
13
questions
3
votes
0
answers
109
views
Lower bounds in type theory proof assistant with ordinals and universes without axioms
I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024?
My ...
- 279
11
votes
5
answers
2k
views
How do real-world proof assistants bind variables and check equality?
There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.
There are also ...
6
votes
2
answers
426
views
Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?
I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
6
votes
1
answer
101
views
What are the typechecking differences between records and iterated sigma types in Agda?
If we have univalence at hand, the records and iterated sigma versions of some type will be equal. Still, there may be some important typechecking-related differences.
For example, it seems that one ...
- 161
3
votes
2
answers
229
views
Has extensionality ever caused any problems in a mathematical proof?
I read the following about extensionality in PLFA,
Agda does not presume extensionality, but we can postulate that it
holds:
...
- 2,210
3
votes
2
answers
254
views
How to convert Agda's with statement to a helper function?
I read here that
Every use of with is equivalent to defining a helper function
But I couldn't get it working with trying to re-implement a with-clause (which itself came from re-implementing the ...
- 2,210
2
votes
1
answer
53
views
Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?
I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (...
- 2,210
3
votes
1
answer
391
views
How to provide proof for termination in Agda?
I am trying to write an integer division function from scratch in agda2 (as of 2.6.3):
...
- 2,210
4
votes
2
answers
210
views
Binding variables to terms involving later variables
Consider the following pseudocode in a hypothetical proof assistant:
def f (n : ℕ) : P n
:= match n with
| zero -> ?0
| suc k -> ?1
end
...
- 3,190
6
votes
1
answer
409
views
What are the principal differences between Agda's core type theory and Coq's?
Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
3
votes
2
answers
153
views
Can Hyperreal exist a axiom-free implementation in HoTT?
The main current implementations of hyperreal numbers are model-theoretic and set-theoretic approaches. Most of these implementations are strongly non-constructive, and many require a very deep ...
- 279
7
votes
1
answer
556
views
Examples of theories where tactic language is required for simple proofs
I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
- 177
7
votes
0
answers
102
views
How to improve/understand typechecking performance in Agda?
I've recently been trying to do some basic formalization of category theory in Agda. As part of this I need to prove a bunch of basic properties around products/monoidal categories. A bunch of these ...
- 171