3
$\begingroup$

I have been using lean for a while and I have noticed that I can't actually prove extensionality for my dependent structures. I was worried at first and then noticed that it was essentially dependent equality that I did not have:

def dependent_equality (X : Type) (A : X → Type) (x : X) (y : X) (p : x = y) : A x = A y := by sorry

For example, X could be Int and A could be ℤ/nℤ in the above, in which case I would want an inhabitant of A n = A m when n = m. I don't know anything about equal types in Lean, but I was more concerned with certain dependent structures whose corresponding extensionality principals had to be made into axioms.

How does Lean handle dependent equality, or why does it not?

For another more meaningful example, given a structure S with possibly dependent entries e₁,...,eₙ, I want to be able to show that (a₁ : e₁) → (b₁ : e₁) → (a₁ = b₁) → S.mk a₁ = S.mk b₁. With some dependent structures, I have noticed that I can't actually demonstrate extensionality because I get that something isn't "type correct". Meanwhile, it seems that if I was allowed to do multiple rewrites in a row before something was type checked that would solve the problem.

While I am mainly interested in dependent structures up to an equivalence of some kind, I think there are also times where it would be nice to have that property involving .mk.

$\endgroup$
3
  • $\begingroup$ Are you perhaps looking for heterogenous equality HEq? $\endgroup$ Aug 5, 2023 at 3:23
  • $\begingroup$ @FrançoisG.Dorais yes that's exactly what I want. How would you introduce HEq and how to you obtain ordinary = from HEq? $\endgroup$ Aug 6, 2023 at 19:04
  • $\begingroup$ Look at eq_of_heq and heq_of_eq. There are some more refined theorems but I think many are currently missing. $\endgroup$ Aug 6, 2023 at 21:08

1 Answer 1

4
$\begingroup$

Replace sorry with congr proves the first one.

For the second question, instead of what you have:

S.mk a₁ = S.mk b₁

You want to show:

S.mk a₁ == S.mk b₁

Where == is an alias of heq, which is a version of = that allows two sides to have different types. It can be converted back and forth with =, see this for example.

$\endgroup$
9
  • $\begingroup$ It says there that Eq.subst is only for propositions. Is there a substitution for dependent types? $\endgroup$ Aug 6, 2023 at 19:03
  • $\begingroup$ I took a look and thought that replacing = with heq may help you the most. $\endgroup$
    – ice1000
    Aug 7, 2023 at 3:20
  • 1
    $\begingroup$ Oh oh I see, it's HEq that I want. I'm looking for the info on HEq then. Are people ever suspicious of HEq? $\endgroup$ Aug 7, 2023 at 4:05
  • $\begingroup$ @Cayley-Hamilton It is incompatible with HoTT, but Lean is not HoTT so it shouldn't matter. $\endgroup$
    – ice1000
    Aug 7, 2023 at 6:07
  • $\begingroup$ Right. How does it work with the forall sign? Can you link me to some rules for HEq? $\endgroup$ Aug 7, 2023 at 6:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.