Zulip Chat Archive

Stream: new members

Topic: identity type and refl


view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:46):

Is it possible to pattern match on the refl constructor of the identity type (eq.refl) in Lean similar to what one can do in Agda? I tried defining one by pattern matching but it didn't seem to work.

view this post on Zulip Mario Carneiro (Nov 13 2018 at 15:50):

yes, there are several ways

view this post on Zulip Mario Carneiro (Nov 13 2018 at 15:51):

subst and cases both work, as does the pattern matcher

view this post on Zulip Mario Carneiro (Nov 13 2018 at 15:52):

note that one side of the equality must be a variable and must participate in the pattern match (be right of the colon) for it to work

view this post on Zulip Reid Barton (Nov 13 2018 at 15:52):

Can you give an example of code you expect to work but doesn't?

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:53):

def subst {A : Type }(P : A  Type ℓ'){a b : A} : a = b  P a  P b :=
  assume p : a = b,
  assume x : P a,
  show P b, from eq.cases_on p x

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:54):

works fine

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:54):

but then

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:54):

def subst_const
  {A : Type }
  {B : Type ℓ'}
  {x y : A}
  : Π
  (p : x = y)
  (b : B)
  , ---------------------
  subst (λ _ , B) p b = b
| (eq.refl) _ := eq.refl

doesn't work

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:55):

This is something I've used a lot in Agda, and I figured if I try to do some of these "basic" things in Lean that could help me learn it, but I think that maybe I don't understand the basic syntax well enough yet...

view this post on Zulip Reid Barton (Nov 13 2018 at 15:55):

Yes, that is because the requirement "one side of the equality must be a variable and must participate in the pattern match (be right of the colon)" (or in this case, below the colon :slight_smile:) is not met

view this post on Zulip Reid Barton (Nov 13 2018 at 15:58):

y needs to move past the colon, and the last line should read | _ (eq.refl _) _ := eq.refl _

view this post on Zulip Reid Barton (Nov 13 2018 at 15:59):

or replace eq.refl _ with rfl

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 15:59):

okay, got it, can I still keep y implicit?

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 16:00):

it seems I can

view this post on Zulip Shaun Steenkamp (Nov 13 2018 at 16:01):

thank you very much for your help!! ^_^


Last updated: May 16 2021 at 20:13 UTC