All Questions
812
questions
1
vote
1
answer
9
views
What is a context mapping in dependent type checking?
I am reading a dissertation about dependent type programming language (Norell, 2007), and had much trouble understanding the definition of context mappings/substitutions as shown in the figure below .
...
- 1,700
2
votes
1
answer
166
views
What is a pattern in dependent pattern matching?
I am trying to understand dependent pattern matching while reading Goguen, McBride, and McKinna (2006)'s paper, but couldn't quite grasp the concept. I know regular pattern matching in functional ...
- 1,700
2
votes
2
answers
68
views
metamath meta variables
I'm reading https://us.metamath.org/mpeuni/mmzfcnd.html and it says
Each "axiom" in Metamath's version of ZFC set theory is not an actual
axiom in the language of first-order logic but is a ...
- 21
1
vote
0
answers
63
views
Unfolding constants while rewriting using rewrite_strat and a hint database
I'm working with a substitution algebra as described by the Autosubst team, and I'm trying to automate some rewritings. As I'm using more than one calculus in my code, I'm trying to use the rewrite ...
- 133
4
votes
1
answer
93
views
What is the best way to learn Iris completely independently
I am looking forward to learning Iris by myself, I have essential basic knowledge of Coq and logic but I don't know where to start. Logically, I looked into materials on the project website; the video ...
0
votes
0
answers
15
views
reference ospecialize and variable prim_base_irreducible not found in the current environment
Error encountered when trying to make after coq_makefile -f _CoqProject -o Makefile for lambda-rust
...
- 123
0
votes
0
answers
50
views
How to check a Zenon-generated proof with Coq?
I installed zenon (opam package, github) and tried to use it to generate a Coq proof.
I couldn't find any documentation for the Zenon's main syntax, so I looked at its test suite.
I grabbed this test ...
- 2,711
0
votes
2
answers
179
views
Is there a multiway system which is equivalent to taking ZFC as axioms?
My understanding is that Stephen Wolfram's concept of a multiway system begins with certain rules and then generates all possible combinations of those rules. There are many distinct mathematical ...
- 175
1
vote
1
answer
79
views
problem with unification
I've faced a problem. I'm not sure how to explain it, so, that is why I'm asking.
...
- 215
1
vote
1
answer
57
views
How to express that two equivalence relations can setoid rewrite across each other (Coq)
I am looking for a way to express that two equivalence relations are compatible and can (setoid) rewrite across each other. As an example here's an ordinary proof I wrote that a left inverse implies ...
- 113
2
votes
1
answer
111
views
Are all LEAN tactics equivalent to applying some theorem?
I don't understand LEAN well enough, but from my rough understanding that tactics delete old pairs of conditions and goals and create new pairs of conditions and goals, it seems all tactics are ...
- 123
1
vote
2
answers
80
views
How to introduce assumption in lean4
This is probably a trivial question, but I've been googling for hours and can't find the syntax I'm looking for.
I'm trying to write a proof of
...
3
votes
2
answers
186
views
Universe inconsistency errors when using ZF model in Coq
I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that ...
- 195
0
votes
1
answer
65
views
How to run lean4 with mathlib manually
I have a file which contents are:
import Mathlib.Data.Rat.Basic
I save it as file.lean in a lean project
and run it like this
...
- 141
5
votes
1
answer
452
views
Examples of theories where tactic language is required for simple proofs
I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
- 158
0
votes
1
answer
127
views
Why inductive types (or variants) are so rigid in terms of the set of constructors
An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined.
For instance:
...
- 125
2
votes
2
answers
93
views
Continue a section (with context) in coq
So I have a file in coq, which is a bit like the following:
...
- 245
2
votes
1
answer
138
views
How to understand the sigma types example from "Theorem Proving in Lean 4"?
In the Lean 4 book called "Theorem Proving in Lean 4" (https://lean-lang.org/theorem_proving_in_lean4/title_page.html), I don't understand a code example about cartesian product types in ...
- 123
2
votes
0
answers
26
views
Problem working with FMapWeakList and Parametrized Records
Consider the following definition of a record R, parametrized over an arbitrary eqType:
...
- 63
2
votes
1
answer
97
views
How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?
I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, ...
- 141
0
votes
0
answers
60
views
Help with fixing a Coq installation using docker and vscoq
I'm following the logic foundation preface and just began learning. I tried to use the docker with vscoq like the suggested in the book but it didn't work for me and kept asking me to install coq ...
1
vote
1
answer
135
views
how to prove 2+2+a=4+a in lean4?
It should be simple but dig it for a while and still not successful.
theorem example (a : R) : 2 + 2 + a = 4 + a := ...
can someone help to figure out how to do next? many thanks
- 11
5
votes
1
answer
167
views
Universe polymorphism and Coq standard library
When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic.
Is there an alternative standard ...
- 75
1
vote
1
answer
100
views
How to handle data from json files in lean 4?
I don't know how mature or efficient Lean 4.1.0's standard feature support is.
However, I did enjoy an interesting case about benchmarking data processing languages.The challenge is to read a json ...
5
votes
1
answer
353
views
What is a deep embedding vs a shallow embedding? With examples?
I'm unclear on the terms "deep embedding" and "shallow embedding". I understand they are concerned with using one logic inside another, e.g. using Metamath/set.mm proofs in Lean ...
- 6,995
1
vote
1
answer
68
views
Use proof irrelevance in cast
I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
- 23
2
votes
2
answers
92
views
6
votes
1
answer
288
views
Benefits of HoTT compared with dependent type theory like what Lean does?
I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would ...
- 161
2
votes
0
answers
99
views
Highschool level linear algebra
I would like to be able to do high-school level linear algebra in Lean/Mathlib. However, it seems pretty hard. I do understand that mathematicians don't care about being able to do this basic stuff ...
- 163
2
votes
2
answers
113
views
Proving that a minimum example exists if any example exists in nat
I'm trying to prove that if a function from nat -> bool is true for any natural number, then there exists a minimum natural number which the function is true for.
I've been trying to find a good ...
- 125
0
votes
1
answer
54
views
Is the Archive of Formal indexed in journal databases?
I was wonder if journals that publish regularly formal proofs are indexed in journal databases like Scopus or Web of Science. Apparently, this is not the case. Why is it so?
- 101
6
votes
0
answers
67
views
How do I write a minimal working example (MWE) in Coq to demonstrate some problem?
To get help with some incomplete proof script or definition in Coq, or demonstrate some failing (e.g., Ltac) tactic or command, I am often asked to write a minimal working example (MWE) of Coq ...
- 385
3
votes
1
answer
160
views
1
vote
0
answers
55
views
Embedding proof assistance in an application
Context
Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes:
I have a project I'm toying around with, the core of which is what I'd call &...
- 111
2
votes
1
answer
92
views
Eta-equality for records: the case of semigroups
Consider the following definition of a semigroup:
...
- 75
0
votes
0
answers
78
views
Is there an algebreic type in lean4?
In lean4 I've seen the Real, Rat, and Int types, but is there an Algebreic type?
Loooking at:
https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/
which links ...
- 101
3
votes
1
answer
91
views
gappa seems to generate bad Coq
I'm using the -Bcoq backend of gappa.
The coq file contains dollar signs.
So far as I can tell, a coq file should not contain dollar signs.
Here is a snippet from -Bcoq :
...
2
votes
1
answer
149
views
Higher Observational Type Theory: variables becoming free in reduction rules
This question is based on the talks given by Mike Shulman on higher observational type theory (part 1, part 2, part 3).
In trying to understand the reduction rules of the calculus, I tried to work ...
- 73
2
votes
1
answer
190
views
4
votes
2
answers
123
views
How to think about writing Lean theorems
In Lean we make definitions and formulate theorems about the things we have defined. Seemingly, to each definition there exists several simple theorems. Let's go to ...
- 446
1
vote
1
answer
291
views
How to write this non-constructive proof in Lean?
There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational.
An interesting proof in classical logic is the following:
Consider $u = \sqrt{2}^{\sqrt{2}}$.
If $u$...
- 273
2
votes
1
answer
150
views
Understanding Mathlib/MeasureTheory Notation
I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
- 446
0
votes
1
answer
36
views
Automatic nightly Lean update?
I recently answered my own question for how to set up a Lean project with Mathlib dependencies. I realize I don't know everything about this. The route I follow starts by navigating to the correct ...
- 446
4
votes
1
answer
109
views
What is the precise meaning of "reducible"?
In Lean 4, I've seen the terms "reducible", "semi-reducible" and "irreducible" mentioned a lot. What is the precise meaning and how are these concepts used in code? When ...
- 163
5
votes
0
answers
204
views
Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination
Setup
Current Understanding
I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
- 73
7
votes
1
answer
213
views
How does Lean `simp` tactic work?
The doc at https://leanprover-community.github.io/extras/simp.html says about simp:
all it does is repeatedly replace (or rewrite) subterms of the form A by B, for ...
- 273
2
votes
1
answer
96
views
Lean: what does the syntax `variable [ring R]` mean?
I have written a simple Lean program, inspired by things I found here and there, which compiles as shown in the web editor:
...
- 273
6
votes
1
answer
244
views
(Dis)Advantages of basing a proof assistant on CH correspondence?
Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
- 273
3
votes
1
answer
45
views
How to prove across language boundaries about functions written in another language via FFI?
I know that a proof assistant can prove properties expressed in its own language. However, I find it desirable to call libraries written in other languages when using proof assistants. For example, I'...
- 1,700
3
votes
1
answer
332
views
Does lean 4 have built-in dictionary types?
Are there builtin dictionary/map types in Lean 4 prover?
I'd like to use dictionaries in my program and prove properties about it, but I am not sure if there is a dictionary type in Lean 4. A similar ...
- 1,700