identity type and refl

Stream: new members

[Shaun Steenkamp]

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.

[Mario Carneiro]

yes, there are several ways

[Mario Carneiro]

subst and cases both work, as does the pattern matcher

[Mario Carneiro]

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

[Reid Barton]

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

[Shaun Steenkamp]

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

[Shaun Steenkamp]

works fine

[Shaun Steenkamp]

but then

[Shaun Steenkamp]

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

[Shaun Steenkamp]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

or replace eq.refl _ with rfl

[Shaun Steenkamp]

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

[Shaun Steenkamp]

it seems I can

[Shaun Steenkamp]

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