# All Questions

342 questions
Filter by
Sorted by
Tagged with
112 views

### Is there a way to use higher order abstract syntax with linear types?

Is there a way to use HOAS style with linear types? I'm also interested in affine types or other substructural systems. I vaguely recall there has been some work for embedded DSLs for Haskell but I'm ...
• 1,721
81 views

### Recursive notations with forall quantifier

How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq? A similar notation (but without quantifiers) appears here ...
200 views

### Tracing the classical reasoner in Isabelle

Some time ago I asked this question on Stack Overflow but got no answer: https://stackoverflow.com/questions/60521384/tracing-tactics-in-isabelle Section 9.4 The Classical Reasoner of the Isar ...
• 163
437 views

### Lean: dubious noncomputability

In Lean, some definitions must be marked as noncomputable, for example if they depend on the law of the excluded middle or other nonconstructive choice principles. Usually, the reason for ...
55 views

### Unfolding expressions in Coq by one layer

Are there any ways to unfold an expression in Coq by a single layer? I have only come up with this obvious solution: ...
46 views

### SSReflect tuple constructor: why not use phantom?

I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
243 views

### auto-generating the proof of infinitude of primes

The chess computer which beat the human world champion in 1997 had a huge database of openings inbuilt into it. However my understanding of Deep Mind's alpha zero is that it is capable of generating ...
• 1,741
150 views

### What is a neutral term?

A neutral/normal term in the lambda calculus is typically defined data nf = Lam of nf | Neu of ne data ne = Var of int | App of ne * nf Now the question is what to ...
• 1,662
56 views

### What are some "real world" first order logical theories for demos?

I'm working on a tool for first order logical theories. I want to show the tool can work with real world logical theories. What are some good theories for demos? I think I want demos that are: ...
• 1,721
141 views

### Normalization by evaluation for extensional type theories

Is there material on how to implement normalization for (any flavor of) ETT? This describes techniques related to doing untyped normalization. But there are (operational and semantic) problems when ...
• 2,246
85 views

### Looking for an entry point in the universe of proof assistants and proof IDE's

This is my first question in this part of StackExchange. What I would like to achieve is the following. Suppose I want to study ( or give a course on ) basic Real Analysis, I want to 1) document the ...
67 views

### How to run the main function in lean 4?

I am following the lean 4 tutorial and see a main function as follows: ...
• 1,310
62 views

### What is focusing and how do I use it?

I have heard the term "focusing" with respect to the sequent calculus (System LK) and related calculi like the $\bar{\lambda} \mu \tilde{\mu}$-calculus. What is focusing and how do I use it? ...
• 1,721
97 views

### How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
511 views

### Construction of inductive types "the hard way"

Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine. But I'm curious about explicit constructions of recursive types within the theory. I know ...
• 1,721
73 views

### How to deal with axioms in a proof assistant?

I'm currently formalizing a little language which has somehow ended up looking a lot like Lawvere theories/finite product theories. I guess it's starting to look a little like Twelf? What I would love ...
• 1,721
195 views

### I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

Specifically, I think what's got me is showing that ∀x y z : ℕ, (z|x and z|y) → z|(x + y), or that ∀x y z : ℕ, (x mod y) = 0 → z mod y = (z + x) mod y, depending on how you want to look at it. I know ...
• 43
107 views

### What are instances of a dependent pair type?

Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a ...
• 133
832 views

### In Lean, contradiction tactic failed but actually goal accomplished

I've been playing with Lean, trying to prove the next lemma: lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) := ...
• 163
587 views

### Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

Question Is CiC stronger than CoC, in terms of proof strength? Context To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue: If I ...
133 views

### Turning off some sProp checks

In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination: (1) Every non-forced argument must be in sProp. (2) The return types of ...
• 856
67 views

### Display style proofs using Coq

How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq? PS: I'm rookie used coq.
49 views

### Tactic unification vs evarconv in Coq

I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a ...
• 497
719 views

### Do you need a Hilbert style Epsilon operator for definitions in set theory?

I've started to play with mechanizing some set theory stuff. I'm not sure if I want a constructive flavor or not yet. Anyhow you can do stuff like axiomize the empty set  \top \vdash \exists P. \...
• 1,721
152 views

### How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
• 433
144 views

• 4,136
245 views

### Examples of formalisation of abelian categories

The question I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
• 1,741