Skip to main content
18 votes
Accepted

What is the difference between refl and rfl in Lean 3?

So you are correct that refl is a tactic, and rfl is a term, so for example: ...
It'sNotALie.'s user avatar
  • 1,445
11 votes

What are the upsides and downsides of typed vs untyped conversion?

From the perspective of implementation of conversion checking, it really depends on the specific setting. For vanilla intuitionistic type theories without more exotic features (like cubical TT, ...
András Kovács's user avatar
9 votes

What is the difference between refl and rfl in Lean 3?

Separately from the rfl (term) vs refl (tactic) distinction, there is also the distinction between ...
Eric's user avatar
  • 971
8 votes

Proving uniqueness of an instance of an indexed inductive type

Or, what would a better way to prove s = single_O? I would define a function that, given a nat n, computes the canonical proof <...
gallais's user avatar
  • 1,166
8 votes
Accepted

How does Metamath Zero handle CIC as in Lean or Coq?

All three of your possibilities are potential options for future directions, although they get progressively more "future" as you go down the list. Extract the full proof from a modified ...
Mario Carneiro's user avatar
6 votes
Accepted

Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?

Indeed, it holds: ...
JoJoModding's user avatar
5 votes

Weird use of equality in Coq

Welcome to homotopy type theory. What if eq : i = i in convert_eq is not refl? Then ...
Andrej Bauer's user avatar
  • 9,194
5 votes

What are the upsides and downsides of typed vs untyped conversion?

Typed conversion makes establishing metatheoretical properties of the syntax overwhelmingly easier, especially if you want to prove things like decidability of typechecking. Basically, when showing ...
Neel Krishnaswami's user avatar
5 votes

Defining coercion for proof irrelevant equality

In the latest versions of Coq, you can use an irrelevant equality, and eliminate it into Set/Type, see the reference manual. You ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

Defining coercion for proof irrelevant equality

Agda has a runtime irrelevance modality which may be closer to what you want. In particular, since there's only one constructor, it is ok to eliminate the identity type even if it is marked irrelevant....
Trebor's user avatar
  • 3,967
5 votes
Accepted

Proving uniqueness of an instance of an indexed inductive type

Rergarding IDProp, this is the pattern-matching compilation of Coq at work. Basically, because you scrutinee has a type that can only correspond to the ...
Meven Lennon-Bertrand's user avatar
5 votes

Why do coinductive types require bisimilarity relations?

Semantically, bisimulation just is the correct notion of equality for coinductive types. A nice intuition for it comes from parametricity. The Church encoding of a coinductive stream type $\nu a.\,(\...
Neel Krishnaswami's user avatar
4 votes
Accepted

Why do coinductive types require bisimilarity relations?

Coinductive types "require bisimilarity instead of =" for the same reason function types "require ...
HTNW's user avatar
  • 533
4 votes
Accepted

Definitional vs propositional equality

My understanding is that two terms are definitionally equal if they reduce to the same term via partial evaluation. With add defined as ...
tarzh's user avatar
  • 291
4 votes
Accepted

Reasoning about non reflexive equalities & type conversions

First a general answer: you cannot get rid of cast in general without further assumptions because type theory has an interpretation in which such casts may have non-trivial actions, namely homotopy ...
Andrej Bauer's user avatar
  • 9,194
4 votes
Accepted

Dealing an equality with coq. - beginner's question

In the pattern-matching, Coq does know that x, y andz "are the same", but the way ...
Meven Lennon-Bertrand's user avatar
3 votes

General method for disproving possibility of judgemental equality

This is a really interesting question! I'll try to give some pointers to some possible answers. One more general question you might ask is What equivalence relations have constructive quotients? ...
cody's user avatar
  • 384
3 votes

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?

The universal property of final coalgebras can be formalized as unique-ana : ∀ (f : A → B × A) (g : A → Stream B) → unfold ∘ g ≡ map₂ g ∘ f → g ≡ ana f where <...
Li-yao Xia's user avatar
  • 1,757
3 votes

Is there an elegant way of proving an equality A=B by going in both directions?

I believe there is, provided that L and R are predicates, of course: ...
user9716869 - supports Ukraine's user avatar
3 votes
Accepted

Destruction of bound dependent types

Coq simply tells you that when it is trying to do a case on n ?= n in the expression ...
Lolo's user avatar
  • 476
3 votes
Accepted

Is type checking in "Ideal Lean" computably enumerable?

Yes. The reasons are as you stated: A typing judgment is a statement about finite objects (expressions and contexts), and because typing judgments are inductively defined, every judgment has a "...
Mario Carneiro's user avatar
3 votes
Accepted

How do I enable this kind of rewriting?

In order to add a Morphism, your function needs a name. It can't just be an anonymous function. Below is a minimal working example. ...
djao's user avatar
  • 434
2 votes
Accepted

Equational reasoning in Coq

This is a hint. Note that you have the following axiom: Axiom ax_f: forall (x y: T), f x (g x y) = x. and your goal is ...
Ana Borges's user avatar
2 votes

How do I make use of an irrelevant equality in a proof?

You can turn an irrelevant proof into a relevant one if you assume excluded middle: ...
Maya's user avatar
  • 151
2 votes
Accepted

Weird use of equality in Coq

This kind of thing is possible if equality on I is decidable. ...
djao's user avatar
  • 434
2 votes

How to deduce this equality based on the fact that these two terms must be the same?

This is a dependent inversion problem that has been bothering many Coq users. There is a short answer on Stack Overflow [1]. For your example, we have H before ...
Qinshi Wang's user avatar
2 votes
Accepted

Rewriting/Applying unidirectional morphisms in Coq

Morphisms only affect rewrite, not apply. The following does work, and makes use of the ...
djao's user avatar
  • 434
1 vote

how to prove 2+2+a=4+a in lean4?

norm_num is a good tactic for this sort of stuff: ...
Jason Rute's user avatar
  • 8,685
1 vote

Use proof irrelevance in cast

It is indeed possible, but not so easy to build infrastructure to do. I'd suggest you have a look at MathComp's subType class, and how it organizes the set of ...
ejgallego's user avatar
  • 111
1 vote
Accepted

Eta-equality for records: the case of semigroups

One approach is to do things the other way around: define SG with all the fields, without any one of them being defined. Then define an interface that will ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible