All Questions
1,072
questions
4
votes
0
answers
53
views
Introductory resources on rewriting logic
Hi I would like to grasp the theory behind Maude [1], [2]
Are there any recommended video lecture notes, talks or introductory notes?
I have been exposed to Functional Analysis, Topology and some Term ...
1
vote
1
answer
43
views
Lean Proving a Prop that has a match
I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem ...
1
vote
1
answer
376
views
Why does Agda use Set instead of Type?
In the 'Hello world' example in Agda — Agda 2.6.5 documentation, it straightforwardly uses Set as follows:
‘Hello world’ in Agda — Agda 2.6.5 documentation
...
- 161
5
votes
2
answers
475
views
The relationship between "true formula" and types in the Curry–Howard correspondence
I have been working through the Implication World in the Natural Number Game using Lean from the following link:
https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/0
While ...
- 161
0
votes
1
answer
36
views
Automatic proofs after simp
My previous question about automatic proofs in Isabelle was answered by @BenjaminBisping pointing out how to use simp.
However, here's a simple example which is the ...
2
votes
1
answer
54
views
Proving factors of GCD in Dafny
While trying to prove various properties of GCD I ran into a proof I am a bit stumped with. Gcd can be defined as the max element in the intersection of the divisors of two numbers. In the code I used ...
- 181
2
votes
1
answer
57
views
Properties of determinants in Isabelle
I would like to use the facts that $\det AB=\det A \det B$ and $\det A = \det A^t$ to prove that $\det AA^t = (\det A)^2$ in Isabelle. Is there a fast way to do this without doing this from scratch?
- 131
0
votes
0
answers
53
views
Arbitrary sorting of non-comparable elements? (Lean 4)
In Lean I'm working a lot with partial orders, and they have this property that not every element is necessarily comparable (i.e. for a, b in P where P is a partial order, it may not be true that ...
0
votes
1
answer
73
views
Defining a Finset in Lean4
I am currently trying to define a finset (of a collection of finite images of some function).
More specifically, given a fixed mapping between the maximal chains of a partially ordered set (of which ...
2
votes
0
answers
59
views
2
votes
2
answers
112
views
Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain
I proved that $\mathbb{Z}[\sqrt{-2}]$ is an integral domain; I would like a review of this proof.
My by hand argument is in Appendix A. It is not the original argument I used. I made a stupid mistake ...
- 3,095
1
vote
1
answer
64
views
Prove that a function's result cannot dependent on Prop-valued parameters in Coq
Consider the following function elem and the lemma that the result of elem does not depend on the proof of ...
- 167
2
votes
3
answers
247
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
- 127
0
votes
0
answers
41
views
Found no matching subterm in goal while it does seem to be there when doing rewrite
I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not?
First place (works fine):
...
2
votes
2
answers
119
views
Type inference with type classes in Coq
I don't understand type classes in Coq. I tried to use them as follows. I have a type cat that is supposed to represent the type of categories and I define the type ...
- 249