Questions tagged [proof-review]
For questions that ask about possible improvements of a working piece of a proof. Make sure to also include the tag for the language used, and follow that tag's guidance regarding additional version-specific tags.
14
questions
2
votes
2
answers
132
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,105
4
votes
2
answers
105
views
How do I approach the final step in proving the cancellation law in Coq?
I'm trying to prove the cancellation law for natural numbers. This is my proof so far:
...
- 209
4
votes
1
answer
2k
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 257
5
votes
1
answer
520
views
Simple Proof about `String.split`
I am new to lean, working on proving a simple lemma in lean4.
lemma String.split_empty (c): String.split "" c = [""]
I tried looking for ...
- 257
3
votes
0
answers
105
views
Using crude but effective stratification & cong to implement transitivity of `=`
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 ...
- 6,346
1
vote
1
answer
698
views
Strong induction for nat in Coq
I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:
...
- 205
2
votes
1
answer
264
views
Axiomization of Peano arithmetic in constructive first-order logic
I've been playing with axiomising systems of first-order logic in Coq. I've started to develop the beginning of a framework. As an example I give a minimal phrasing of Peano arithmetic in Coq in the ...
- 2,868
7
votes
1
answer
1k
views
In Lean, contradiction tactic failed but actually goal accomplished
I've been playing with Lean, trying to prove the next lemma:
lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) :=
...
- 205
6
votes
2
answers
275
views
Problem proving a binary add function
I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).
I have created this badd function that ...
user1231
6
votes
1
answer
217
views
Proof of symmetry of universe-polymorphic Leibniz equality in Agda
Consider the following definition of universe-polymorphic Leibniz equality:
...
- 6,346
3
votes
1
answer
187
views
Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis
I'm proving that a simple propositional logic satisfies Aristotle's thesis.
I'm curious how to improve the code in question.
Here are the things I know that are wrong with it:
I'm using ...
- 3,105
5
votes
1
answer
180
views
How to implement first-order relational structures in Coq?
I'm trying to define a first-order relational structure in Coq.
I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.
I also have a ...
- 3,105
4
votes
2
answers
124
views
Proof Review: Basic theorem about ternary relations in Coq
I'm proving a simple fact about ternary relations in Coq as an exercise.
I'm interested in ternary relations at the moment because they are a simple thing that can represent a finitary consequence ...
- 3,105
14
votes
1
answer
207
views
Proof review: Sum of nCk over antidiagonal = Fibonacci
Theorem to prove:
The sum of the binomial coefficients over an antidiagonal is a Fibonacci number. More specifically, the $n$th antidiagonal sums to the $n+1$th Fibonacci number, where the ...
- 684