Stream: math-comp users

Topic: ✔ Got `_m_` while eliminating inductive proposition

abab9579 (Sep 02 2022 at 00:42):

I have inductively defined Foo (m: nat) f defined alike

Inductive Foo (m: nat) f :=
  | Foo0 : Bar f -> Foo 0 f
  | FooS : forall (m: nat), Baz (Foo m) f -> Foo m.+1 f

Then, I destructured it as follows.

(* I had a hypothesis (Hm: Foo m.+1 f) here *)
case Eq: m'.+1 f / Hm=> //.

Now I got bunch of variables like _m_, _f_ introduced.
I heard this method of inversion gives me more control, so I did not expect this.
Why is this happening? Is there a way to assign names that I want?

I also cannot use these hypothesis, it says "identifier is reserved".

Paolo Giarrusso (Sep 02 2022 at 01:29):

IIRC you can introduce them (and give names) after the =>. Usually ssreflect would let you leave them in the goal, but that'd be ill-typed here, since you're introducing Eq.

abab9579 (Sep 02 2022 at 01:44):

Thank you! I was confused because it gave a branch, so I needed to introduce variables for each branch.

Notification Bot (Sep 02 2022 at 03:14):

abab9579 has marked this topic as resolved.

Last updated: Apr 19 2024 at 14:02 UTC