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: Oct 13 2024 at 01:02 UTC