Newest Questions
1,209 questions
0
votes
1
answer
29
views
An optimal proof of the theorem in Coq
On the link Basics I encountered the following problem: Prove the following theorem, which states that as long as the grade starts above F-, the lower_grade option indeed lowers the grade. As usual, ...
- 1
2
votes
0
answers
18
views
Proving that negative axioms don't break canonicity
In Negative consistent axioms can be postulatedwithout loss of canonicity, the authors show that if $\lnot P$ is a consistent axiom with MLTT, then MLTT+$\lnot P$ still has canonicity of $\mathbb N$. ...
- 181
5
votes
1
answer
584
views
Why are dependent sums and products called sums and products?
The immediate impetus for this is watching this video by Mario Carneiro; around the 8:05 mark he mentions dependent type theory. That reminded me of a question I first had years ago about why ...
- 3,561
0
votes
1
answer
76
views
Proving a disjunction without left nor right in Coq
A beginner's question again.
I'm in the current proof:
...
- 159
1
vote
1
answer
44
views
Why the result of pattern matching don't get propagated in some expressions?
I experienced this when I was trying to prove some lemma. Here are my definitions:
...
- 111
3
votes
1
answer
168
views
Can a metamath identifier be reused across scopes?
I am writing a metamath verifier in OCaml as a learning exercise.
I am mostly working off of their book and some other things like this presentation.
So far I've worked on this without consulting the ...
- 3,561
0
votes
2
answers
42
views
Coq: how to apply "only once"
I'm having a stupid struggle with Coq. Although, given
Goal 1
P, Q : Prop
H : P
H0 : P -> Q
(1 / 1)
False
when I ...
- 159
3
votes
1
answer
147
views
2
votes
1
answer
93
views
Coq: when to give a context variable of imported package as argument
I'm a beginner in Coq.
When I run the following code
...
- 159
2
votes
1
answer
34
views
Induction over multiple arguments in Isabelle
Exercise 2.11 of "Concrete Semantics" by Tobias Nipkow, Gerwin Klein asks to define polynomials as lists of coefficients, I defined addition as matching over two parameters:
...
- 121
0
votes
1
answer
38
views
No notations from custom entries inside the proof state
In the previous question I was told to create custom notations for my formal logical system.
In order for the notation to work I had to change the symbol from the answer:
...
- 333
1
vote
1
answer
97
views
Constructing elements of Fin type after using `<?`
I'm ... tired of struggling with this question? I'm trying to construct elements of a Fin set, and not succeeding. Here's a simple definition that hopefully clarifies my difficulty:
...
- 113
1
vote
1
answer
72
views
How to automate resolving circular dependencies between definitions and obligations in Coq?
The answer to this question suggests to use the sequence set (x := foo_obligation_n _ _ ... _). clearbody x. simpl in x. before ...
- 111
0
votes
2
answers
50
views
Coq alternative mechanisms of proving that a function terminates
I wrote a proof for this question, but it's long and kind of terrible, see Appendix A.
There is one specific thing that I want to focus on and that is the induction step in ...
- 3,561
1
vote
1
answer
84
views
how to proof on coq double negation of p is logical equivalent to p
how to proof on coq double negation of p is logical equivalent to p?
¬(¬ p )->p
i found actually a way but this not seemed like the purest form. Can someone help?
...
- 13
2
votes
1
answer
405
views
How to do simultaneous induction in Coq?
I have proofs for
P(0, 0)
P(0,n)->P(0, Sn)
P(m,0)->P(S m, 0)
P(m,n)->P(S m, S n).
How do I prove A for all values in Coq?
I tried two normal inductions, but it required P(m, S n)->P(S m, ...
5
votes
1
answer
108
views
Significance of uniqueness rules in MLTT-style systems (vs. CIC-style systems)
For context, I'm trying to compare the systems grouped under the umbrella "Martin-Löf type theory" with those under the umbrella "calculus of inductive constructions". It seems ...
- 467
1
vote
0
answers
15
views
Show that a ratio of numbers is always greater than one in ACL2R
There is a straightforward by-hand argument for this question from the Math StackExchange.
I'm trying to produce a mechanically verifiable proof for it using acl2r.
...
- 3,561
1
vote
0
answers
30
views
In Lean 4 prover, how to include a constructor into the search scope of a tactic?
I'm translating a soundness proof of system F- from Rocq to Lean 4.
Here is part of the relevant Rocq code:
...
- 131
1
vote
1
answer
66
views
Inductive Hypothesis is wrongly generated
(Compiling code at the end)
So, I'm trying to prove progress for a small language:
...
1
vote
1
answer
80
views
How to redefine standard notation
In this code I would like to change the standard notation for "~":
...
- 333
3
votes
1
answer
67
views
Best tool for proving that a (big) first order model is actually the model of some (big) first order theory.
I have to check that a (big: several hundreds axioms) first order logic theory is satisfiable.
There are various authomated provers for first order logic (e.g. Vampire) that could tell me if the ...
- 47
1
vote
1
answer
50
views
"Implicit arguments declaration relies on type, discarding", meaning in Coq
I am proving some basic things in Coq as an exercise.
Here is the hypothetical syllogism, corresponding to combining functions in reverse order.
...
- 3,561
3
votes
2
answers
99
views
Distinct setvars in metamath
Metamath uses a very special system of variable distinctness to avoid having to codify capture-avoiding substitution in other formal systems. In metamath/set.mm for example, there is an axiom $$\vdash ...
- 4,344
2
votes
0
answers
62
views
What are some strategies for encoding a topology in Coq?
Topologies are the simplest example I can think of of a mathematical object that's fundamentally non-first-order.
I'm curious what some strategies are for encoding topologies or topological spaces in ...
- 3,561
2
votes
1
answer
89
views
Improving the proof of transitivity theorem
After a lot of work done in this answer by Andrej Bauer I decided to use his formal system to continue with theorems from Mendelsons book. Here is the next theorem after deduction(transitivity):
A -&...
- 333
4
votes
2
answers
1k
views
Proof assistants for undergraduate analysis
I am looking for a program that would help me prove some elementary inequalities. What I mean by that is that:
I would tell the program some term written with usual functions, then I would tell him « ...
- 143
1
vote
1
answer
64
views
In LEAN4 prover, what's the problem of generalising a type from String to a free type?
I'd like to convert the following code in Coq to Lean 4:
(this is the beginning of the soundness proof of type system F-)
...
- 131
0
votes
1
answer
30
views
What are the Mizar tools mizf and miz2prel?
You can build various executables that are distributed as part of the Mizar system with the following shell script adapted from this script from Roland Coghetto referred to in this answer by Alex ...
- 3,561
-4
votes
1
answer
143
views
How the soundness / completeness proofs are formalized for new type theories? (with application to automated extension of calculi / proof assistants)
Initial teaser: if we work in the predefined proof assistant/type theory (constructive type theory for Coq, Lean or HOL in the guise of type theory in Isabelle/HOL), then we can state some theorem in ...
- 85
2
votes
1
answer
64
views
Need help to prove that a variable is extracted using pattern matching from a pair (or a dependent pair) in Lean 4
everyone! I'm new to Lean4, and I'm practicing to write a proof.
I write a function that returns several values, proofs or functions, and I pack them in a nested dependent pair. I wanna create new ...
- 21
1
vote
2
answers
46
views
lean 4 foreign function interface for matrix multiplication?
I am trying to get some experience with using Lean 4 and write some functional programs that I can use for my daily work. One feature I'd like to have is to interface Lean 4 with external C/C++ code ...
- 2,662
1
vote
2
answers
168
views
3
votes
1
answer
209
views
How do you build Mizar locally?
Here is the recently open-sourced repo for the Mizar system.
It's pretty cool.
It's written in Pascal and appears to be compilable with using fpc with the ...
- 3,561
3
votes
0
answers
82
views
Proof assistant comparison chart
Is there a proof assistant comparison chart for common tasks?
I'm picturing something like this very old page comparing SML and OCaml, which I found helpful when I was learning OCaml because it made ...
- 3,561
0
votes
0
answers
33
views
Defining Integral operator and proof of laws
I would like to make a definition of the Integral operator and proofs of laws about the integral operator. How can I go about it?
Have started like this in Temporal Logic of Actions (TLA)
...
- 1
5
votes
1
answer
250
views
Learning category theory from Lean formalization?
I am trying to learn basic category theory using Lean 4. I don't have prior coursework on it. And I wonder whether this is feasible and if there is a good tutorial for this.
My main goal is to be able ...
- 2,662
3
votes
1
answer
79
views
Can I in Coq define a class with a notation for its field such that another field uses the notation?
It's basically this question but about classes.
Imagine I want to do this:
...
- 6,532
1
vote
2
answers
191
views
what's the difference between Lean 4's simpa and simp tactics?
I am having some difficulty understanding the simpa tactic in the example below (and in general).
The documentation says that
simpa [rules, ⋯] using e will ...
- 2,662
1
vote
1
answer
478
views
Delaying opacification of Lemma in Coq
I am interested in ergonomic ways of expressing modal logic and relevant logics in Coq. I would prefer to do it without axioms (besides perhaps something like ...
- 3,561
6
votes
1
answer
220
views
State of homotopy canonicity of HoTT with univalence axiom
I'm new to HoTT. I've started reading the current version of the HoTT book.
On page 12, it mentions as an open problem whether HoTT + univalence has the “homotopy canonicity” property, i.e., every ...
- 467
2
votes
1
answer
105
views
Type annotation of fixpoint combinator intereferes with Lean4's strictness
As many people already know, it's not possible to implement a Y combinator in a strict language using the following combinator $\mathsf{M},\,\mathsf{W}$ where
$$
\...
- 23
0
votes
2
answers
89
views
Coq proving special cases of the law of the exlcuded middle: equalities on inductive types
I recently tried to prove that $x = y \lor x \neq y$ for two types $\mathbb{N}$ and $\text{Option}[\mathbb{N}]$.
The first special case is easy to prove with lia, ...
- 3,561
6
votes
1
answer
642
views
Can I in Coq define a recursive function with a notation such that the recursive calls can use it?
Say I want to define add : nat -> nat -> nat with a notation Notation "a + b" := add a b and I want to write <...
- 6,532
2
votes
0
answers
47
views
Countermodel generators for constructive logics
Is there any software out there that can generate countermodels in some form for non-theorems in a constructive logic? I am especially interested in generating countermodels for theorems that are ...
- 3,561
1
vote
0
answers
19
views
"Pausing updating" Tactic state mid-sentence by a shortcut key or a setting in Lean 4 VSCode extension?
While entering Lean 4 proofs involving mathlib, I noticed that the Lean often get stuck in updating the Tactic state in Infoview while new characters are entered and the current command is not yet ...
- 2,662
1
vote
3
answers
314
views
Which natural deduction rule is this "application"?
Working of propositional logic, using Coq just for exploration:
I cannot match the effect of apply in this code with a rule of natural deduction (*):
...
- 587
3
votes
1
answer
182
views
Why unknown identifier for a declared variable in Lean 4
I'm trying to follow the Introductory Proof with Lean 4 - Natural Numbers but I get unknown identifier 'b' and the same happens with all the variables except ...
- 133
0
votes
1
answer
33
views
Isabelle Jedit try to check file and show all errors
I am using Isabelle with JEdit on Windows, mostly because I'm interested in understanding exactly how powerful the sledgehammer tactic is.
I have the following extremely basic file and I'm trying to ...
- 3,561
6
votes
1
answer
462
views
What is the two-dot notation in Lean 4?
I saw a new notation consisting of two dots .. as in the map_zero .. line in the following (from Mathematics in Lean):
...
- 2,662