# All Questions

478 questions
Filter by
Sorted by
Tagged with
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 ...
1 vote
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 ...
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
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 ...
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. ...
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
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 ...
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
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
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 ...
1 vote
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
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
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
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
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
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"; ...
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
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: ...
107 views

### Coproducts in Lean

All, I am using Lean. I am hoping to obtain a coproduct construction which works something like this: ...
1 vote
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
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
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 ...
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
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&...
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
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
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
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
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
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
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 ...
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 ...
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
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
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
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
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
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
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
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 ...
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
80 views

### How to define two mutually recursive functions in Coq?

I make such codes, and cannot preceed. ...
• 285
1 vote
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
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
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
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
63 views

• 285
1 vote
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
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) ...