All Questions
Tagged with formal-verification theorem-proving
21 questions
0
votes
2
answers
332
views
How to formally verify a compiler (frontend and/or backend)?
For a project I am about to begin, I was exploring formal verification of a compiler. I came across the CompCert C Compiler which is an ACM awarded, formally verified C compiler.
When I read further, ...
- 1,872
1
vote
1
answer
161
views
How to proceed in Isabelle when the goal has implications and existentials?
I'm trying to write a proof in the Isabelle "structured style" and I'm not sure how to specify the value of existential variables. Specifically, I'm trying to expand the sorrys in this proof:...
- 5,550
1
vote
1
answer
71
views
Cannot prove in Dafny that f(a,b)=f(b,a)
I m trying to prove in Dafny that a function is symmetric: i.e., f(a,b)=f(b,a). I specify this Dafny by doing ensures f(a,b) == f(b,a). However, it is not able to verify; but what I do not understand ...
- 766
2
votes
1
answer
112
views
How to rearrange newly defined associative terms in Coq?
I wonder what is the most elegant way of rearranging associative terms in Coq. I think it is a well-defined problem for some existing operators, such as plus.
I have defined new associative operater ...
- 67
1
vote
2
answers
536
views
SMT solvers or an alternative for uninterpreted symbols + ∀
I wanted to use Z3 to prove theorems from axioms with universal quantifiers, but Z3 seems to be a bad fit for my problem. It is able to solve some such problems, but it seems to get stuck every now ...
- 81
1
vote
0
answers
94
views
Definition of multiplicative group of a field in Isabelle
theory Scratch
imports
"HOL.Fields"
"HOL.Groups"
begin
locale Field_is_group=
fixes F :: "'a :: field"
begin
typedef 'a mul_group = "{x :: 'a set. x ≠ 0}...
- 11
0
votes
1
answer
185
views
Dafny prove lemmas in a high-order polymorphic function
I have been working on an algorithm (Dafny cannot prove function-method equivalence, with High-Order-Polymorphic Recursive vs Linear Iterative) to count the number of subsequences of a sequence that ...
- 766
0
votes
1
answer
283
views
Proving in Dafny: A non-empty even sequence, is the concatenation of it's two halves
I would like to prove this "trivial" lemma in Dafny. A non-empty even sequence, is the concatenation of it's two halves:
lemma sequence_division(sequ:seq<int>)
requires sequ != []
...
- 766
1
vote
1
answer
236
views
How to prove reverse nil is nil in Lean
I have defined a reverse function on lists, and I am trying to prove the trivial property that reverse of an empty list is empty. It should be provable by reflexivity:
def reverse (t : list α) : ...
- 1,425
1
vote
1
answer
206
views
Knowing when an Isar-style proof is actually valid in Isabelle
I am working on an exercise while trying to learn the Isar language. I have the following script for a lemma about lists.
lemma "EX ys zs. xs = ys @ zs ∧ (length ys = length zs ∨ length ys = length ...
- 123
11
votes
3
answers
899
views
Non-empty list append theorem in Coq
I am trying to prove the following lemma in Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> [] \/ b <> []) -> a ++ b ...
- 21
3
votes
1
answer
381
views
In Isabelle, what do the angle brackets and double asterisks mean?
I'm trying to understand some Isabelle code, and there is some syntax I don't understand. I haven't seen them in tutorials, including the two bundled with the Isabelle2017 distribution, "Programming ...
- 3,655
2
votes
1
answer
198
views
Fully evaluated results in Z3?
Z3 often gives back models defined in terms of a bunch of intermediate functions. For example, it's common to see the following (pardon my improper syntax):
(define-const myArray (Array Bool Int) (_ ...
- 8,383
9
votes
0
answers
133
views
Which First Order theorem provers are guaranteed to halt on monadic inputs?
Monadic First Order Logic, where all predicates take exactly one argument, is a known decidable fragment of first order logic. Testing whether a formula is satisfiable in this logic is decidable, and ...
- 8,383
1
vote
1
answer
284
views
From set inclusion to set equality in lean
Given a proof of set inclusion and its converse I'd like to be able to show that two sets are equal.
For example, I know how to prove the following statement, and its converse:
open set
universe u
...
- 1,622
1
vote
1
answer
159
views
How to write a definition of the non-dependent product using Pi types in Lean?
I'm working through chapter 7 – Inductive Types of "Theorem Proving in Lean".
I'd like to know how to write the definition of dependent non-dependent product in a more expanded or "primitive" form.
...
- 1,622
8
votes
1
answer
606
views
Proving substitution property of successor over equality
I'm trying to understand inductive types from chapter 7 of "theorem proving in lean".
I set myself a task of proving that successor of natural numbers has a substitution property over equality:
...
- 1,622
2
votes
2
answers
154
views
Rewriting in simple theorem proof
I wrote a definition of group in Idris:
data Group: Type -> Type where
Unit: (x: t) -> Group t
(*): Group t -> Group t -> Group t
Inv: Group t -> Group t
postulate
...
- 4,398
4
votes
2
answers
306
views
How to implement fully-declarative Horn logic? [closed]
I would like to formalize some knowledge and execute queries in what may referred to as fully-declarative Horn logic (or, fully-declarative Prolog). Could anyone provide some guidelines on how to ...
- 823
6
votes
1
answer
842
views
Need help understanding the Owicki-Gries method
I've (mistakenly) picked up a course about verifying concurrent programs, and we've so far covered this method called "Owicki-Gries method". Apparently, one can prove various results about the program ...
- 985
7
votes
1
answer
3k
views
printing internal solver formulas in z3
The theorem proving tool z3 is taking a lot of time to solve a formula, which I believe it should be able to handle easily. To understand this better and possibly optimize my input to z3, I wanted to ...
- 383