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.
13
questions
2
votes
1
answer
64
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,073
1
vote
2
answers
68
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
40
views
Rewriting/Applying unidirectional morphisms in Coq
Link to Code Gist
I have the following definition
...
- 1,502
1
vote
1
answer
73
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
262
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
99
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
160
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
218
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
82
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
99
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