Newest Questions
1,207 questions
5
votes
1
answer
176
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
0
answers
31
views
Coq: proving a disjunction without left nor right
a beginner's question again.
I'm in the current proof
...
- 157
1
vote
1
answer
29
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
159
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
38
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 ...
- 157
3
votes
1
answer
146
views
2
votes
1
answer
90
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
...
- 157
2
votes
1
answer
29
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
36
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
89
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
69
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
49
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
83
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
387
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
101
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
14
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
29
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
65
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
0
answers
17
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 ...
kataph
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,334
2
votes
0
answers
61
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
61
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
29
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
141
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
1
answer
32
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
208
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
80
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
247
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,512
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
457
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
219
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
641
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,512
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
313
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 (*):
...
- 530
3
votes
1
answer
181
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
31
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
1
vote
3
answers
110
views
How to target an introduced value set with the set tactic for induction in Coq?
Suppose I have a pair of two natural numbers $(a, b) \in \mathbb{N} \times \mathbb{N}$.
I define the relation $<$ below.
$(a, b) < (a', b') \;\; \text{if and only if} \;\; a + b < a' + b'$.
...
- 3,561
0
votes
3
answers
83
views
What are the set of mathematical fonts in Lean 4?
When reading mathematics books, there are often different fonts for indicating concepts such as sets and algebraic structures. In Lean 4 using VSCode:
\bn produces ...
- 2,662