# Questions tagged [proof-techniques]

The tag has no usage guidance.

12 questions
Filter by
Sorted by
Tagged with
68 views

### Proof Checking for State Machines Similar to TLA+

I'm wanting to find a modern proof assistant that I can use for modeling distributed systems or similar protocols/algorithms. TLA+ is the most commonly used language in that field, but I recently ...
• 21
1 vote
145 views

### Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?

Remark 1. The following counting formula can be derived using arithmetic properties of inequalities, properties of floor / ceiling, inclusion-exclusion, sieve-of-Eratosthenes, and the inclusion-...
• 303
74 views

### Verify maximal diameter of a tree in Dafny

I am trying to learn formal methods and have been learning Dafny and practicing by verifying Leetcode problems. I have gotten stuck on this one. https://leetcode.com/problems/diameter-of-binary-tree/...
• 181
566 views

### Examples of theories where tactic language is required for simple proofs

I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
• 177
343 views

### How to write this non-constructive proof in Lean?

There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational. An interesting proof in classical logic is the following: Consider $u = \sqrt{2}^{\sqrt{2}}$. If $u$...
• 313
1 vote
163 views

### İnduction/inversion and others in coq

I'm trying to learn Coq using the software foundations. I somehow made it to the 2nd volume but I'm struggling writing proofs on my own. Especially whether I should be using inversion or induction. I ...
81 views

### Formally verified email or communication?

This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway. I would like to consider the simplest possible formally verified ...
1 vote
48 views

### How do I prove this property about a factorial specification in Coq?

Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...
1 vote
177 views

### How do I prove a record related lemma?

I'm new to coq. I would appreciate it if you could help me. Consider the following definition: Record person:= mk_person { p_name : t1; p_age : t2}. How to prove ...
313 views

### Proving strict positivity in Agda

In Agda we can prove termination of functions by using well-founded relations, is there a guideline for proving datatype declarations strictly positive, possibly via use of some container techniques ...
• 547
1 vote
198 views

### How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?

Disclaimer: this question is not asking for code -- it's asking for a proof strategy. For simplicity we may use Fin n (for the usual ...
• 6,346
I’ve been thinking lately about counting-in-two-ways proofs. For example, we can prove the identity $$2^n = \sum_{k=0}^n \binom n k$$ just by noting these are just two ways to count the number of ...