All Questions

Filter by
Sorted by
Tagged with
4 votes
1 answer
374 views

Does "unique mere existence" imply "existence"?

Hopefully this question fits in well here. I'm hoping that more people who know the answer will see it here than on somwehere like mse, but please let me know if you'd rather I move it there! Say you'...
Chris Grossack's user avatar
3 votes
0 answers
66 views

Inductive from CoInductive?

It is possible to represent CoInductive using parts that are Inductive. As a simple example, ...
scubed's user avatar
  • 131
2 votes
1 answer
56 views

Lean4 instance management

I have a group $G$ and $G$-sets $X$ and $Y$. I would like to let $G$ act on the type $(X\to Y)$ by the usual rule $(g\bullet u)(x)=g\bullet u(g^{-1}\bullet x)$. I define a ...
Neil Strickland's user avatar
0 votes
0 answers
107 views

Trouble proving a theorem using induction in Coq

Theorem five_and_three: forall i, exists a b, i + 8 = 3 * a + 5 * b. I'm currently using these tactics: ...
camsterwheel's user avatar
1 vote
1 answer
54 views

How do I enable this kind of rewriting?

Link to Code Gist Given two extensionally equal sets, s1 ≡ s2, I want to be able to obtain a ∈ s2 from ...
Agnishom Chattopadhyay's user avatar
-4 votes
0 answers
80 views

Proof for Question V.10

Problem IV.10 Prove that any number greater than seven can be written as a sum of multiples of three and five. The Coq statement is Theorem three_and_five : forall n : nat, exists (a b : nat), n + 8 = ...
Siam's user avatar
  • 1
4 votes
1 answer
216 views

Dealing an equality with coq. - beginner's question

I am studying the sf book - ProofObjects.v file. I'm confused with "equality__leibniz_equality_term" exercise. ...
ignorant student's user avatar
0 votes
1 answer
56 views

Coq, Merging two forall definitions ranging over the same types

...
The Circle's user avatar
1 vote
1 answer
86 views

Applying universally quantified equalities to propositions

In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one ...
Jozef Mikušinec's user avatar
3 votes
0 answers
47 views

Bounding Volume Proof Assistant Library

I am interested in learning Lean/Coq/Isabelle etc. and wanted to try to formalize Joseph O'Rourke's Minimum Bounding Box Algorithm. I do not have much experience with proof assistant tools. Is there a ...
WakkaTrout's user avatar
0 votes
1 answer
69 views

Using lean4 to prove subset properties

I'm learning Lean4. I'm trying to prove in lean4 these basic properties of subsets: $ X \subseteq X $ $ X \subseteq Y , Y \subseteq Z \Rightarrow X \subseteq Z$ $ X \subseteq Y , Y \subseteq X \...
teoobo's user avatar
  • 3
1 vote
1 answer
29 views

Lean 4 directive to always include a section variable

Here is something that I think used to work in Lean 3, although I no longer have a working installation of Lean 3 with which to check that the details of this minimal example are precisely correct. I ...
Neil Strickland's user avatar
2 votes
1 answer
69 views

Negating universal/existential quantifier in type theory, propositions on elements of the empty type

