All Questions

Filter by
Sorted by
Tagged with
3 votes
1 answer
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 ...
user avatar
3 votes
0 answers
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 ...
user avatar
6 votes
1 answer
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 ...
user avatar
  • 163
2 votes
2 answers
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 ...
user avatar
3 votes
0 answers
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: ...
user avatar
2 votes
0 answers
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....
user avatar
11 votes
1 answer
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 ...
user avatar
6 votes
1 answer
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 ...
user avatar
  • 1,662
3 votes
0 answers
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: ...
user avatar
9 votes
1 answer
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 ...
user avatar
  • 2,246
4 votes
1 answer
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 ...
user avatar
3 votes
2 answers
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: ...
user avatar
  • 1,310
7 votes
0 answers
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? ...
user avatar
5 votes
1 answer
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 ...
user avatar
8 votes
3 answers
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 ...
user avatar
3 votes
0 answers
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 ...
user avatar
2 votes
4 answers
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 ...
user avatar
3 votes
1 answer
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 ...
user avatar
6 votes
1 answer
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) := ...
user avatar
11 votes
3 answers
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 ...
user avatar
4 votes
2 answers
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 ...
user avatar
  • 856
4 votes
0 answers
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.
user avatar
4 votes
0 answers
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 ...
user avatar
  • 497
14 votes
3 answers
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. \...
user avatar
5 votes
2 answers
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. ...
user avatar
  • 433
4 votes
1 answer
144 views

In (CHM/CCHM) cubical type theory, how to conversion-check face formulae?

In my impression (also according to Amelia in her discord server), some non-syntactically equal face formulae should be definitionally-equal (denoted $\equiv$): $(a = 1 \land b = 1) \equiv (b = 1 \...
user avatar
  • 4,136
12 votes
0 answers
147 views

How do Coq's bidirectionality hints (`&`) affect type checking?

I have used Coq's bidirectionality hints (placement of & in a call to Arguments) to some effect, mostly by trial and error. ...
user avatar
  • 497
9 votes
1 answer
242 views

Current status of cubical inductive families

I have the impression that cubical type theory hasn't dealt with inductive families yet. But the only source on this matter I can get is this Agda issue. What I've gathered is Agda supports defining (...
user avatar
  • 2,246
9 votes
1 answer
531 views

What axioms do I need to search the naturals?

Theorem search {P : nat -> Prop} (dec : forall n, {P n} + {~P n}) : ~~(exists n, P n) -> {n | P n}. Admitted. I don't think this is provable in Coq without ...
user avatar
  • 303
13 votes
3 answers
647 views

How to extract the witness from exists in Coq in function notation/without destructing?

Assuming I have some definition with a forall and an exists like so: Definition fooable A B P := forall a : A, exists b : B, P a b. Then on an intuitive level, I ...
user avatar
  • 233
5 votes
0 answers
86 views

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
user avatar
6 votes
2 answers
146 views

Policies on introducing free variables when rewriting?

When using a fact like x = y <=> x + z = y + z as a rewrite rule, it can be desirable to introduce an unused free variable into the result of the rewrite ...
user avatar
  • 295
4 votes
1 answer
128 views

Tutorial implementation of analytic tableaux

I am re-reading John Harrison's wonderful Handbook of Practical Logic and Automated Reasoning, and he has a rather idiosyncratic presentation of analytic tableaux. What other tutorial implementations ...
user avatar
  • 1,357
3 votes
1 answer
73 views

Found type UU where "?T" was expected

I am trying to solve a couple of exercises in coq. However, with the following code: ...
user avatar
8 votes
2 answers
410 views

Curly Braces and Lambdas in Agda

The docs on lambdas in Agda provide two forms of lambda: a curly brace based version, and the where syntax. But while writing some programs, I stumbled across a third version: one pattern, no braces, ...
user avatar
7 votes
0 answers
95 views

Tutorial implementations of extensional type theories

There are cool projects out there that covers the basic principles of implementing dependent type theories as very spartan proof assistants. These projects helped a lot when I learned about (...
user avatar
  • 2,246
3 votes
3 answers
426 views

How can I prove this theorem with induction in Coq?

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1). where sum_n2 is defined ...
user avatar
6 votes
1 answer
184 views

How to replace a function by its body

I have this function: Definition bexp x y := bexp_r x y [true]. And I have this goal: value (bexp [] y) = 0 ^ value y I want ...
user avatar
2 votes
1 answer
166 views

Lemma about splitting of homogeneous polynomial equations into irreducible equations

Proof assistants, and Lean, are completely new to me. How can I derive the following simple lemma in Lean? How can I let Lean check if the lemma is correctly written? How can I let Lean check if the ...
user avatar
  • 131
12 votes
1 answer
434 views

Lean "nonempty" vs "inhabited"

In the init/logic.lean file of the Lean 3 standard library, nonempty and inhabited are defined. It seems like these two classes ...
user avatar
6 votes
2 answers
245 views

Problem proving a binary add function

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront). I have created this badd function that ...
user avatar
8 votes
2 answers
650 views

Explanation of Coq math-comp repositories

How are the Coq math-comp account and repositories related? Details One of my side goals is to try to keep the tags on this site meaningful and useful. Today I ran into this question: How to prove ...
user avatar
  • 2,676
8 votes
1 answer
213 views

Kunen's inconsistency axiom-free proof on Metamath

Kunen's inconsistency theorem is an important theorem in set theory on upper bounds for large cardinals. It has long been thought to be able to be encoded on ZFC, but the full implementation has never ...
user avatar
4 votes
1 answer
95 views

How can I prove has_esp when using mathcomp.analysis?

How can I prove the following goal (which I believe to be true) using mathcomp.analysis? ...
user avatar
  • 157
4 votes
1 answer
154 views

Cannot discriminate `0 = 1`

I am just practicing a bit with coq, doing some UniMath exercises and am trying to prove (0 = 1) -> empty. However, for some reason, I seem unable to reason ...
user avatar
5 votes
2 answers
64 views

How to provide a countType when using mathcomp?

The following snippet can't pass type checking. From mathcomp Require Import choice. Definition exfn (A:countType) := false. (* Fail *) Check exfn nat. Failed with ...
user avatar
  • 157
9 votes
2 answers
367 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
user avatar
  • 1,662
10 votes
1 answer
223 views

How to implement the type checking of `transp` in de Morgan cubical type theory?

I am reading many referential materials and I want to find a proper way to implement it. Suppose the syntax is ${\sf transp}~A~\psi:A~0\to A~1$, where (let's call it "the condition") $A:\...
user avatar
  • 4,136
20 votes
1 answer
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 ...
user avatar
8 votes
1 answer
155 views

What should be cited for "the Calculus of inductive Constructions"?

The history of dependent data types spans decades and is a bit confusing. I have seen some implausible claims about which documents present what. I would like to get it right for my own work without ...
user avatar

15 30 50 per page
1
2 3 4 5
7