Questions tagged [proof]
A mathematical proof is any mathematical argument which demonstrates the truth of a mathematical statement. Informal proofs are typically rendered in natural language and are held true by consensus; formal proofs are typically rendered symbolically and can be checked mechanically. "Proofs" can be valid or invalid; only the former kind constitutes actual proof, whereas the latter kind usually refers to a flawed attempt at proof.
proof
836
questions
2
votes
1
answer
50
views
WP Plugin: Why does the following simplified code fail to verify
I am a new Frama-C User and I am trying to prove certain properties for a large project. I was seeing a particular proof fail, and tried reducing the problem to a minimum reproducible example, and the ...
0
votes
1
answer
45
views
How to instruct `auto` to simplify the goal during proof search?
A minimal example of my issue looks as follows:
Goal let x := True in x.
This is immediately solved by simpl. auto., but auto. does not work.
In my actual case, the search tree is a bit bigger than ...
- 6,849
1
vote
1
answer
28
views
Prove max x y = y given that x <= y in Idris 2?
I am new to Idris2 and need some guidance on proving the following relationship:
simplify_max : (LTE x y) -> (max x y) = y
simplify_max prf = ?code
I read in the docs that the constructors for LTE ...
- 21
0
votes
1
answer
58
views
Is is possible to rename a coq term?
Sorry, I'm not sure if the title is the adequate question.
I have been going through Logical Foundations. In the Lemma "double_plus" i solved it with this solution:
Lemma double_plus : ...
- 71
1
vote
1
answer
47
views
How to extract a variable from an exist clause
I am triying to make a simple reduction to absurd proof with Dafny, normally when I do so (in real life mathematics) I use arguments like "ok, now lets choose a p that fullfills this property ...
0
votes
1
answer
59
views
Proof by reductio ad absurdum in Isabelle
I understand how ccontr works, however I am unsure how (or even if it is possible) to use it on a lemma declared with assumption(s).
Take this simple example, all is good:
lemma l1: "A⊆B ⟶ A ∩ B =...
- 29
1
vote
0
answers
34
views
I have a problem in Isabelle related to 'Clash of types' that I am unable to solve. Could someone help me?
I would want to formalise a calculus in Isabelle. I started with this definitions:
type_synonym Signature = "string ⇀ nat"
type_synonym 'a Interpretation = "string ⇀ 'a list set"
...
4
votes
2
answers
153
views
Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
This was actually something I wanted to understand with my previous question, but I misworded it by giving for granted the solution would somehow have to build on sequence and repeat, so I got an ...
- 26.7k
0
votes
0
answers
56
views
How to improve a LH=RH chain proof
I am tying to get a better understanding how Isabelle manages the chain proofs, specifically when associativity/commutativity is involved. Imagine I have a binary non-homogeneous operator op that is ...
- 29
0
votes
2
answers
211
views
How to prove that nat_to_bin combines bin_to_nat b = normalize b in Coq
I am a green hand in studying Coq with the reference book softwarefoundation-induction
In the last part of this phrase, there is an exercise about proving that
change a binary to a nature number and ...
-2
votes
3
answers
72
views
Is this the best loop variant for the following code which takes in a sorted array of integers and determines if theres are ints x,y that equal k
Would "there exists a pair x,y in the subarray arr[left:right+1] that sums up to k." be a good loop variant for the code below which determines given a sorted array of integers if there is a ...
- 9
-1
votes
2
answers
58
views
Sledgehammer output with vampire
I tried to use sledgehammer in proof and got such output
Sledgehammering...
vampire found a proof...
Derived "False" from these facts alone: SymbolicE, const_bool_simp, ptype_bool_not, ...
- 23
0
votes
1
answer
36
views
Agda Recursion on Proof
I have created a recursive Datatype „Positive“ in Agda. Im using this datatype to Index some Tree.
On those trees I am trying to proof that a set operation on some Index q doesnt affect a get ...
- 59
0
votes
1
answer
78
views
What is the simplest AVL tree structure to demonstrate a complete right rotation?
I'm learning about AVL trees and their rotations in data structures. I wish my lectures had showcased the simplest complete right rotation because I found the topic became way easier for me when I ...
0
votes
1
answer
60
views
Agda Unresolved Metas
I have created a Tree datatype. And a get function that should retrieve a value from it. I now want to create a Proof that retrieving any Value from an Empty Tree will return "nothing".
(I ...
- 59