All Questions

Filter by
Sorted by
Tagged with
4 votes
0 answers
51 views

Introductory resources on rewriting logic

Hi I would like to grasp the theory behind Maude [1], [2] Are there any recommended video lecture notes, talks or introductory notes? I have been exposed to Functional Analysis, Topology and some Term ...
Vasileios Anagnostopoulos's user avatar
1 vote
1 answer
39 views

Lean Proving a Prop that has a match

I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem ...
opfromthestart's user avatar
1 vote
1 answer
360 views

Why does Agda use Set instead of Type?

In the 'Hello world' example in Agda — Agda 2.6.5 documentation, it straightforwardly uses Set as follows: ‘Hello world’ in Agda — Agda 2.6.5 documentation ...
shingo.nakanishi's user avatar
5 votes
2 answers
428 views

The relationship between "true formula" and types in the Curry–Howard correspondence

I have been working through the Implication World in the Natural Number Game using Lean from the following link: https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/0 While ...
shingo.nakanishi's user avatar
0 votes
1 answer
33 views

Automatic proofs after simp

My previous question about automatic proofs in Isabelle was answered by @BenjaminBisping pointing out how to use simp. However, here's a simple example which is the ...
Bjørn Kjos-Hanssen's user avatar
2 votes
1 answer
54 views

Proving factors of GCD in Dafny

While trying to prove various properties of GCD I ran into a proof I am a bit stumped with. Gcd can be defined as the max element in the intersection of the divisors of two numbers. In the code I used ...
Hath995's user avatar
  • 181
2 votes
1 answer
57 views

Properties of determinants in Isabelle

I would like to use the facts that $\det AB=\det A \det B$ and $\det A = \det A^t$ to prove that $\det AA^t = (\det A)^2$ in Isabelle. Is there a fast way to do this without doing this from scratch?
Craig Feinstein's user avatar
0 votes
0 answers
52 views

Arbitrary sorting of non-comparable elements? (Lean 4)

In Lean I'm working a lot with partial orders, and they have this property that not every element is necessarily comparable (i.e. for a, b in P where P is a partial order, it may not be true that ...
UmbralChrysanthemums's user avatar
0 votes
1 answer
73 views

Defining a Finset in Lean4

I am currently trying to define a finset (of a collection of finite images of some function). More specifically, given a fixed mapping between the maximal chains of a partially ordered set (of which ...
UmbralChrysanthemums's user avatar
2 votes
0 answers
57 views

Inconsistent failures of coercions when type checking in Coq

...
Feryll's user avatar
  • 154
2 votes
2 answers
110 views

Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain

I proved that $\mathbb{Z}[\sqrt{-2}]$ is an integral domain; I would like a review of this proof. My by hand argument is in Appendix A. It is not the original argument I used. I made a stupid mistake ...
Greg Nisbet's user avatar
  • 3,095
1 vote
1 answer
63 views

Prove that a function's result cannot dependent on Prop-valued parameters in Coq

Consider the following function elem and the lemma that the result of elem does not depend on the proof of ...
return true's user avatar
2 votes
3 answers
244 views

Uniqueness of proofs for inductively defined predicates

In Init/Peano.v the less-than-or-equal predicate is defined as follows: ...
Pavel Shuhray's user avatar
0 votes
0 answers
39 views

Found no matching subterm in goal while it does seem to be there when doing rewrite

I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not? First place (works fine): ...
The Coding Wombat's user avatar
2 votes
2 answers
119 views

Type inference with type classes in Coq

I don't understand type classes in Coq. I tried to use them as follows. I have a type cat that is supposed to represent the type of categories and I define the type ...
Bruno's user avatar
  • 249
0 votes
1 answer
30 views

What to import to use le_not_gt_iff?

According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it. I am trying to prove ...
kutschkem's user avatar
  • 159
1 vote
1 answer
46 views

Arguing with sumbools

I have the following definitions: Variables Sd_pre : nat -> Prop. Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }. Admitted. And the following are ...
kutschkem's user avatar
  • 159
1 vote
1 answer
57 views

Using Isabelle's Archive of Formal Proofs

I am new to Isabelle proof assistant and want to use it to verify a standard proof of the Bruck Ryser Chowla theorem. Since this theorem is about symmetric block designs, I figured that the folder ...
Craig Feinstein's user avatar
3 votes
2 answers
113 views

A $\mu$-recursive function converges at an input, how to find the output?

Summary: I want to implement an interpreter for $\mu$-recursive functions which, for any $\mu$-recursive function $f$ and input $\mathbf{x}$, returns $f \left( \mathbf{x} \right)$ if it is defined. ...
Kijeong Lim's user avatar
3 votes
2 answers
85 views

Using if in Fixpoint

I have this recursive function I am trying to define by way of Fixpoint, but the if condition is giving me trouble. ...
kutschkem's user avatar
  • 159
2 votes
3 answers
572 views

What is a positive coinductive type and why are they so bad?

What is a positive coinductive type and why are they so bad? This question is specifically within the context of Coq and is inspired by this question, the opening lines of which are: Since positive ...
Greg Nisbet's user avatar
  • 3,095
2 votes
2 answers
41 views

Determining the minimal index where lexicographically different lists diverge in Lean 4

I'm trying to define the smallest index at which two lexicographically different lists of equal length diverge. This is what I have so far: ...
UmbralChrysanthemums's user avatar
1 vote
1 answer
76 views

Best practices: Should I prefer definitions or iff when defining predicates?

I am a beginner in Coq, and I have a proposition I defined in this way: ...
kutschkem's user avatar
  • 159
5 votes
4 answers
3k views

Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

How do you prove that an Ascii character compares equal with itself in Coq idiomatically? In the course of trying to prove a random exercise in Logical Foundations, I wanted to prove the following ...
Greg Nisbet's user avatar
  • 3,095
2 votes
1 answer
107 views

Is there any way to approximate noncomputable functions in Lean4?

As you may know, there are some definitions in lean4 that can't be evaluated due to the noncomputable tag. Is there any way to approximate their value in lean4? For ...
ArshakParsa 's user avatar
2 votes
1 answer
72 views

Strategies for representing proofs of equality

I am interested in strategies for representing proof terms inside the kernel of a proof assistant, specifically proofs of equality. What are the different strategies that are available for ...
Greg Nisbet's user avatar
  • 3,095
3 votes
1 answer
207 views

Finding reflexive, transitive closure

I got a relation like: R: A -> A -> bool. Using this, I need to find an Rclose: A -> A -> bool such that ...
J...S's user avatar
  • 131
1 vote
1 answer
32 views

Feeding rewrites and other hints into an omnibus tactic

How do I feed rewrites that I've marked as safe into a custom tactic? I'm trying to write shorter Coq proofs with more of the easy stuff hidden. To that end, in the script below I proved that ...
Greg Nisbet's user avatar
  • 3,095
1 vote
4 answers
211 views

Formalizing "finite or infinite" in Coq

In Coq, I am trying to formalize the notion of a finite or infinite sequence, e.g. of natural numbers: call it a run, and call ...
Julio Di Egidio's user avatar
4 votes
1 answer
158 views

How to perform type conversion/coercion in Lean 4?

Does Lean 4 have a good way of handling data type conversion (e.g. between the natural and real numbers)? I am trying to solve the following property from the Mechanics of Proof book: $\forall a \in Z,...
tinlyx's user avatar
  • 2,220
1 vote
2 answers
250 views

Why did this proof succeed without function extensionality?

I'm very confused as to why a proof of a lemma succeeded without function extensionality. I'm messing around with some trivial Coq proofs for manipulating pseudosequences of the form ...
Greg Nisbet's user avatar
  • 3,095
3 votes
1 answer
117 views

How to use SSReflect to prove commutativity and associativity of addition idiomatically?

How do you prove commutativity and associativity of addition idiomatically using SSReflect? I am trying to learn SSReflect so I have another tool in my belt for ...
Greg Nisbet's user avatar
  • 3,095
2 votes
0 answers
20 views

Use of `by` on first line of lean proof - when to / when not to? [duplicate]

The following lean4 proof generates no warnings or errors. ...
Penelope's user avatar
  • 121
2 votes
1 answer
39 views

Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?

