Zulip Chat Archive

Stream: new members

Topic: easy questions


view this post on Zulip Adrian Chu (Jun 26 2019 at 08:23):

theorem test (x : ):  a : , 2*a = 4 := sorry

theorem test2 (x : ):  b : , 3*b = 6 :=
begin
fapply exists.intro,
  exact 3, sorry
end

in this stupid theorem, i want to replace 3 with the a given by test, how should i write?

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:25):

you can't take out what you put in the proof of an existential statement

view this post on Zulip Adrian Chu (Jun 26 2019 at 08:27):

huh? but then how should we define a number x+1, in which the existence of x is guaranteed by some previous theorem A?

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:28):

example (choice : Π (C :   Prop), ( n, C n)  )
  (spec :  (C :   Prop) (n : ) (h : C n), choice C n, h = n) :
  false :=
nat.zero_ne_one $ show 0 = 1, from
calc  0
    = choice (λ n, n = n) 0, rfl : (spec (λ n, n = n) 0 rfl).symm
... = choice (λ n, n = n) 1, rfl : rfl
... = 1                           : spec (λ n, n = n) 1 rfl

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:28):

this is because of proof irrelevance, where two proofs of the same theorem are definitionally equal

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:29):

so in particular two witnesses result in the same proof of the existential.

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:32):

but you can use a subtype to retain the witness:

def test : { a :  // 2*a = 4} := 2, rfl

theorem test2 :  b : , 3*b = 6 := test.1, rfl

view this post on Zulip Alistair Tucker (Jun 26 2019 at 08:35):

But if you want only want to use the witness a in a proof of something else then you can say cases test with a ha,

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:36):

oh right

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:38):

theorem test :  a : , 2*a = 4 := 2, rfl

theorem test2 :  b : , 3*b = 6 :=
begin
  cases test with a ha,
  refine a, _⟩,
  have : a = 2,
  { rw two_mul at ha,
    exact nat.bit0_inj ha },
  subst this,
  refl
end

view this post on Zulip Adrian Chu (Jun 26 2019 at 08:42):

i see, thanks!!

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 10:56):

you can't take out what you put in the proof of an existential statement

Don't listen to the constructivist!

import tactic.interactive

theorem test (x : ):  a : , 2*a = 4 := sorry

theorem test2 (x : ):  b : , 3*b = 6 :=
begin
  choose a ha using test 37,
  /-
  1 goal
  x a : ℕ,
  ha : 2 * a = 4
  ⊢ ∃ (b : ℕ), 3 * b = 6
  -/
  sorry
end

[why does test take an input which is never used?]

view this post on Zulip Reid Barton (Jun 26 2019 at 10:59):

You don't need choose here, just cases which was mentioned earlier

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 11:01):

Sure, but this is a refutation of Kenny's claim "you can't take out what you put in the proof of an existential statement". The issue with choose is that it is noncomputable (Lean actually forgot a once it had checked your proof, so there is no algorithm for getting it back).

view this post on Zulip Kenny Lau (Jun 26 2019 at 12:31):

but my point was that you can't take out what you put in, i.e. the explicit witness you constructed

view this post on Zulip Kenny Lau (Jun 26 2019 at 12:31):

contrary to maths where you can always destruct an existential to get data

view this post on Zulip Mario Carneiro (Jun 26 2019 at 12:33):

I don't know that in maths the behavior is much different from choose

view this post on Zulip Mario Carneiro (Jun 26 2019 at 12:34):

Except possibly that you can prove additional properties to put in the existential after the fact

view this post on Zulip Mario Carneiro (Jun 26 2019 at 12:34):

but this is more of a proof structuring thing

view this post on Zulip Keeley Hoek (Jun 26 2019 at 12:41):

I think the situation in real maths is just that if you constructed an existential by directly producing a term, then if you ever need it later you're allowed to remember your proof and the element

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 12:49):

It's even better than that, we're even allowed to say "By the proof of Theorem 3.2, ..."

view this post on Zulip Adrian Chu (Jun 27 2019 at 11:46):

how to prove that

def x:    := (λ i, i+1)
def y:    := (λ i, 1+i)
theorem test : x = y  := by sorry

