Giving a proof in the type

Stream: new members

[Bhavik Mehta]

I'm getting the type mismatch error: term A has type (rset r X) but is expected to have type (rset (r - 1 + 1) X). r is a nat, so I understand why this error is happening but I have the assumption r ≥ 1 - so how do I express my lemma to convince lean that these types match

[Bhavik Mehta]

(to save anyone looking, it's nat.sub_add_cancel that should solve this)

[Kevin Buzzard]

Aah, the joys of type theory. If r>=1 then perhaps you should have used r' := r-1 with r'>=0 instead? But you'll have to post code to get hints.

[Kevin Buzzard]

This sort of issue can sometimes result in a redesign. I'll dig out the cdga thread to show you type theory at its worst.

[Bhavik Mehta]

Yeah, it turned out to be nicer to express it like that - but this is the sort of thing I feel like I'll come across again, where redesigns don't seem like the right approach

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167848869

[Kevin Buzzard]

Hopefully you can just insert an appropriate rewrite and it will sort you out. Reid chose an intentionally nasty example, and various solutions were proposed there.

[Wojciech Nawrocki]

For Lean to accept a term of type rset (r-1+1) X in a place where rset r X is expected, you have to cast/rewrite it using a proof of r-1+1 = r. This is because the Lean typechecker doesn't "know" that these are the same if r \geq 1.