The universal/existential quantifier: In classical logic, ~∀x P(x) is equivalent to ∃x ~P(x). Looking at the existential quantifier in Lean4, the object ∃ x:nat P(x) is essentially the tuple (x:nat, P(...
Snowybluesky's user avatar
2 votes
1 answer
344 views

How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?

I found the definition of Nat's but lean still complains that it doesn't exist. Why is it? ...
Charlie Parker's user avatar
1 vote
2 answers
112 views

Topic for undergraduate thesis

I'm an undergraduate student in my final year studying applied mathematics. To graduate, I need to present a thesis, and I'm considering using Lean and first-order predicate logic for my thesis. My ...
Hackerman's user avatar
  • 111
5 votes
2 answers
913 views

How do I express a negative premise in Coq?

I would like to express a transition system in the style of the small-step operational semantics as found in volume 2 of "Software foundations". Unfortunately my transition system has rules ...
Pietro Braione's user avatar
2 votes
1 answer
80 views

How to use a lemma that is defined in a Coq module?

How can I use the Lemma div_0_l from the standard library? Somehow I cannot instantiate the module that is defined as ...
The Circle's user avatar
5 votes
0 answers
150 views

Coq - Are there functions which are provably equal but not definitionally equal?

In Coq, are there types A,B and functions f, g : A -> B such that f = g propositionally ...
Patrick Nicodemus's user avatar
2 votes
1 answer
65 views

Packaging Mathematical Structures in Coq: Help Understanding a Definition

Context I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to ...
user2628206's user avatar
3 votes
2 answers
49 views

What is the most ergonomic way to eliminate multiple similar goals in Coq?

I recently bumped into some theorems that can be proved easily but not very elegantly. It is not elegant because when I was doing case analysis, Coq discharged many goals, but most of them can be ...
Hiroki Chen's user avatar
-3 votes
0 answers
57 views

What are some examples of very large term enumerations of a proof assistant language?

I’m just curious to know of significant instances of brute force, total enumeration of all terms in a logical theory. For example, enumerating every term of ZFC - how far has anyone gotten? What are ...
Julius Hamilton's user avatar
1 vote
0 answers
97 views

Proving Quine's notion that identity belongs to logic within type-constrained proof assistants

I'm having difficulty generalizing the following proof to permit predicates of any finite arity. Consider the following axioms of identity consistent with W. V. O. Quine's argument that relative ...
James Bowery's user avatar
4 votes
2 answers
87 views

what symbols can I use in coq?

Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?
RataMágica's user avatar
2 votes
0 answers
22 views

Extract explicit value from Isabelle proof

How can I extract an explicit value for a schematic variable in Isabelle after using it in a proof? For example, in the following goal, I’m looking to extract a numerical value for ...
Jimmy's user avatar
  • 21
1 vote
2 answers
109 views

What is the $\mu$ in the labmda calculus defined here?

In the Lambda: Introduction to Lambda Calculus chapter of PLFA, it has the following definition for the lambda calculus, which includes a $\mu$ operator that I haven't seen before. Syntax of terms ...
tinlyx's user avatar
  • 2,034
4 votes
2 answers
648 views

In a dependently typed language, are all types statements?

In dependently typed languages such as Agda, Lean, Coq, Idris (and Pie), a mathematical or logical statement can be expressed as a type, and then proven by writing a program that creates an instance ...
Mars's user avatar
  • 141
0 votes
0 answers
48 views

Analysis of proof that for a category which is also a poset, every diagram commutes

A poset may be defined as a set (axioms of ZFC go here to define "set") and a binary relation (which is taken as a primitive notion in first-order logic), which meets these conditions: $a R ...
Julius Hamilton's user avatar
0 votes
1 answer
31 views

Tactic to Propify a bool expression

Let's say I have bool expressions <bexp> consisting of true, false, variables, ...
Agnishom Chattopadhyay's user avatar
2 votes
1 answer
47 views

Pattern Matching on List x Fin

So, here is the example I'm working on: ...
redjamjar's user avatar
  • 165
3 votes
2 answers
114 views

Lean4: How to construct an HEq between dependent functions?

I have an extremely simple goal to prove: HEq (fun px rd => match px, rd with | Sum.inr _ppos, dir => dir) fun x => id The reason the match ...
André Muricy's user avatar
0 votes
0 answers
30 views

Coq: Language server crashes when trying to introduce an equality-hypothesis

I'm working in Coq in VSCode (using VSCoq). Repeatedly the Coq language server crashes. I try to prove the following: ...
name1les's user avatar
3 votes
2 answers
58 views

Creating a tactic for 'destructing' a list by last element?

Sometimes, I have a context in which I have some l : list X, and I want to prove the goal by proving that (1) If l = [], the ...
Agnishom Chattopadhyay's user avatar
2 votes
0 answers
77 views

Why does the following Coq code fail to meet Coq's positivity requirement for inductive types?

I'm currently studying a proof of Gödel's incompleteness theorem written in Coq, by Russell O'Connor. I would like to understand the following section: 2.2 Definition of Term For any given language, ...
Julius Hamilton's user avatar
1 vote
1 answer
47 views

What is an assumption in Isar?

I have the following code: lemma assumes "A" shows "A ∧ A" proof - show "A ∧ A" apply (rule conjI) apply assumption Now, ...
Gergely's user avatar
  • 311
1 vote
1 answer
87 views

Assistance using destruct on an equality proof for functors

Context I am currently learning how to use the Coq proof assistant and am at the level where I know the fundamentals of dependent-type theory and have done most of the "Software Foundations" ...
user2628206's user avatar
1 vote
1 answer
49 views

Termination for Wrapped Fin in Lean4

The following example type checks in Lean 4, but I am confused why the termination_by declaration is required. ...
redjamjar's user avatar
  • 165
2 votes
1 answer
196 views

Conflicting terminology for completeness/soundness of normalization algorithm

While reading some articles about formalization of various normalization algorithms, I found that these two papers use the term completeness/soundness in opposite way. Hereditary Substitutions for ...
damhiya's user avatar
  • 123
3 votes
2 answers
189 views

Has extensionality ever caused any problems in a mathematical proof?

I read the following about extensionality in PLFA, Agda does not presume extensionality, but we can postulate that it holds: ...
tinlyx's user avatar
  • 2,034
5 votes
2 answers
568 views

In Coq, what tactic can I use to remove a True precondition from a hypothesis

One of my hypothesis is an implication with an always-true condition (x=x->P). What tactic can I use to rewrite this hypothesis into its conclusion ...
hugomg's user avatar
  • 153
2 votes
1 answer
73 views

How to find the data type of a Json value that in lean4, to perform type validation. (Functional programming in lean)

Basically I am taking in a json object in lean4 as input and I want to check whether a particular feild like 'age' should always be Nat not something else depending on the schema that the user has ...
Ashmit's user avatar
  • 21
3 votes
2 answers
237 views

How to convert Agda's with statement to a helper function?

I read here that Every use of with is equivalent to defining a helper function But I couldn't get it working with trying to re-implement a with-clause (which itself came from re-implementing the ...
tinlyx's user avatar
  • 2,034
1 vote
0 answers
53 views

How to choose an axiom system in Isabelle/HOL?

First of all, sorry if my question is too nonsensical and naive, I'm just getting started with Isabelle/HOL. I am reading Hou's "Fundamentals of Logic and Computation: With Practical Automated ...
Red Banana's user avatar
4 votes
3 answers
165 views

For formal proofs of graph structures and algorithms, which proof assistant should I learn?

My goal is to be able to make formal proofs for graph structures and algorithms, proving i.e. for every vertex in a directed-acyclic-graph there exists a path from a source vertex to that vertex, or i....
Snowybluesky's user avatar
0 votes
1 answer
53 views

Proving non-existence of "least" subtype generator in Coq

I'm working through Programming Language Foundations in my free time. In the subtyping chapter, I am greeted by the following exercise, where TF P := P \/ ~ P: <...
Charles Averill's user avatar
0 votes
1 answer
60 views

How does one define a structure with the ext theorem in Lean 4?

I get this error: unknown attribute [ext] and my code is literally a copy paste of the code from mathematics in lean: ...
Charlie Parker's user avatar
2 votes
1 answer
44 views

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (...
tinlyx's user avatar
  • 2,034
5 votes
4 answers
1k views

How to prove non-existence of terms that contain themselves in Coq

Why can't inversion figure out that it isn't structurally possible for a term to contain itself? Here's a basic example: ...
Charles Averill's user avatar
3 votes
1 answer
366 views

How to provide proof for termination in Agda?

I am trying to write an integer division function from scratch in agda2 (as of 2.6.3): ...
tinlyx's user avatar
  • 2,034
0 votes
0 answers
40 views

Create an olog for Wikipedia policy

I really want to try my hand at formalizing some kind of conceptual argument as an olog, after David Spivak. There are so many unknowns at the same time that I would really appreciate external ...
Julius Hamilton's user avatar
2 votes
1 answer
131 views

How to recover implicit arguments of inductive types in a match expression?

def IsEven: Nat → Prop | Nat.zero => True | Nat.succ pred => ¬IsEven pred inductive Example: Nat → Prop | IsExample: IsEven n → Example (n + 10) Here, ...
Jozef Mikušinec's user avatar

15 30 50 per page
1
2 3 4 5
20