All Questions

Filter by
Sorted by
Tagged with
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 . ...
tinlyx's user avatar
  • 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 ...
tinlyx's user avatar
  • 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 ...
Hamster's user avatar
  • 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 ...
paulotorrens's user avatar
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 ...
asha soroushpoor's user avatar
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 ...
Sheldon's user avatar
  • 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 ...
Greg Nisbet's user avatar
  • 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 ...
hmltn's user avatar
  • 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. ...
Andrey's user avatar
  • 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 ...
Chris Henson's user avatar
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 ...
kid111's user avatar
  • 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 ...
basicLeanWoes's user avatar
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 ...
Circuit Craft's user avatar
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 ...
Rainb's user avatar
  • 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 ...
uhbif19's user avatar
  • 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: ...
Tiago Campos's user avatar
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: ...
Tempestas Ludi's user avatar
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 ...
Ludovic Kuty's user avatar
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: ...
Felipe's user avatar
  • 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, ...
Rainb's user avatar
  • 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 ...
Abde Mojito's user avatar
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
Tim Eric's user avatar
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 ...
Jon's user avatar
  • 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 ...
Matheus C. França's user avatar
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 ...
Jason Rute's user avatar
  • 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 ...
Adrian L's user avatar
2 votes
2 answers
92 views

Simplifying Array Access

I'm confused how to show the second example here: ...
redjamjar's user avatar
  • 123
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 ...
ch271828n's user avatar
  • 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 ...
Adomas Baliuka's user avatar
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 ...
Tony Peterson's user avatar
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?
user1868607's user avatar
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 ...
palmskog's user avatar
  • 385
3 votes
1 answer
160 views

Understanding noConfusion

Data.List.getLast is defined as follows: ...
retonlage's user avatar
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 &...
Eric Anderson's user avatar
2 votes
1 answer
92 views

Eta-equality for records: the case of semigroups

Consider the following definition of a semigroup: ...
Jon's user avatar
  • 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 ...
Erotemic's user avatar
  • 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 : ...
Michael Hennebry's user avatar
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 ...
idka's user avatar
  • 73
2 votes
1 answer
190 views

iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq

...
Sheldon's user avatar
  • 123
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 ...
Alex Byard's user avatar
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$...
Weier's user avatar
  • 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 ...
Alex Byard's user avatar
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 ...
Alex Byard's user avatar
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 ...
Adomas Baliuka's user avatar
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 ...
idka's user avatar
  • 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 ...
Weier's user avatar
  • 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: ...
Weier's user avatar
  • 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 ...
Weier's user avatar
  • 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'...
tinlyx's user avatar
  • 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 ...
tinlyx's user avatar
  • 1,700

15 30 50 per page
1
2 3 4 5
17