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.
20
questions
4
votes
1
answer
89
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 ...
- 3,678
2
votes
1
answer
89
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
113
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,231
0
votes
1
answer
56
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 ...
- 43
1
vote
2
answers
106
views
2
votes
1
answer
106
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 ...
- 145
4
votes
3
answers
222
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
83
views
Destruction of bound dependent types
I'm having an issue with dependent typing. I have reduced it to the following minimal example:
...
- 13
2
votes
1
answer
199
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 ...
- 6,713
2
votes
1
answer
150
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 ...
- 263
0
votes
1
answer
142
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, ...
- 195
4
votes
2
answers
190
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,748
9
votes
2
answers
425
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,141
11
votes
2
answers
377
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
155
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 ...
- 3,678
3
votes
2
answers
166
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
8
votes
1
answer
339
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 ...
- 6,713
16
votes
2
answers
329
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
174
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
19
votes
2
answers
374
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? ...
- 400