All Questions
342
questions
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 ...
- 1,721
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
...
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 ...
- 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 ...
- 909
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:
...
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....
- 21
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 ...
- 1,741
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 ...
- 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:
...
- 1,721
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 ...
- 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 ...
- 141
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:
...
- 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?
...
- 1,721
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 ...
- 53
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 ...
- 1,721
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 ...
- 1,721
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 ...
- 43
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 ...
- 133
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) :=
...
- 163
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 ...
- 119
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 ...
- 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.
- 41
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 ...
- 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. \...
- 1,721
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.
...
- 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 \...
- 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. ...
- 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 (...
- 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 ...
- 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 ...
- 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:
...
- 225
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 ...
- 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 ...
- 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:
...
- 225
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, ...
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 (...
- 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
...
- 41
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 ...
user1231
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 ...
- 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 ...
- 614
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 ...
user1231
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 ...
- 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 ...
- 83
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?
...
- 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 ...
- 225
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 ...
- 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
...
- 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:\...
- 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 ...
- 1,741
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 ...
- 383