All Questions
478
questions
2
votes
1
answer
29
views
How to unfold definitions in Lean / find the right theorems to apply?
After a few days playing around with Lean4, I notice I keep running into the problem of how to find the right theorems to apply. The situation below is one I run into particularly often, so perhaps I ...
- 113
1
vote
1
answer
51
views
Question about default definitions in fields
In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other ...
- 113
7
votes
2
answers
137
views
Why are impredicative constructions used less in type theory than in material set theory?
Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of ...
- 2,926
5
votes
2
answers
123
views
Unclarity about Preorder class in Lean4
I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be ...
- 113
2
votes
3
answers
76
views
Equality of records with members whose types are dependent (Lean 4)
(Previously, I asked
about converting a term a: A to a term of type B provided that A = B.
...
- 225
4
votes
1
answer
79
views
Is 'subsingleton elimination' the same concept as 'function comprehension'?
I saw:
subsingleton elimination from lean-forward, which, I so far understood as "eliminate a type in Prop to a type in whatever universe that we know has at ...
- 4,750
10
votes
3
answers
123
views
Given `A = B`, how to prove `a: A` also has type B in Lean 4
I guess my question can be reduced to implementing this function:
def abEq (A B : Type) (a: A) (ab : A = B): B := sorry
I am new to Lean 4 and started learning ...
- 225
5
votes
0
answers
90
views
Can we bring unification results under cofibrations outside?
Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do ...
- 4,750
4
votes
1
answer
119
views
Can we completely erase propositions in the type checker?
Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Suppose we have an impredicative universe of ...
- 4,750
3
votes
0
answers
21
views
.CoqMakefile.d required by CoqMakefile but not generated
I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2.
When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
- 31
1
vote
2
answers
233
views
Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?
In this question, I am talking about the language Pie described in the book The Little Typer.
One can derive that $0=1$ is contradictory:
...
- 317
5
votes
1
answer
197
views
Very dependent functions
A "very dependent function" is a function whose output type at input $n$ depends on its own output values at inputs $k<n$. Is there a precise definition of such things that makes sense ...
- 2,215
4
votes
1
answer
147
views
How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?
Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global ...
- 4,690
1
vote
2
answers
110
views
Does quantification over functions (STLC) increase strength beyond first order logic?
Does quantification over functions (STLC) increase strength beyond first order logic?
I want to add support for binders in my little constructive first order logic formalism I'm working on but I'm ...
- 2,422
3
votes
2
answers
898
views
Using proof assistants to generate fast code
Proof assistants allow to state that
$$A(BC) = (AB)C$$
with $A$,$B$,$C$ compatible matrices,
Is there a formal system that takes this sort of equations to choose among interpretation strategies of ...
- 139
3
votes
1
answer
119
views
Equality type and Propositions
I'm writing a library in the Lean computer proof assistant.
Evidently,
X : Type
x : X
y : X
#check x = y
Produces "Prop" and not "Type"; ...
- 73
2
votes
1
answer
103
views
Canonical forms of combinators
Binders are painful when dealing with metatheory. Combinators are one potential approach to avoid the pain of binders. But it'd be nice if I could normalize combinators to canonical forms. Is there ...
- 2,422
1
vote
2
answers
55
views
Suppressing notation in Lean
I'm using the Lean computer proof assistant and customizing some notation. Here's the example I'm working with:
...
- 73
0
votes
2
answers
107
views
Coproducts in Lean
All,
I am using Lean. I am hoping to obtain a coproduct construction which works something like this:
...
- 73
1
vote
1
answer
106
views
Does Agda's --injective-type-constructors flag have canonicity?
Since 2010/01/07, when the Anti-classicality of Agda was proved by Chung-Kil Hur, Agda's --injective-type-constructors is separated from the main branch of Agda (...
- 109
1
vote
1
answer
84
views
Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression
In this question, I am talking about the language Pie described in the book The Little Typer.
Consider the definition
...
- 317
1
vote
1
answer
69
views
Inductive types associated to instances of a structure in Lean
I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example.
In it I have a structure Graph. I want to ...
- 73
-2
votes
1
answer
183
views
A project in Lean which involves "programming"
all,
I have a project in Lean which turns out to involve some features which might better be called programming. So, for that part of the project, I was thinking I would treat Lean like it is Python ...
1
vote
1
answer
76
views
Making a finite graph type in Lean - introduction rule
I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set&...
0
votes
0
answers
47
views
If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?
From $\mathbb{Q}$, the set of all rational numbers, I make some new structure $I$, and also make strict order and (equivalence) equality on $I$.
I want to use rewrite tactic for my defined relations (...
- 285
2
votes
1
answer
60
views
Why does an internal term produced by Lean's equation compiler have holes in it?
Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
- 35
1
vote
1
answer
111
views
Can I unfold not all things but only one thing in Coq?
For example,
Example example (a b c : Q) :
(a * b) * c == a * (b * c).
Proof.
unfold Qmult.
This code show me this screen.
...
- 285
0
votes
1
answer
40
views
How can I correspond a hypothesis to a decidable axiom in match (in Coq)?
I made some record structure $I$ with addition and equality. And I made an axiom.
Axiom I_dec :
forall a : I, ({0 < a} + {a < 0}) + {a == 0}.
With this ...
- 285
6
votes
1
answer
163
views
How to implement a visual proof assistant?
Higher structures in category theory lead very organically to visual or graphical interpretations in terms of string diagrams and commuting squares. However, it seems hard to implement a graphical ...
- 2,422
1
vote
1
answer
49
views
How can I use a (three terms) decidable axiom in a case analysis?
In Coq, I made some record structure $I$ and also make a strict order and equality $<$ and $==$.
And I showed that $a < b$ or $a == b$ or $b < a$ for every $a, b \in I$.
...
- 285
1
vote
1
answer
79
views
How do I prove this property in Coq?
I am working on a variant of an example by Christine Paulin-Mohring. It represents in Coq the Needham-Schroeder protocol in the (flawed) public key version. I would like to prove that the protocol is ...
- 135
2
votes
1
answer
80
views
Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?
I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
- 123
2
votes
1
answer
92
views
Natural deduction with coq assistant prover
I want to mimic natural deduction proofs in coq ; for instance the proof I made for "A /\ B -> B /\ A" is for now
...
- 123
4
votes
2
answers
146
views
Formalization of abstract definitions
I'm asking about the abstract keyword in Agda and equivalent features in other languages. It marks a definition as non-expandable, potentially speeding up ...
- 2,926
4
votes
1
answer
75
views
How can I search only all of the lemmas in a different module (in Coq)?
I usually import QArith.
If I write
Search "max" "id".
Then I can see something like this:
...
- 285
7
votes
1
answer
201
views
Can you build W-types out of natural numbers predicatively?
I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, ...
- 251
5
votes
1
answer
97
views
In lean, how do I expand a definition without knowing what it is?
Suppose I have a goal of proving
$a \lt b$
But I don't how < is defined. Maybe it's defined as $\exists c \in \mathbb{N}. a + c + 1 = b$ or maybe it's defined ...
- 197
1
vote
2
answers
83
views
In lean, how to work around "invalid pattern, 'x' already appeared in this pattern"
I am trying to define what it means for an item to be in a list. I wrote this case breakdown:
...
- 197
1
vote
2
answers
324
views
What is the remaining goals on the shelf?
When I prove a theorem in Coq, I made a hypothesis that is 'False',
and by using 'contradiction' tactics, I finish my proof.
However, the coq program show some words for me.
...
- 285
2
votes
1
answer
123
views
What are references for learning type theory?
What could be a good set of references for starting to learn type theory? We can assume that the students have a computer science background but not specifically on functional programming or lambda ...
- 135
3
votes
2
answers
332
views
In lean, why is it possible to prove zero_ne_succ (without adding it as an axiom) by using pattern matching?
If I define a custom set of natural numbers:
inductive mynat : Type
| zero : mynat
| succ : mynat → mynat
I can prove no successor is equal to 0 by defining a ...
- 197
0
votes
2
answers
80
views
How to define two mutually recursive functions in Coq?
I make such codes, and cannot preceed.
...
- 285
1
vote
1
answer
51
views
Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?
In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
- 35
1
vote
1
answer
67
views
Proving that applicative functors compose
For simplicity, here an applicative functor means (in a proof assistant based on dependent type theory) the Haskellian applicative functor, bundled with its equational laws.
This I can of course brute ...
- 2,926
0
votes
1
answer
67
views
Prove in Lean that ∀ i, 0 ≤ X i → ∃ i, X i > 1 → ∑ i, X i > 1
How to prove that if a term in a sum is > 1 then the sum is > 1?
...
- 173
1
vote
1
answer
105
views
Can I prove this axiom without using excluded-middle property?
I define the following axiom.
(First, I want to prove it, and make it Theorem.
However, I can not find how to start.)
...
- 285
2
votes
2
answers
63
views
1
vote
2
answers
54
views
Is there a tactic in Coq to make a hypothesis from applying two hypotheses?
Suppose in Coq we have the following hypotheses:
x, y, z: Z
H : x < y
H0 : y < z
and I would like to introduce also the hypothesis
...
- 285
3
votes
2
answers
106
views
Coq: can `tauto` be used to prove classical tautologies?
When I experiment, I get inconsistent results.
Running the following code (with a proof included to double-check that it's provable)
...
2
votes
2
answers
153
views
Reference request for an introduction to higher-order logic
I'm looking for an introductory text or other materials on higher order logic, with a minimum of assumed background knowledge beyond first order logic.
- 389