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
67
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 ...
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 ...
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
vote
1
answer
74
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 ...
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 ...
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 ...
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?
...
1
vote
1
answer
220
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
1
vote
1
answer
83
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 ...
2
votes
1
answer
105
views
Eta-equality for records: the case of semigroups
Consider the following definition of a semigroup:
...
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 ...
2
votes
1
answer
105
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 ...
1
vote
1
answer
146
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 ...