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
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