Questions tagged [proof-techniques]
The proof-techniques tag has no usage guidance.
12
questions
2
votes
0
answers
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
1
answer
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
4
votes
0
answers
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
7
votes
1
answer
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
2
votes
1
answer
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
1
answer
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 ...
- 71
2
votes
0
answers
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
0
answers
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
1
answer
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 ...
- 11
7
votes
2
answers
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
2
answers
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
7
votes
3
answers
321
views
Counting in two ways
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 ...
- 9,653