? library search gives nothing

view this post on Zulip Johan Commelin (Jun 27 2019 at 11:48):

begin
  funext i,
  sorry
end

view this post on Zulip Johan Commelin (Jun 27 2019 at 11:49):

Or in term mode: funext $ _

view this post on Zulip Adrian Chu (Jun 27 2019 at 11:51):

i see

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:10):

Why does rfl fail?

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:10):

def x:    := (λ i, i+1)
def y:    := (λ i, 1+i)
theorem test : x = y  := rfl -- type mismatch

view this post on Zulip Kenny Lau (Jun 27 2019 at 12:18):

the first one is i+1 and the second one is 1+i

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:26):

oh thanks. Duh.

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:26):

The colours played a trick on my brain somehow

view this post on Zulip Keeley Hoek (Jun 27 2019 at 12:35):

Whoever made the courier new typeface has caused at least billions of dollars of damage with how close i and 1 look

view this post on Zulip Adrian Chu (Jun 27 2019 at 14:08):

wouldn't 1 and l be deadlier?

view this post on Zulip Marc Huisinga (Jun 27 2019 at 14:36):

1ucki1y l is 1ess common in programming

view this post on Zulip Keeley Hoek (Jun 29 2019 at 06:34):

is it illegal to delcare a long literal in Java with a lower case l?

view this post on Zulip Keeley Hoek (Jun 29 2019 at 06:34):

If no, that's a good one

view this post on Zulip Mario Carneiro (Jun 29 2019 at 06:49):

that's legal

view this post on Zulip Johan Commelin (Jun 29 2019 at 07:05):

There's an entire class of "off-by-l" errors

view this post on Zulip Gun Pinyo (Jul 21 2019 at 16:53):

Hi guys, I want to use the heterogeneous equality but cannot derive it to homogeneous equality. i.e. can we define the following?

    def foo (α β : Type) (p : α = β) (x : α) (y : β) :
              x == y  (eq.rec_on p x : β) = y := sorry

view this post on Zulip Chris Hughes (Jul 21 2019 at 16:57):

def foo (α β : Type) (p : α = β) (x : α) (y : β) :
              x == y  (eq.rec_on p x : β) = y := λ h, by cases h; refl

view this post on Zulip Chris Hughes (Jul 21 2019 at 17:01):

You don't need the assumption α = β, it's implied by x == y

view this post on Zulip Gun Pinyo (Jul 21 2019 at 17:01):

@Chris Hughes ah, thanks. but how about another way?

view this post on Zulip Gun Pinyo (Jul 21 2019 at 17:04):

wait, if we don't need p : α = β, then how can we express (eq.rec_on p x : β) = y?

view this post on Zulip Chris Hughes (Jul 21 2019 at 17:05):

You could write eq.rec_on (type_eq_of_heq (h : x == y)) x

view this post on Zulip Gun Pinyo (Jul 22 2019 at 10:34):

Hi, there. Can anyone tell me why the following example doesn't work?

example (α β : Type) (p : α = β) : unit  α = unit  β :=
  begin rw p, reflexivity end

after rw p the goal is unit → β = unit → β but reflexivity doesn't work.

view this post on Zulip Chris Hughes (Jul 22 2019 at 10:35):

Brackets

example (α β : Type) (p : α = β) : (unit  α) = (unit  β) :=
  begin rw p end

view this post on Zulip Gun Pinyo (Jul 22 2019 at 10:36):

@Chris Hughes wow, such a silly mistake. Thank you

view this post on Zulip Kenny Lau (Jul 22 2019 at 10:43):

example (α β : Type) (p : α = β) : unit  α = unit  β :=
  begin intros _ h, rw [ p, h], exact () end

view this post on Zulip Gun Pinyo (Jul 22 2019 at 18:06):

Does lean have something like the following in standard library or mathlib?

def uip (α : Prop) (x y : α) : x = y := sorry

if not, how can we prove this?

view this post on Zulip Kenny Lau (Jul 22 2019 at 18:07):

rfl

view this post on Zulip Kenny Lau (Jul 22 2019 at 18:07):

this is called proof irrelevance and is built into Lean

