All Questions

Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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. ...
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 ...
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 ...
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 ...
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"; ...
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 ...
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: ...
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: ...
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 (...
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 ...
-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 (...
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. ...
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 ...
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 ...
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$. ...
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 ...
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 ...
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: ...
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 ...
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: ...
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. ...
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 ...
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 ...
0 votes
2 answers
80 views

How to define two mutually recursive functions in Coq?

I make such codes, and cannot preceed. ...
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? ...
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.) ...
2 votes
2 answers
63 views

When I destruct record, can I make a hypothesis name without 0?

I made such record. ...
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 ...
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.

15 30 50 per page
1
2 3 4 5
10