Questions tagged [equality]
Questions pertaining to equality in type theory (all kinds of equality are included: judgemental, propositional, observational, setoid equality, etc.) and equality reasoning in proof assistants.
32
questions
2
votes
1
answer
74
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
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 ...
- 249
11
votes
5
answers
2k
views
How do real-world proof assistants bind variables and check equality?
There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.
There are also ...
2
votes
1
answer
41
views
Rewriting/Applying unidirectional morphisms in Coq
Link to Code Gist
I have the following definition
...
- 1,502
1
vote
1
answer
77
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 ...
- 1,502
4
votes
1
answer
267
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.
...
1
vote
1
answer
100
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 ...
- 411
0
votes
0
answers
119
views
MLTT with first-order reasoning and equality-reasoning information preservation
Terms in Extensional MLTT don't contain equality-reasoning information (implicit transports), effectively meaning data is lost, which is bad. But at the same time, higher-order reasoning (reasoning ...
- 345
3
votes
1
answer
163
views
Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?
The short version:
Is this statement correct? If it is, is it provable in Coq?
...
- 33
1
vote
1
answer
225
views
how to prove 2+2+a=4+a in lean4?
It should be simple but dig it for a while and still not successful.
theorem example (a : R) : 2 + 2 + a = 4 + a := ...
can someone help to figure out how to do next? many thanks
- 11
1
vote
1
answer
84
views
Use proof irrelevance in cast
I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
- 23
2
votes
1
answer
105
views
Eta-equality for records: the case of semigroups
Consider the following definition of a semigroup:
...
- 75
4
votes
1
answer
100
views
General method for disproving possibility of judgemental equality
There is a slick definition of categories (as a record type with eta-equality) such that taking the opposite category twice results in the original one judgementally. Similar tricks seems to exist for ...
- 4,025
2
votes
1
answer
106
views
Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?
Suppose we work inside MLTT with equality reflection (extensional MLTT).
Assume I postulate existence of Streams as final co-algebra for the suitable functor.
Is that enough to prove the bisimulation ...
- 345
1
vote
1
answer
147
views
How to deduce this equality based on the fact that these two terms must be the same?
Brief (but possibly inaccurate) Summary:
I have a proposition H : Prop1 p q. When I use inversion on the proposition, I get ...
- 1,502
0
votes
1
answer
69
views
Reasoning about non reflexive equalities & type conversions
Following-up from the answers to this question, reasoning about conversions between types that have decidable equalities is somewhat trivial (here I'm taking nat as ...
- 63
1
vote
2
answers
195
views
2
votes
1
answer
179
views
Equality of two functions
I am wondering about definition of functions in Lean and proving equality (in some sense to be defined) of two functions.
Note: I have consulted the answer to the following related question but it ...
- 167
4
votes
3
answers
452
views
Rewrite with definitional equality and dependent types
In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
- 193
1
vote
1
answer
121
views
Destruction of bound dependent types
I'm having an issue with dependent typing. I have reduced it to the following minimal example:
...
- 23
2
votes
1
answer
246
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:
“algorithmic” definitional ...
- 9,195
2
votes
1
answer
270
views
Definitional vs propositional equality
Theorem Proving in Lean highlights a distinction between definitional and propositional equality when creating recursive functions:
The example above shows that the defining equations for ...
- 273
1
vote
2
answers
180
views
Equational reasoning in Coq
I've been doing some exercises on Coq, and have stuck for the next problem:
Let T: Set with 2 operations f, ...
- 205
4
votes
2
answers
261
views
Why do coinductive types require bisimilarity relations?
I was messing around with induction stuff again and some stuff seems to require bisimilarity relations instead of just equality when dualizing for coinductive types.
...
- 2,868
9
votes
2
answers
468
views
Defining coercion for proof irrelevant equality
Say I would like to define coercion for proof irrelevant equality between types. In Coq I try
...
- 2,300
11
votes
2
answers
415
views
Proving uniqueness of an instance of an indexed inductive type
Consider the simple indexed inductive type
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Intuitively, I ...
- 213
10
votes
0
answers
175
views
What are the practical differences between intensional and extensional type theories?
It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
- 4,025
3
votes
2
answers
214
views
How do I make use of an irrelevant equality in a proof?
open import Agda.Primitive
import Relation.Binary.PropositionalEquality as Eq
open Eq public
open Eq.≡-Reasoning
Suppose I have a dependent pair whose second ...
- 151
11
votes
1
answer
544
views
How does Metamath Zero handle CIC as in Lean or Coq?
Metamath Zero (MM0) is a proof assistant developed by Mario Carneiro. It has a metalogic very similar to the metalogic of MetaMath, but it also borrows design choices from Lean (and maybe other ...
- 9,195
16
votes
2
answers
406
views
What are the upsides and downsides of typed vs untyped conversion?
What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?
Background
Generally speaking, in dependent type ...
- 394
8
votes
1
answer
181
views
Is there an elegant way of proving an equality A=B by going in both directions?
I would like to prove an equality by splitting it into a proof in each direction.
Is there a more elegant style to start such a proof than this way::
...
- 81
20
votes
2
answers
745
views
What is the difference between refl and rfl in Lean 3?
I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
- 410