view this post on Zulip Kenny Lau (Jul 22 2019 at 18:07):

it says that two proofs of the same proposition are definitionally equal

view this post on Zulip Gun Pinyo (Jul 22 2019 at 18:08):

@Kenny Lau , thank you :)

view this post on Zulip Gun Pinyo (Jul 25 2019 at 10:52):

I have a problem with unfolding tactic. Considering the following code

structure graph :=
  (nodes  : Type)
  (edges  : Type)
  (srctrg : bool  edges  nodes)

def prism_graph (G : graph) : graph :=
  { nodes  := bool × G.nodes
  , edges  := (bool × G.edges)  G.nodes
  , srctrg := λ b e, match e with
                     | (sum.inl (b', e)) := (b, G.srctrg b' e)
                     | (sum.inr v)       := (b, v)
                     end
  }

def cube_graph :   graph
| 0      := unit, unit, (λ _ _, ())
| (n +1) := prism_graph (cube_graph n)

example (n : ) (b : bool) (v : (cube_graph n).nodes) :
      (graph.srctrg (cube_graph (n +1)) b (sum.inr v)) = (b, v) :=
  begin
    unfold cube_graph,
  end

I don't understand why unfold cube_graph fails. Clearly, it should succeed with the goal become (graph.srctrg (prism_graph (cube_graph n)) b (sum.inr v)) = (b, v).

Ps. You might argue that I can close this tactic by refl but my point is to use unfold. The reason is that this is the simplified version of the actual problem that I am working and I can't just use refl.
Ps2. This is another question. If refl works, why simp doesn't. Isn't simp use refl at the end anyway?

view this post on Zulip Patrick Massot (Jul 25 2019 at 11:02):

You're expecting too much from unfold. What you want here is dsimp [cube_graph].

view this post on Zulip Patrick Massot (Jul 25 2019 at 11:03):

About your second question, maybe simp is actually doing some thing which turns your goal into a non-refl goal.

view this post on Zulip Chris Hughes (Jul 25 2019 at 11:03):

You can use dunfold. The reason simp doesn't work, is because graph.srctrg is a dependent function, so the expression after rewriting only typechecks because cube_graph (n + 1) = prism_graph (cube_graph n) is s definitional equality.

view this post on Zulip Gun Pinyo (Jul 25 2019 at 13:23):

@Patrick Massot @Chris Hughes Thank you for introducing dsimp and dunfold to me.

Another question, if I have two occurrences of the same
definition in a goal. (d)unfold once will affect the first
occurrence an not the second, if I want another way (i.e. affect the second
one and not the first one) what should I do?

view this post on Zulip Kevin Buzzard (Jul 25 2019 at 13:25):

Definitional unfolding is all defeq, so if your goal does not look like what you want it to look like, you can just write change <what you want the goal to look like> and if what you write is definitionally equal to what the goal is, the goal will change to what you write. Note that show is synonymous with change, although you can use change on hypotheses as well.

view this post on Zulip Kevin Buzzard (Jul 25 2019 at 13:26):

The other approach for zooming in on terms in goals is conv mode: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

view this post on Zulip Kevin Buzzard (Jul 25 2019 at 13:27):

I don't know how much you know about definitional equality v all the other equalities, but here's something I wrote about definitional equality: https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/

view this post on Zulip Chris Hughes (Jul 25 2019 at 13:28):

Patrick Massot Chris Hughes Thank you for introducing dsimp and dunfold to me.

Another question, if I have two occurrences of the same
definition in a goal. (d)unfold once will affect the first
occurrence an not the second, if I want another way (i.e. affect the second
one and not the first one) what should I do?

Do you have an example of this. Usually I think it unfolds all occurrences, so it might be not unfolding the second one for some other reason.

view this post on Zulip Kevin Buzzard (Jul 25 2019 at 13:31):

Another thing you might want to know is that if you type #print prefix cube_graph then you can see all the stuff that Lean generated for you when you made cube_graph. Things called cube_graph._equation.1 or something (I forget what they're exactly called) are the things which Lean tries to use when you run unfold -- that's what the tactic actually does. Similarly dsimp [cube_graph] tries to simplify using those "hidden" equation lemmas.

view this post on Zulip Gun Pinyo (Jul 25 2019 at 13:35):

@Kevin Buzzard Thank you for introducing change and conv. These what tactics that I have been looking for many days. It is also interesting to know that we can even unfold anonymous functions as well.

@Chris Hughes I have but it is in a long file and it can be the case that the second occurrence is not unfoldable at the moment so I miss understood the behaviour of (d)unfold .

view this post on Zulip Jesse Michael Han (Jul 25 2019 at 15:13):

@Gun Pinyo you should definitely read through the general mathlib tactic documentation

view this post on Zulip Gun Pinyo (Jul 27 2019 at 10:48):

If I am in the tactic mode with 2 goals. Is there any tactic that lets me prove the second goal before the first one?
The motivation behind this is when the second goal is a lot easier than the first one.

Ps. I have read through https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md but didn't find any.

view this post on Zulip Kevin Buzzard (Jul 27 2019 at 10:48):

swap

view this post on Zulip Kevin Buzzard (Jul 27 2019 at 10:48):

Once you've got it working, hover over the tactic to see the docstring.

view this post on Zulip Gun Pinyo (Jul 27 2019 at 10:52):

@Kevin Buzzard Thank you.
So there are more tactics that are not in mathlib. Where can I find the documentation of these built-in tactics?
At first, I thought every built-in tactic should be in https://leanprover.github.io/reference/tactics.html# but it is not the case for swap.

view this post on Zulip Kevin Buzzard (Jul 27 2019 at 10:54):

Maybe swap is in core Lean? You can just right click on it to check.

view this post on Zulip Kevin Buzzard (Jul 27 2019 at 10:54):

A great place for learning about core tactics is the book Theorem Proving In Lean.

view this post on Zulip Bryan Gin-ge Chen (Jul 27 2019 at 10:59):

It would be good to add swap and any other missing core tactics to that doc page. Maybe for now we should just add a comment to this issue https://github.com/leanprover-community/mathlib/issues/450

view this post on Zulip Gun Pinyo (Jul 27 2019 at 10:59):

@Kevin Buzzard I agree, that was what I did before starting my current project.
But again, it doesn't mention swap.

view this post on Zulip Gun Pinyo (Jul 27 2019 at 11:04):

Oh, btw, swap is defined in mathlib and not the builtin one. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean

view this post on Zulip Keeley Hoek (Jul 27 2019 at 13:48):

If I recall, core defines tactic.swap but does not expose to interactive?

view this post on Zulip Gun Pinyo (Aug 07 2019 at 14:01):

This might be a very stupid question but why can't we add univalence axiom to lean3? i.e. why axiom K of lean3 doesn't play well with the univalence axiom?

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:01):

