Skip to main content
14 votes
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 ...
Kyle Miller's user avatar
11 votes
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 ...
Mario Carneiro's user avatar
6 votes
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 ...
Ana Borges's user avatar
6 votes
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 ...
Åsmund Kløvstad's user avatar
5 votes
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 ...
Andrej Bauer's user avatar
  • 8,989
5 votes
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 ...
Jason Gross's user avatar
  • 1,457
4 votes
Accepted

Simple Proof about `String.split`

I personally believe that this is impossible. Note that the signature of splitAux is: ...
ice1000's user avatar
  • 6,144
4 votes
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 ...
Ana Borges's user avatar
4 votes

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. ...
Li-yao Xia's user avatar
  • 1,727
3 votes
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 ...
Trebor's user avatar
  • 3,867
3 votes
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: ...
ice1000's user avatar
  • 6,144
3 votes
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 ...
Jason Rute's user avatar
  • 8,555
3 votes
Accepted

Strong induction for nat in Coq

A classic solution is to define a stronger property, which you prove by induction. ...
Pierre Castéran's user avatar
2 votes

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

Here is a proof without congruence, closer to your paper proof. What you want is probably the injection tactic, more about ...
Villetaneuse's user avatar
2 votes

Problem proving a binary add function

In this case you can use functional induction and automated solvers. Unfortunately, functional induction doesn't work well over dependent types. The popular Equations plugin works better with ...
Molly Stewart-Gallus's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible