# All Questions

1,073 questions
Filter by
Sorted by
Tagged with
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 ...
1 vote
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 ...
1 vote
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 ...
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 ...
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 ...
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 ...
• 181
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?
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 ...
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 ...
57 views

...
• 154
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 ...
• 3,095
1 vote
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 ...
• 167
244 views

### Uniqueness of proofs for inductively defined predicates

In Init/Peano.v the less-than-or-equal predicate is defined as follows: ...
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): ...
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 ...
• 249
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 ...
• 159
1 vote
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 ...
• 159
1 vote
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 ...
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. ...
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. ...
• 159
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 ...
• 3,095
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: ...
1 vote
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: ...
• 159
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 ...
• 3,095
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 ...
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 ...
• 3,095
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 ...
• 131
1 vote
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 ...
• 3,095
1 vote
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 ...