(deleted)

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:02):

(deleted)

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:02):

This has been talked about before and I know it's inconsistent but I don't know why. It's something to do with impredicativity of Prop

view this post on Zulip Chris Hughes (Aug 07 2019 at 14:10):

Because equality is a subsingleton, and univalence says it is isomorphic to something which is not a subsingleton. Even if you define a equality to return a type, rather than a Prop, this is still provably a subsingleton (the proof uses the proof irrelevant version of eq).

view this post on Zulip Chris Hughes (Aug 07 2019 at 14:11):

I think α ≃ β → α = β is consistent though, but not very useful.

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:15):

So is even my undeleted post incorrect?

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:16):

Because α = β → α ≃ β is a theorem

view this post on Zulip Chris Hughes (Aug 07 2019 at 14:18):

Those two function aren't inverses of each other in Lean, but univalence says they are.

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:19):

Surely α ≃ β → α = β would be useful in Lean, because it would enable me to show that if R and S are isomorphic rings and R is Noetherian local then S is Noetherian local?

view this post on Zulip Chris Hughes (Aug 07 2019 at 14:21):

You also need the ring structures to be heq for that. Which won't be provable.

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:23):

So you can't get from the bare α ≃ β → α = β statement about types to statements about isomorphic groups being equal groups by using some kind of trickery?

view this post on Zulip Kevin Buzzard (Aug 07 2019 at 14:23):

