Questions tagged [proof-techniques]
The proof-techniques tag has no usage guidance.
9
questions
5
votes
1
answer
452
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 ...
- 158
1
vote
1
answer
291
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$...
- 273
1
vote
1
answer
56
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 ...
- 51
2
votes
0
answers
74
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 ...
- 175
1
vote
0
answers
42
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
107
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
256
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 ...
- 517
1
vote
2
answers
182
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 ...
- 5,857
6
votes
3
answers
277
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 ...
- 6,995