I am trying to define something in a proof. I have the following set up:

```
Definition nat_rec (P : nat -> Type) (p0 : P 0) (psuc : forall n, P n -> P (S n)) (n : nat) : P n.
Proof.
Definition
sigsuc (p : {n | P n}) : {n | P n} :=
match p with
| (n ; pn) => (S n, psuc _ pn)
end.
```

I get told that the reference to P was not found in the current environment, is there a different way to make something like this work (apologies I am not experienced at coq).

You are looking for tactics such as `pose`

and `set`

: https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.pose

Thank you!

Could you tell me how you can add a type sig to `pose`

or `set`

. What I tried did not seem successful.

I don't know the answer but `refine (let sigsuc (p : {n | P n}) : {n | P n} := (blah) in _)`

seems like a workaround.

Last updated: Jun 24 2024 at 14:01 UTC