# Tag Info

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: ...
• 1,445

### 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, ...
• 2,077

### 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 ...
• 971

### 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 <...
• 1,166
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 ...
• 1,579
Accepted

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

Indeed, it holds: ...
• 421

### Weird use of equality in Coq

Welcome to homotopy type theory. What if eq : i = i in convert_eq is not refl? Then ...
• 9,194

### 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 ...
• 2,013

### 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 ...
• 5,046
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....
• 3,967
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 ...
• 5,046

### 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.\,(\...
• 2,013
Accepted

### Why do coinductive types require bisimilarity relations?

Coinductive types "require bisimilarity instead of =" for the same reason function types "require ...
• 533
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 ...
• 291
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 ...
• 9,194
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 ...
• 5,046

### 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? ...
• 384

### 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 <...
• 1,757

### 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: ...
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 ...
• 476
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 "...
• 1,579
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. ...
• 434
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 ...
• 936

### 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: ...
• 151
Accepted

### Weird use of equality in Coq

This kind of thing is possible if equality on I is decidable. ...
• 434

### 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 ...
Accepted

### Rewriting/Applying unidirectional morphisms in Coq

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

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

norm_num is a good tactic for this sort of stuff: ...
• 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 ...
• 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 ...
• 5,046

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