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.

Filter by
Sorted by
Tagged with
1 vote
1 answer
47 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 ...
Agnishom Chattopadhyay's user avatar
4 votes
1 answer
205 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. ...
ignorant student's user avatar
1 vote
1 answer
81 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 ...
Jozef Mikušinec's user avatar
0 votes
0 answers
117 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 ...
Russoul's user avatar
  • 345
3 votes
1 answer
146 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? ...
Liu Xiaoyi's user avatar
1 vote
1 answer
193 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
Tim Eric's user avatar
1 vote
1 answer
75 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 ...
Adrian L's user avatar
2 votes
1 answer
101 views

Eta-equality for records: the case of semigroups

Consider the following definition of a semigroup: ...
Jon's user avatar
  • 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 ...
Trebor's user avatar
  • 3,867
2 votes
1 answer
102 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 ...
Russoul's user avatar
  • 345
1 vote
1 answer
140 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 ...
Agnishom Chattopadhyay's user avatar
0 votes
1 answer
63 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 ...
Felipe's user avatar
  • 63
1 vote
2 answers
173 views

Weird use of equality in Coq

I have a situation that is kind of like this: ...
sudgy's user avatar
  • 193
2 votes
1 answer
169 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 ...
Matematiflo's user avatar
4 votes
3 answers
370 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 ...
sudgy's user avatar
  • 193
1 vote
1 answer
106 views

Destruction of bound dependent types

I'm having an issue with dependent typing. I have reduced it to the following minimal example: ...
Adrian L's user avatar
2 votes
1 answer
236 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 ...
Jason Rute's user avatar
  • 8,535
2 votes
1 answer
238 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 ...
Felipe's user avatar
  • 273
0 votes
1 answer
145 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, ...
Pavel Snopov's user avatar
4 votes
2 answers
227 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. ...
Molly Stewart-Gallus's user avatar
9 votes
2 answers
450 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
Couchy's user avatar
  • 2,211
11 votes
2 answers
404 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 ...
L. F.'s user avatar
  • 213
10 votes
0 answers
168 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 ...
Trebor's user avatar
  • 3,867
3 votes
2 answers
200 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 ...
Maya's user avatar
  • 151
9 votes
1 answer
486 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 ...
Jason Rute's user avatar
  • 8,535
16 votes
2 answers
379 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 ...
Blaisorblade's user avatar
8 votes
1 answer
178 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:: ...
Mark Utting's user avatar
19 votes
2 answers
657 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? ...
Jia Ming جيا ميڠ's user avatar