Skip to main content

Questions tagged [proof-techniques]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
0 answers

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.
Hath995's user avatar
  • 131
6 votes
1 answer

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 ...
uhbif19's user avatar
  • 167
2 votes
1 answer

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$...
Weier's user avatar
  • 313
1 vote
1 answer

İ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 ...
noCrayCray's user avatar
2 votes
0 answers

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 ...
Julius Hamilton's user avatar
1 vote
0 answers

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 ...
bodacious_bandit's user avatar
1 vote
1 answer

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 ...
B.Rolando's user avatar
7 votes
2 answers

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 ...
Ilk's user avatar
  • 547
1 vote
2 answers

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 ...
ice1000's user avatar
  • 6,186
7 votes
3 answers

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 ...
Jason Rute's user avatar
  • 8,685