I have a Lean 4 test project in C:\Temp\MyProject I open with Visual Studio. In that directory, I have a Main.lean file. And, in ...
Jérôme Verstrynge's user avatar
5 votes
1 answer
119 views

Automatic proofs concerning inequalities

I've heard that Isabelle can be used to get automatic answers to questions like this: lemma "∃ x :: real . 2 /3 < x ∧ x < 3 /4" Of course, this one ...
Bjørn Kjos-Hanssen's user avatar
0 votes
1 answer
54 views

How to combine the PROP of a list of PROP in lean 4?

I have the following structures: structure MyElem where identifier : Nat acceptable : Prop structure MyList where elements : List ( MyElem ) I want to ...
Jérôme Verstrynge's user avatar
1 vote
2 answers
135 views

ACL2: Is there a way to check that a Skolem function does what it says on the tin?

I have been trying various things to try to prove that the product of two positive rationals is positive in ACL2, see here for one attempt. Recently, I entered the following Skolem function via ...
Greg Nisbet's user avatar
  • 3,095
1 vote
1 answer
55 views

Applying an axiom from a class in a proof

I'm trying to represent Boole-Schroder Algebra in Coq, and am trying to use apply to start a proof using one of my defined axioms, but I'm getting an "unable ...
Lisanna Dettwyler's user avatar
1 vote
1 answer
98 views

Trying to use 'Equations'

Examples from Chlipala's book https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html ...
Pavel Shuhray's user avatar
0 votes
1 answer
41 views

ACL2 Prove that the product of two positive numbers is positive

Here's a trivial book that proves that addition and multiplication of positive integers are positive. Interestingly, ACL2 can also prove out of the box that x + y ...
Greg Nisbet's user avatar
  • 3,095
2 votes
1 answer
70 views

Checking if a goal is *definitely wrong* by testing it against random examples in Coq

I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was <...
Greg Nisbet's user avatar
  • 3,095
1 vote
2 answers
70 views

Dependent equality in Coq

Let’s say that cat is the type of categories (I don’t think its precise formalization really matters here). I define the type of « initial structures » of a ...
Bruno's user avatar
  • 249
1 vote
1 answer
45 views

Showing that elements match after reducing list (Lean 4)

I'm currently trying to show that the elements of a reduced list match the original list after applying List.take. It feels obvious but it doesn't seem to be ...
UmbralChrysanthemums's user avatar
1 vote
2 answers
113 views

ACL2 compile single book on command line

How do you compile a book on the command line using ACL2? I'm looking for something akin to coqc for Coq. Consider the following book ...
Greg Nisbet's user avatar
  • 3,095
1 vote
1 answer
128 views

How to implement separate compilation?

This feels like a really basic question, but I haven't been able to find an answer to it. How should a proof assistant implement separate compilation? Maybe the answer is "just like any ...
Mike Shulman's user avatar
  • 3,200
0 votes
2 answers
79 views

Coq can you enter a tactic context inside of a `Fixpoint` definition?

I can use an opaque term created by a tactic in a Fixpoint definition. ...
Greg Nisbet's user avatar
  • 3,095
0 votes
0 answers
13 views

How do I fold a function over the bindings in a map in Isabelle?

Coq has the FMap modules, is there a similar Isabelle theory module? https://coq.inria.fr/doc/v8.19/stdlib/Coq.FSets.FMapInterface.html What I want to be able to do is fold a function over the ...
Glyn Webster's user avatar
0 votes
1 answer
59 views

Coq equivalent of Lean's `nth_rewrite`

Does Coq have an equivalent of Lean's nth_rewrite? rewrite ... at ... appears to specialize at its first unification site ...
Greg Nisbet's user avatar
  • 3,095
1 vote
1 answer
66 views

Lean4: Prove that ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) = ∑ x : Fin nn, k (Fin.castLE _ ↑↑x) (sums over Fin n)

Im working with sums over Fin n for some n : Nat, and I am stuck with two sums, that should be equal (and look exactly equal in ...
Urh's user avatar
  • 13
3 votes
0 answers
112 views

Lower bounds in type theory proof assistant with ordinals and universes without axioms

I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024? My ...
Ember Edison's user avatar

15 30 50 per page
1
2 3 4 5
22