# Tag Info

Accepted

### Proof review: Sum of nCk over antidiagonal = Fibonacci

I'll first go through piece-by-piece and suggest some local improvements. For the induction principle, when you find yourself doing intros as the first step of a ...
• 506
Accepted

### In Lean, contradiction tactic failed but actually goal accomplished

The issue is the ; at the end of the long line. This is causing the {right, ...} block to be applied to all goals, meaning that ...
• 1,484
Accepted

### Axiomization of Peano arithmetic in constructive first-order logic

Some references: Essential Incompleteness of Arithmetic Verified by Coq includes a formalization of Peano Arithmetic, but it hasn't been kept up-to-date with recent Coq versions AFAIK, and I include ...
• 926
Accepted

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

Here is a version where A : Set i and both equalities live in Set (lsuc i). The idea is taken from Leibniz Equality is ...
Accepted

### How to implement first-order relational structures in Coq?

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as ...
• 8,989
Accepted

### Proof Review: Basic theorem about ternary relations in Coq

I decided to formalize this in Coq in the simplest way possible, defining a new type $T * T * T \to 2$ In proof assistants and functional programming languages more generally, it's generally more ...
• 1,457
Accepted

### Simple Proof about String.split

I personally believe that this is impossible. Note that the signature of splitAux is: ...
• 6,144
Accepted

### Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis

Here is how you can defer the choice of what variables are to a later time. This amounts to making OpenWff depend on a parameter; I'm not sure why that was giving ...
• 926

### Proof Review: Basic theorem about ternary relations in Coq

To permute abc to cba with the given primitives, a single rotation and a single transposition suffice. ...
• 1,727
Accepted

### Problem proving a binary add function

If you can change your definition of badd, then you can try swapping l1 and l2, which is in ...
• 3,867
Accepted

### How do I approach the final step in proving the cancellation law in Coq?

You can prove your theorem S_n_eq_S_m_if_n_eq_m by congruence: ...
• 6,144
Accepted

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

Note, this my not be the most optimal answer, but here is how I would approach this. Also, note, it is important to provide a MWE when you ask questions like this so that the answerer can plug this ...
• 8,555
Accepted

### Strong induction for nat in Coq

A classic solution is to define a stronger property, which you prove by induction. ...