# 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.

13 questions
Filter by
Sorted by
Tagged with
102 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: ...
1k views

### Doing case-by-case proofs about match statements in Lean4

In Lean4, I am stuck in a proof with a goal like this: ...
459 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 ...
100 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,166
1 vote
614 views

### Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
• 195
235 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 ...
980 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) := ...
• 195
271 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 ...
215 views

### Proof of symmetry of universe-polymorphic Leibniz equality in Agda

Consider the following definition of universe-polymorphic Leibniz equality: ...
• 6,166
164 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 ...
• 2,761
167 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 ...
• 2,761
114 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 ...
• 2,761
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 ...