I would imagine that in HoTT they can do this somehow

view this post on Zulip Chris Hughes (Aug 07 2019 at 14:25):

I don't think so. In Lean, you have no idea what eq.mp gives you. In HoTT, you know from the right_inv part of the univalence equivalence, that eq.mpr is to_fun of your bijection. Then you can prove that eq.rec one_ring_strcuture = the_other_ring_structure

view this post on Zulip Chris Hughes (Aug 07 2019 at 14:29):

In the univalence equivalence inv_fun := eq.mp. The axiom says that eq.mp has a two sided inverse.

view this post on Zulip Floris van Doorn (Aug 07 2019 at 16:19):

In answer to the original question: from univalence you can show that bool = bool has two unequal elements (one corresponding to the identity function, and one corresponding to the function that swaps the elements), which contradicts axiom K.

view this post on Zulip Floris van Doorn (Aug 07 2019 at 16:23):

And I'm quite sure that Chris is right that weak univalence (α ≃ β → α = β) doesn't give you that isomorphic groups are equal.

view this post on Zulip Gun Pinyo (Aug 10 2019 at 15:57):

Hi, there. Regarding defined class in stdlib, many of them have one field. I try to understand why don't you just use def with @[class]? For example,

class inhabited (α : Sort u) :=
(default : α)

@[class] def inhabited' (α : Sort u) := α

inhabited' should be as usable as inhabited but we also don't need to write the constructor.

There are some classes that way such as in library/init/relator.lean. I can see the advantage of using the letter way but haven't seen the advantage of the former way. Could you please explain to me please?

view this post on Zulip Andrew Ashworth (Aug 11 2019 at 05:05):

<deleted>

view this post on Zulip Andrew Ashworth (Aug 11 2019 at 05:10):

<deleted>

view this post on Zulip Andrew Ashworth (Aug 11 2019 at 05:18):

<deleted>

view this post on Zulip Floris van Doorn (Aug 11 2019 at 05:25):

One difference is that inhabited' α is definitionally equal to α, while inhabited α is not (it is equivalent to α, in the sense that equiv (inhabited α) α can be proven).
Sometimes extra definitional equalities are convenient, but sometimes they have downsides. It is possible that the elaborator of Lean will unfold inhabited' in places where you didn't want to, and then you are not talking about the type inhabited' α anymore, but about α. The latter is not a class, which might cause issues with type class inference not firing.
Since inhabited is not a definition, it can never be unfolded.

view this post on Zulip Andrew Ashworth (Aug 11 2019 at 05:27):

This is a much better explanation of why, haha.

view this post on Zulip Gun Pinyo (Aug 11 2019 at 14:43):

@Floris van Doorn , how about we add @[irreducible] to inhabited' α, would it solved the problem with unwanted unfolding?

view this post on Zulip Reid Barton (Aug 11 2019 at 15:42):

In that case there won't be much advantage of the def over the single-field class

view this post on Zulip Floris van Doorn (Aug 11 2019 at 17:12):

That would also be fine. But as Reid said: if you don't want to unfold it, you can just as well make it a structure.

view this post on Zulip Gun Pinyo (Aug 11 2019 at 17:23):

Well, my point is that I don't want to keep writing .intro or something like that.

view this post on Zulip Andrew Ashworth (Aug 11 2019 at 17:39):

Angle bracket notation doesn't work for you?

view this post on Zulip Chris Hughes (Aug 11 2019 at 17:52):

If you marked it irreducible you'd have to define anintro and use that.

view this post on Zulip Gun Pinyo (Aug 14 2019 at 16:06):

I just discover that we can write numerals as elements of fin
type. So I want to refactor the following code:

def fin.zero {n : } : fin (n +1) := 0, nat.zero_lt_succ n
def vector.insert_nth_zero : v.insert_nth a fin.zero = a :: v :=
  begin
    cases v with l p,
    simp [fin.zero, vector.insert_nth, vector.cons, list.insert_nth],
  end

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
  begin
    cases v with l p,
    simp [{!what should be here?!}, vector.insert_nth, vector.cons, list.insert_nth],
  end

