All Questions
25
questions
1
vote
1
answer
57
views
type variable in datatype definition
I want to modify the datatype which is now defined as below.
datatype assn =
Aemp (*r Empty heap *)
| Apointsto exp exp (infixl "⟼" 200) ...
- 167
3
votes
1
answer
239
views
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
More specially, given arbitrary Lean proof/theorem, is it possible to express it solely using first-order logic? If so, is it practical, i.e. the generated FOL will not be enormously large?
I have ...
- 17.2k
2
votes
0
answers
89
views
concurrent separation logic in Isabelle
Is there a concurrent separation logic in Isabelle for imperative language? I found A Separation Logic Framework for Imperative HOL but that's not designed for concurrent imperative language like C ...
- 167
2
votes
3
answers
320
views
How to write intermediate proof statements inside Coq - similar to how in Isar one has `have Statement using Lemma1, Lemma2 by auto` but in Coq?
I wanted to write intermediate lemmas inside Coq proof scripts, e.g., inside SCRIPT in Proof. SCRIPT Qed. itself - similar to how one would do in Isar. How does one do this in Coq? e.g.:
have Lemma ...
- 5,961
3
votes
3
answers
365
views
Certified calculations in a proof assistant
Symbolic calculations performed manually or by a computer algebra system may be faulty or hold only subject to certain assumptions. A classical example is sqrt(x^2) == x which is not true in general ...
- 43
1
vote
0
answers
550
views
How does one display an arbitrary programming language (e.g. Isabelle/Isar) in latex in their native display in *.pdf format?
I want to display the Isabelle/Isar and Coq languages in Latex, e.g.
when I do coding format in a *.pdf format (for an academic paper).
How do I do this? (I hope this generalizes to other languages ...
- 5,961
0
votes
1
answer
94
views
Handling forall inside an hypothesis
I have just finished my PhD in CS. Now, I am currently learning coq. I am following the course of Software Foundations), which is really good and I am learning a lot. I am starting also a little ...
- 11
2
votes
1
answer
387
views
Does lean enhance proof surveyability?
By proof-surveyability I understand the fact that a human user could "trace" all the details of a proof. There are things that are not easily traceable. For instance, an SMT proof is based ...
- 2,600
0
votes
2
answers
166
views
How to model/formalize the change of the variable (change of world) in Isabelle/HOL?
I am trying to formalize business rules in Isabelle/HOL, but business rules involve the change of the values of some variables, like if x=5 => x=6. => is not the usual implication there, because ...
- 2,926
0
votes
1
answer
320
views
Does Isabelle/HOL have its tactic language?
Coq has tactic language Ltac with match facilities and so on. Does Isabelle/HOL have some programming language for tactics with the services for parsing, pattern matching and so on? I skimmed through ...
- 2,926
4
votes
2
answers
768
views
How proof assistants are implemented?
What are the main blocks of a proof assistant?
I am just interested in knowing the internal logic of proof checking. For example, topics about graphical user interfaces of such assistants do not ...
- 1,373
1
vote
1
answer
170
views
What is Isabelle/HOL command for Compute in Coq?
Proof assistant Coq have compute command (and also check command for determination of the type) which returns the result of function application. Does Isabelle/HOL have similar command and how it is ...
- 2,926
17
votes
0
answers
643
views
What is the Parigot Mendler encoding?
The following encoding of Nats is used in some Cedille sources:
cNat : ★
cNat = ∀ X : ★ . X ➔ (∀ R : ★ . (R ➔ X) ➔ R ➔ X) ➔ X
cZ : cNat
cZ = Λ X . λ z . λ s . z
cS : ∀ A : ★ . (A ➔ cNat) ➔ A ➔ cNat
...
- 52.4k
2
votes
2
answers
1k
views
How we can access Coq or Isabelle/HOL using python program?
I want to access Coq or Isabelle/HOL interactive theorem prover using my python program. Is there any python packages is available? Please suggest
- 934
10
votes
3
answers
2k
views
Nested recursion and `Program Fixpoint` or `Function`
I’d like to define the following function using Program Fixpoint or Function in Coq:
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.
Require Import Recdef.
...
- 25.7k