All Questions
1,062
questions
0
votes
1
answer
18
views
Prove that a function's result cannot dependent on Prop-valued parameters in Coq
Consider the following function elem and the lemma that the result of elem does not depend on the proof of ...
- 5,455
2
votes
1
answer
33
views
Extract explicit value from Isabelle proof
How can I extract an explicit value for a schematic variable in Isabelle after using it in a proof? For
example, in the following goal, I’m looking to extract a numerical value for ...
- 101
2
votes
3
answers
147
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
2
votes
1
answer
150
views
Is there a way to rename parameters when including/reusing a module type in Coq?
Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
CommunityBot
- 1
2
votes
1
answer
64
views
Strategies for representing proofs of equality
I am interested in strategies for representing proof terms inside the kernel of a proof assistant, specifically proofs of equality.
What are the different strategies that are available for ...
- 5,455
0
votes
0
answers
32
views
Found no matching subterm in goal while it does seem to be there when doing rewrite
I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not?
First place (works fine):
...
2
votes
2
answers
102
views
Type inference with type classes in Coq
I don't understand type classes in Coq. I tried to use them as follows. I have a type cat that is supposed to represent the type of categories and I define the type ...
- 9,722
0
votes
1
answer
27
views
What to import to use le_not_gt_iff?
According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it.
I am trying to prove ...
- 126
1
vote
1
answer
35
views
Arguing with sumbools
I have the following definitions:
Variables Sd_pre : nat -> Prop.
Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
Admitted.
And the following are ...
- 446
3
votes
2
answers
86
views
A $\mu$-recursive function converges at an input, how to find the output?
Summary: I want to implement an interpreter for $\mu$-recursive functions which, for any $\mu$-recursive function $f$ and input $\mathbf{x}$, returns $f \left( \mathbf{x} \right)$ if it is defined.
...
1
vote
0
answers
33
views
Using Isabelle's Archive of Formal Proofs
I am new to Isabelle proof assistant and want to use it to verify a standard proof of the Bruck Ryser Chowla theorem. Since this theorem is about symmetric block designs, I figured that the folder ...
- 111
3
votes
2
answers
76
views
Using if in Fixpoint
I have this recursive function I am trying to define by way of Fixpoint, but the if condition is giving me trouble.
...
- 124
2
votes
3
answers
546
views
What is a positive coinductive type and why are they so bad?
What is a positive coinductive type and why are they so bad?
This question is specifically within the context of Coq and is inspired by this question, the opening lines of which are:
Since positive ...
- 2,022
2
votes
1
answer
35
views
Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?
I have a Lean 4 test project in C:\Temp\MyProject I open with Visual Studio. In that directory, I have a Main.lean file. And, in ...
25
votes
1
answer
1k
views
What is the state of coinductive types and reasoning in Coq?
Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type ...
- 9,105