vector.insert_nth_zero' is the same as vector.insert_nth_zero
except that fin.zero is changed to 0. Everything should be fine, however, I don't know there to replace fin.zero in simp tactic now. Does anyone know how to fix this?

view this post on Zulip Joe (Aug 14 2019 at 17:01):

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
  begin
    cases v with l p,
    simp only [vector.insert_nth], norm_cast
  end

view this post on Zulip Joe (Aug 14 2019 at 17:05):

or maybe this

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
  begin
    cases v with l p,
    simp only [vector.insert_nth, vector.cons, subtype.mk_eq_mk],
    show list.insert_nth 0 a l = a :: l,
    simp [list.insert_nth]
  end

view this post on Zulip Gun Pinyo (Aug 15 2019 at 14:02):

I still have another question regarding fin. Sometimes, I want to use pattern matching on i : fin n in the same way as one will do in but since the inductive part is in i.val so I need to do as follows:

def fin_is_even : Π n : , fin n  bool
| 0      i                        := i.elim0
| (n +1) 0,    _⟩                := true
| (n +1) i_val +1, succ_i_is_lt :=
     let i : fin n := i_val, nat.pred_le_pred succ_i_is_lt
      in bnot (fin_is_even n i)

Ok it works, but in practice, I find it quite annoying to write let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩ every time whereas i should be obtained directly from something like fin.succ i. Therefore, I try to use @[pattern] to help me with this as follows:

@[pattern]
def fin.zero {n : } : fin (n +1) := 0, nat.zero_lt_succ n

attribute [pattern] fin.succ

def fin_is_even' : Π n : , fin n  bool
| 0      i            := i.elim0
| (n +1) fin.zero     := true
| (n +1) (fin.succ i) := bnot (fin_is_even' n i)

However I get an error, what is wrong with my code? Did I misunderstand anything about @[pattern]?

err msg1:
invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
err msg2:
don't know how to synthesize placeholder context: fin_is_even' : Π (n : ℕ), fin n → bool ⊢ fin n

view this post on Zulip Chris Hughes (Aug 15 2019 at 15:03):

You're basically expecting the equation compiler to determine whether an element of fin n is in the image of fin.succ or not, and if it is what the element that maps to it is. This is very hard in general. I think the pattern attribute only works for things that are definitionally equal to a constructor. for example λ x, x + 2 = λ x, nat.succ (nat.succ x), by definition, so marking add with the pattern attribute works. Incidentall changing your definition of fin.zero also works - it also wanted to reduce the proof to a constructor, but it's probably not a desirable change.

@[pattern]
def fin.zero {n : } (h): fin (nat.succ n) := 0, h

attribute [pattern] fin.succ

def fin_is_even' : Π n : , fin n  bool
| 0      i            := i.elim0
| (n +1) (fin.zero h)     := true
--| (n +1) x := bnot (fin_is_even' n i)

view this post on Zulip Gun Pinyo (Aug 15 2019 at 17:31):

@Chris Hughes , thank you, now I can see why fin.succ doesn't work. Anyway, is there any other that allow us use something like fin.zero and fin.succ in pattern matching? I really miss the following alternative definition of fin

inductive fin' :   Type
| zero : fin' 0
| succ : Π {n : }, fin' n  fin' (n +1)

But I use this definition, it is incompatible with the standard library.

I think the pattern attribute only works for things that are definitionally equal to a constructor

How about this following code in data.vector? Is this definitionally equal to any constructor? I fact, I haven't seen any code using pattern matching on vector

@[pattern] def nil : vector α 0 := [],  rfl

@[pattern] def cons : α  vector α n  vector α (nat.succ n)
| a  v, h  :=  a::v, congr_arg nat.succ h 

view this post on Zulip Chris Hughes (Aug 15 2019 at 17:46):

nil definitely is. cons definitely isn't.

Actually it depends on the vector you're trying to match with. If your vector is a variable then it won't work. If you do

match vector.mk l rfl with...

Then it has a better chance of working, but I think the prood of equality would have to be rfl.

view this post on Zulip Kevin Buzzard (Aug 16 2019 at 07:17):

I thought this variant of fin was in mathlib somewhere


Last updated: May 08 2021 at 02:46 UTC